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



Greetings,

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:

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.

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

Thanks,
GB

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

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

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

~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}"
${root_run}
\<close>
*)
end

Attachment: 151113a_session_error_2_cartouche.png
Description: PNG image



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