Joe English responded:
>
> Sounds good to me.
>
> You might consider a TABSTOPS attribute too:
>
> <!attlist pre
> -- ... other attributes --
> tabwidth NUMBER #IMPLIED
> tabstops NUMBERS #IMPLIED
> >
>
> <pre tabstops="2 4 8 16 32">
> ..
> </pre>
>
> This would also be useful. (And, I hope, might
> replace the bletcherous <TAB> element in the current
> HTML 3 draft.)
>
Do we need both attributes? Two ways to get the same thing?
As long as we understand which one takes precedence, I suppose.
Murray