Re: [isabelle] Juxtaposed cartouche error in session run; okay in PIDE

On Fri, 13 Nov 2015, Gottfried Barrow wrote:

The previously stated suboptimal, non-response-non-feedback formality applies; a very scary formality under unknown circumstances, before the knowns become known; a formality not to be fully formally stated more than once every 6 months, or at least not twice within a week, even at the expense of being ambiguous.

Can you say this again in plain words?

This is just a report that I get an error for a session run that I don't get in the PIDE.

The following outer syntax command causes an error in the session run, but not in the PIDE:


If a space is put between the two commands '\<close>\<open>', then there is no error, or if quotes are used instead of cartouche delimiters.

Isabelle outer syntax is normally written with a bit more space, e.g. like this:

  FOOBAR \<open>test\<close> \<open>test\<close>

You are nonetheless right, that there is a mistake in the scanner for cartouches in Isabelle/ML, and it disagrees with the Isabelle/Scala version. I have changed that 3 weeks ago here:

Thus the coming winter release should work better in this respect. When the first release candiates are announced, you should definitely try them. There is a good chance that other improvements are in conflict with your way of writing Isabelle documents. See also


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