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
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