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


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.

If I'm covering info already covered, I apologize more than those who apologize for the possibility of sending out duplicate notices for calls for submissions.

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.

I include the example theory and outer syntax command below. A small image is attached showing the failure in the session run.


(******* THEORY *********)

theory i151113a
imports Complex_Main (*"$GEZ/m/IsE"*)
keywords "FOOBAR" :: diag
\<open>Outer_Syntax.command @{command_keyword "FOOBAR"}
  "(IsE) IMM general text/text tag"
(Parse.text -- Parse.text >> (fn _ => Toplevel.keep (fn _ => ())))\<close>

I.prog \<open>w,p\<close> \<open>\<open>f\<bar>ROOT\<close>\<close> \<open>
session "i151113a" (i151113a) = "HOL" +
  options [quick_and_dirty = true]

~I.prog \<open>bash.bash\<bar>w,ss,con0\<close> \<open>\<open>f\<bar>root_run.bash\<close>\<close> \<open>
root_run="isabelle build -v -d . -g i151113a"
printf "%s\n" "$ ${root_run}"

Attachment: 151113a_session_error_2_cartouche.png
Description: PNG image

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