# HG changeset patch
# User wenzelm
# Date 1554993782 -7200
# Node ID a0b21b4b7a4a0c1505f26472150f48cc71a606b4
# Parent  61e26527480ea01b7409398404ecd3291c4e8b1a
strip cartouches from arguments of "embedded" document antiquotations, corresponding to automated update via "isabelle update -u control_cartouches" -- e.g. relevant for documents with thy_output_source (e.g. doc "isar-ref", "jedit", "system");

diff -r 61e26527480e -r a0b21b4b7a4a NEWS
--- a/NEWS	Thu Apr 11 15:44:06 2019 +0200
+++ b/NEWS	Thu Apr 11 16:43:02 2019 +0200
@@ -130,6 +130,13 @@
 should be delimited as cartouche; this takes precedence over the
 analogous option "quotes".
 
+* Many document antiquotations are internally categorized as "embedded"
+and expect one cartouche argument, which is typically used with the
+\<^control>\<open>cartouche\<close> notation (e.g. \<^term>\<open>\<lambda>x y. x\<close>). The cartouche
+delimiters are stripped in output of the source (antiquotation option
+"source"), but it is possible to enforce delimiters via option
+"source_cartouche", e.g. @{term [source_cartouche] \<open>\<lambda>x y. x\<close>}.
+
 
 *** Isar ***
 
diff -r 61e26527480e -r a0b21b4b7a4a etc/options
--- a/etc/options	Thu Apr 11 15:44:06 2019 +0200
+++ b/etc/options	Thu Apr 11 16:43:02 2019 +0200
@@ -28,6 +28,8 @@
   -- "indentation for pretty printing of display material"
 option thy_output_source : bool = false
   -- "print original source text rather than internal representation"
+option thy_output_source_cartouche : bool = false
+  -- "print original source text rather than internal representation, preserve cartouches"
 option thy_output_modes : string = ""
   -- "additional print modes for document output (separated by commas)"
 
diff -r 61e26527480e -r a0b21b4b7a4a src/Doc/Isar_Ref/Document_Preparation.thy
--- a/src/Doc/Isar_Ref/Document_Preparation.thy	Thu Apr 11 15:44:06 2019 +0200
+++ b/src/Doc/Isar_Ref/Document_Preparation.thy	Thu Apr 11 16:43:02 2019 +0200
@@ -422,6 +422,13 @@
     printing of the given source text, with the desirable well-formedness
     check in the background, but without modification of the printed text.
 
+    Cartouche delimiters of the argument are stripped for antiquotations that
+    are internally categorized as ``embedded''.
+
+    \<^descr> @{antiquotation_option_def source_cartouche} is like
+    @{antiquotation_option source}, but cartouche delimiters are always
+    preserved in the output.
+
   For Boolean flags, ``\<open>name = true\<close>'' may be abbreviated as ``\<open>name\<close>''. All
   of the above flags are disabled by default, unless changed specifically for
   a logic session in the corresponding \<^verbatim>\<open>ROOT\<close> file.
diff -r 61e26527480e -r a0b21b4b7a4a src/Pure/Thy/document_antiquotation.ML
--- a/src/Pure/Thy/document_antiquotation.ML	Thu Apr 11 15:44:06 2019 +0200
+++ b/src/Pure/Thy/document_antiquotation.ML	Thu Apr 11 16:43:02 2019 +0200
@@ -12,6 +12,7 @@
   val thy_output_margin: int Config.T
   val thy_output_indent: int Config.T
   val thy_output_source: bool Config.T
+  val thy_output_source_cartouche: bool Config.T
   val thy_output_break: bool Config.T
   val thy_output_modes: string Config.T
   val trim_blanks: Proof.context -> string -> string
@@ -48,6 +49,7 @@
 val thy_output_margin = Attrib.setup_option_int ("thy_output_margin", \<^here>);
 val thy_output_indent = Attrib.setup_option_int ("thy_output_indent", \<^here>);
 val thy_output_source = Attrib.setup_option_bool ("thy_output_source", \<^here>);
+val thy_output_source_cartouche = Attrib.setup_option_bool ("thy_output_source_cartouche", \<^here>);
 val thy_output_modes = Attrib.setup_option_string ("thy_output_modes", \<^here>);
 
 
@@ -229,6 +231,7 @@
   setup_option \<^binding>\<open>margin\<close> (Config.put thy_output_margin o integer) #>
   setup_option \<^binding>\<open>indent\<close> (Config.put thy_output_indent o integer) #>
   setup_option \<^binding>\<open>source\<close> (Config.put thy_output_source o boolean) #>
+  setup_option \<^binding>\<open>source_cartouche\<close> (Config.put thy_output_source_cartouche o boolean) #>
   setup_option \<^binding>\<open>goals_limit\<close> (Config.put Goal_Display.goals_limit o integer));
 
 end;
diff -r 61e26527480e -r a0b21b4b7a4a src/Pure/Thy/document_antiquotations.ML
--- a/src/Pure/Thy/document_antiquotations.ML	Thu Apr 11 15:44:06 2019 +0200
+++ b/src/Pure/Thy/document_antiquotations.ML	Thu Apr 11 16:43:02 2019 +0200
@@ -67,7 +67,7 @@
 fun basic_entities name scan pretty =
   Document_Antiquotation.setup name scan
     (fn {context = ctxt, source = src, argument = xs} =>
-      Thy_Output.pretty_items_source ctxt src (map (pretty ctxt) xs));
+      Thy_Output.pretty_items_source ctxt {embedded = false} src (map (pretty ctxt) xs));
 
 in
 
