[Ur] big string block in ur?

[Adam Chlipala]

hao deng wrote:
>      Is there a way to include a big block of txt (xml string  for
> example ) in Ur as a string ?
> There are many double quote in the txt. What I want is some thing like
> python's """ , triple quote.
>    

There isn't anything like that in there now.  I'm not sure it would be 
worth adding such a feature.  It wouldn't be hard to write a small 
program to properly encode any string into the form needed for an Ur 
string literal.