Re: [isabelle] CHAR ''\092''
- To: Makarius <makarius at sketis.net>
- Subject: Re: [isabelle] CHAR ''\092''
- From: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>
- Date: Wed, 1 Jul 2015 10:57:34 +0200
- Cc: Lars Noschinski <noschinl at in.tum.de>, cl-isabelle-users at lists.cam.ac.uk
- In-reply-to: <alpine.LNX.firstname.lastname@example.org>
- References: <559291F3.email@example.com> <559298C9.firstname.lastname@example.org> <alpine.LNX.email@example.com>
- User-agent: Mozilla/5.0 (X11; Linux x86_64; rv:31.0) Gecko/20100101 Thunderbird/31.7.0
My usecase for \ inside string literals was related to code generation. I wanted to write
a generate a program with the code generator such that one of the functions returns a
string representation of the computed data, which should contain among others backslashes
(used for quoting other characters in that string). For example, I defined literal strings
definition lit_paren = STR [Char Nibble5 NibbleC, CHR ''('']
such that the code generator produces in ML
val lit_paren = "\(";
which can then be used in other parts.
On 30/06/15 17:31, Makarius wrote:
On Tue, 30 Jun 2015, Andreas Lochbihler wrote:
I remember having run into the same problem a while ago. At that time, I just used the
nibble notation, i.e., Char Nibble5 NibbleC as in
"backsl = ''This string contains a '' @ Char Nibble5 NibbleC #
This is of course not a solution or explanation, just a workaround.
On 30/06/15 14:56, Lars Noschinski wrote:
I noticed that in HOL terms
''\091'' is the string ''[''
''\093'' is the string '']''
''\092'' is not the backslash, but gives a syntax error.
I can't recall all reasons for this on the spot -- the full explanations would require
archeological digging of approx. 20 years of history.
Generally, there is a problem that an ASCII backslash is used for escaping in various
"text containers", e.g. double quoted strings of outer syntax. It also has a special
meaning for Isabelle symbol notation: \<foobar>
In distant past, we've had two (!) versions of Proof General -- one for the ML toplevel
one for the Isar toplevel -- with different quoting and escaping rules. In these dark
times the above special case was introduced.
Today we are no longer bound by any toplevel loop, and have just to deal with outer +
inner syntax of Isabelle.
When the question about \n in Isabelle/HOL strings came up some time ago, the escape hatch
was to introduce \<newline> for that. One could do the same for \<backslash> for example.
Overall, I am not sure. What are the concrete applications?
This archive was generated by a fusion of
Pipermail (Mailman edition) and