@@ -87,7 +87,7 @@
   basic_entities \<^binding>\<open>full_prf\<close> Attrib.thms (pretty_prf true) #>
   Document_Antiquotation.setup \<^binding>\<open>thm\<close> (Term_Style.parse -- Attrib.thms)
     (fn {context = ctxt, source = src, argument = arg} =>
-      Thy_Output.pretty_items_source ctxt src (pretty_thms_style ctxt arg)));
+      Thy_Output.pretty_items_source ctxt {embedded = false} src (pretty_thms_style ctxt arg)));
 
 end;
 
@@ -240,7 +240,10 @@
         val _ = ctxt
           |> Proof.theorem NONE (K I) [[(prop, [])]]
           |> Proof.global_terminal_proof (m1, m2);
-      in Thy_Output.pretty_source ctxt [hd src, prop_tok] (Thy_Output.pretty_term ctxt prop) end));
+      in
+        Thy_Output.pretty_source ctxt {embedded = false}
+          [hd src, prop_tok] (Thy_Output.pretty_term ctxt prop)
+      end));
 
 
 (* verbatim text *)
diff -r 61e26527480e -r a0b21b4b7a4a src/Pure/Thy/thy_output.ML
--- a/src/Pure/Thy/thy_output.ML	Thu Apr 11 15:44:06 2019 +0200
+++ b/src/Pure/Thy/thy_output.ML	Thu Apr 11 16:43:02 2019 +0200
@@ -20,11 +20,12 @@
   val isabelle_typewriter: Proof.context -> Latex.text list -> Latex.text
   val typewriter: Proof.context -> string -> Latex.text
   val verbatim: Proof.context -> string -> Latex.text
-  val source: Proof.context -> Token.src -> Latex.text
+  val source: Proof.context -> {embedded: bool} -> Token.src -> Latex.text
   val pretty: Proof.context -> Pretty.T -> Latex.text
-  val pretty_source: Proof.context -> Token.src -> Pretty.T -> Latex.text
+  val pretty_source: Proof.context -> {embedded: bool} -> Token.src -> Pretty.T -> Latex.text
   val pretty_items: Proof.context -> Pretty.T list -> Latex.text
-  val pretty_items_source: Proof.context -> Token.src -> Pretty.T list -> Latex.text
+  val pretty_items_source: Proof.context -> {embedded: bool} -> Token.src ->
+    Pretty.T list -> Latex.text
   val antiquotation_pretty:
     binding -> 'a context_parser -> (Proof.context -> 'a -> Pretty.T) -> theory -> theory
   val antiquotation_pretty_embedded:
@@ -492,9 +493,19 @@
   then Document_Antiquotation.indent_lines ctxt #> typewriter ctxt
   else split_lines #> map (typewriter ctxt) #> lines #> Latex.block;
 
-fun source ctxt =
+fun token_source ctxt {embedded} tok =
+  if Token.is_kind Token.Cartouche tok andalso embedded andalso
+    not (Config.get ctxt Document_Antiquotation.thy_output_source_cartouche)
+  then Token.content_of tok
+  else Token.unparse tok;
+
+fun is_source ctxt =
+  Config.get ctxt Document_Antiquotation.thy_output_source orelse
+  Config.get ctxt Document_Antiquotation.thy_output_source_cartouche;
+
+fun source ctxt embedded =
   Token.args_of_src
-  #> map (Token.unparse #> Document_Antiquotation.prepare_lines ctxt)
+  #> map (token_source ctxt embedded #> Document_Antiquotation.prepare_lines ctxt)
   #> space_implode " "
   #> output_source ctxt
   #> isabelle ctxt;
@@ -502,16 +513,14 @@
 fun pretty ctxt =
   Document_Antiquotation.output ctxt #> Latex.string #> single #> isabelle ctxt;
 
-fun pretty_source ctxt src prt =
-  if Config.get ctxt Document_Antiquotation.thy_output_source
-  then source ctxt src else pretty ctxt prt;
+fun pretty_source ctxt embedded src prt =
+  if is_source ctxt then source ctxt embedded src else pretty ctxt prt;
 
 fun pretty_items ctxt =
   map (Document_Antiquotation.output ctxt #> Latex.string) #> items #> isabelle ctxt;
 
-fun pretty_items_source ctxt src prts =
-  if Config.get ctxt Document_Antiquotation.thy_output_source
-  then source ctxt src else pretty_items ctxt prts;
+fun pretty_items_source ctxt embedded src prts =
+  if is_source ctxt then source ctxt embedded src else pretty_items ctxt prts;
 
 
 (* antiquotation variants *)
@@ -528,7 +537,8 @@
 
 fun gen_antiquotation_pretty_source name embedded scan f =
   gen_setup name embedded scan
-    (fn {context = ctxt, source = src, argument = x} => pretty_source ctxt src (f ctxt x));
+    (fn {context = ctxt, source = src, argument = x} =>
+      pretty_source ctxt {embedded = embedded} src (f ctxt x));
 
 fun gen_antiquotation_raw name embedded scan f =
   gen_setup name embedded scan (fn {context = ctxt, argument = x, ...} => f ctxt x);