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:

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

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: http://isabelle.in.tum.de/repos/isabelle/rev/760e21900b01

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 http://isabelle.in.tum.de/repos/isabelle/file/f1b257607981/NEWS#l85


	Makarius




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