Re: [isabelle] CHAR ''\092''



Hi Makarius,

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 like

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.

Andreas


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

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.