[Ur] HTML5 tags: source tag conflict

[Adam Chlipala]

Your conundrum here is strictly simpler than the one for the HTML 
<table> tag, since 'table' is a keyword in Ur/Web!

The solution is to pick a different identifier in lib/ur/basis.urs, and 
then add a special-case translation rule in src/monoize.sml. Search for 
"tabl" to find the place where <table> already gets special handling.  
(The combinator in the standard library is called [tabl].)

On 05/03/2015 05:26 AM, Sergey Mironov wrote:
> Hi! I am working on adding HTML5 media tags to the basis. According to
> the reference [1], <audio> tag may contain one or more tags named
> <source>. Unfortunately, we already have value named 'source' in
> basis.ur. What can we do to address this issue?  I'll try to
> experiment with adding source tag via FFI for now and see how it looks
> like.
>
> Regards,
> Sergey
>
> [1] http://www.w3schools.com/tags/tag_audio.asp