Re: [isabelle] CHAR ''\092''
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
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