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

definition backsl
where [simplified]:
  "backsl = ''This string contains a '' @ Char Nibble5 NibbleC #
  ''backslash''"

This is of course not a solution or explanation, just a workaround.

On 30/06/15 14:56, Lars Noschinski wrote:
 Hi everyone,

 I noticed that in HOL terms

    ''\091'' is the string ''[''
    ''\093'' is the string '']''

 but

    ''\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?


	Makarius





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.