[Ur] Defining new tags like <pre>...

[Michael Stone]

On 3/5/10, Adam Chlipala <adamc at impredicative.com> wrote:
> Michael Stone wrote:
>> Second, in the course of playing with Ur/Web over the last few hours,
>> I encountered a need to produce an HTML<pre>  tag in a page.
>>
>> I was able to accomplish this objective by adding an entry to
>> lib/ur/basis.urs like so:
>>
>>    val div : bodyTag boxAttrs
>>    val span : bodyTag boxAttrs
>> +  val pre : bodyTag boxAttrs
>>
>> Unfortunately, I don't fully understand why making this change has the
>> desired effect. Would you mind saying a few words about why defining
>> this value "just works"?
>>
>
> The short answer is: the Ur/Web compiler is specialized to the standard
> library.  It compiles anything with a tag type like an XML tag.  You
> gave <pre> a tag type, so you got the behavior you wanted. :-)

Is the responsible logic mainly to be found in Monoize.monoExp
(specifically the cases following line 2545 in the 20100213 source
release)?

> It's worth pointing out that you will still encounter some friction from
> the optimizer, which doesn't know that whitespace inside <pre> has
> special semantics.  Every sequence of whitespace will be collapsed into
> one.  More special compiler support would really be needed to avoid
> this.  (Or I could turn off that optimization, but it's just so much
> fun. :])

Good to know. Where does this logic live?

> I'll also point out that it's easy to implement a function that provides
> <pre>-like functionality without a native browser tag, by replacing
> newlines with <br>, spaces with one of a variety of tricks for explicit
> space in HTML, etc..

Also worthwhile knowledge.

Thanks kindly,

Michael