[opentheory-users] quoted strings

[Ramana Kumar]

On Mon, Jan 10, 2011 at 7:37 PM, Joe Hurd <joe at gilith.com> wrote:
> Hi Ramana,
>
>> First of all, what does it mean to obtain a string by matching a
>> regular expression?
>
> Good question: I've tightened up the language to
>
> "A name command is a string that matches the following regular expression:"
>
>> And then you're left with the string, you discard the quotes, but what
>> about the slashes inside the string?
>
> You leave the slashes in the string. The most important property here

Leave the slashes in the string?
But bool.art uses Data.Bool./\\, but I think the intention is for the
name to be Data.Bool./\, no?
I'm at the moment using String.fromString on the line I get back from
TextIO.inputLine - I can't keep track of where all these functions
(including whatever's printing things out to my terminal) add and
remove slashes. Would you expect to have to use fromString on a line
from an article, or should the line itself be right?
If the extra slash in bool.art is wrong, perhaps you got caught by an
SML printer that was trying to print something it could read back in
to a value.

> is that equality of names is the same as equality of the strings
> representing them. For example, the two names
>
> A.b
>
> and
>
> A\.b
>
> are different, so it is good that they are represented by different
> strings (because the slashes are left in).
>
> This is all that automatic tools for processing articles need to know.
> However, for the purpose of displaying names in human-readable form,
> the names might undergo some further processing, so A.b is actually
> treated as the name b in the namespace A, and A\.b is treated as the
> name A\.b in the global namespace, and as a result "show" tags might
> transform them differently.
>
> In my eyes an import tool falls into the "automatic tools" category,
> so I don't think you need to worry about the human readability angle.
>
> Does that help?
>
> Cheers,
>
> Joe
>
> _______________________________________________
> opentheory-users mailing list
> opentheory-users at gilith.com
> http://www.gilith.com/opentheory/mailing-list
>