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

[Adam Chlipala]

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. :-)

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. :])

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..