# HG changeset patch
# User wenzelm
# Date 1554990246 -7200
# Node ID 61e26527480ea01b7409398404ecd3291c4e8b1a
# Parent  45ca4006a37fa2e560f75c4585c8c721929cae37
added document antiquotation option "cartouche";

diff -r 45ca4006a37f -r 61e26527480e NEWS
--- a/NEWS	Thu Apr 11 14:22:52 2019 +0200
+++ b/NEWS	Thu Apr 11 15:44:06 2019 +0200
@@ -126,6 +126,10 @@
 multiple markers are composed in canonical order, resulting in a
 reversed list of tags in the presentation context.
 
+* Document antiquotation option "cartouche" indicates if the output
+should be delimited as cartouche; this takes precedence over the
+analogous option "quotes".
+
 
 *** Isar ***
 
diff -r 45ca4006a37f -r 61e26527480e etc/options
--- a/etc/options	Thu Apr 11 14:22:52 2019 +0200
+++ b/etc/options	Thu Apr 11 15:44:06 2019 +0200
@@ -18,8 +18,10 @@
   -- "indicate output as multi-line display-style material"
 option thy_output_break : bool = false
   -- "control line breaks in non-display material"
+option thy_output_cartouche : bool = false
+  -- "indicate if the output should be delimited as cartouche"
 option thy_output_quotes : bool = false
-  -- "indicate if the output should be enclosed in double quotes"
+  -- "indicate if the output should be delimited via double quotes"
 option thy_output_margin : int = 76
   -- "right margin / page width for printing of display material"
 option thy_output_indent : int = 0
diff -r 45ca4006a37f -r 61e26527480e src/Doc/Isar_Ref/Document_Preparation.thy
--- a/src/Doc/Isar_Ref/Document_Preparation.thy	Thu Apr 11 14:22:52 2019 +0200
+++ b/src/Doc/Isar_Ref/Document_Preparation.thy	Thu Apr 11 15:44:06 2019 +0200
@@ -387,8 +387,13 @@
     \<^descr> @{antiquotation_option_def break}~\<open>= bool\<close> controls line breaks in
     non-display material.
 
+    \<^descr> @{antiquotation_option_def cartouche}~\<open>= bool\<close> indicates if the output
+    should be delimited as cartouche.
+
     \<^descr> @{antiquotation_option_def quotes}~\<open>= bool\<close> indicates if the output
-    should be enclosed in double quotes.
+    should be delimited via double quotes (option @{antiquotation_option
+    cartouche} takes precedence). Note that the Isabelle {\LaTeX} styles may
+    suppress quotes on their own account.
 
     \<^descr> @{antiquotation_option_def mode}~\<open>= name\<close> adds \<open>name\<close> to the print mode
     to be used for presentation. Note that the standard setup for {\LaTeX}
diff -r 45ca4006a37f -r 61e26527480e src/Doc/antiquote_setup.ML
--- a/src/Doc/antiquote_setup.ML	Thu Apr 11 14:22:52 2019 +0200
+++ b/src/Doc/antiquote_setup.ML	Thu Apr 11 15:44:06 2019 +0200
@@ -126,7 +126,7 @@
       map (fn (thm, name) =>
         Output.output
           (Document_Antiquotation.format ctxt
-            (Document_Antiquotation.quote ctxt (Thy_Output.pretty_thm ctxt thm))) ^
+            (Document_Antiquotation.delimit ctxt (Thy_Output.pretty_thm ctxt thm))) ^
         enclose "\\rulename{" "}" (Output.output name))
       #> space_implode "\\par\\smallskip%\n"
       #> Latex.string #> single
diff -r 45ca4006a37f -r 61e26527480e src/Pure/Thy/document_antiquotation.ML
--- a/src/Pure/Thy/document_antiquotation.ML	Thu Apr 11 14:22:52 2019 +0200
+++ b/src/Pure/Thy/document_antiquotation.ML	Thu Apr 11 15:44:06 2019 +0200
@@ -7,6 +7,7 @@
 signature DOCUMENT_ANTIQUOTATION =
 sig
   val thy_output_display: bool Config.T
+  val thy_output_cartouche: bool Config.T
   val thy_output_quotes: bool Config.T
   val thy_output_margin: int Config.T
   val thy_output_indent: int Config.T
@@ -17,7 +18,7 @@
   val trim_lines: Proof.context -> string -> string
   val indent_lines: Proof.context -> string -> string
   val prepare_lines: Proof.context -> string -> string
-  val quote: Proof.context -> Pretty.T -> Pretty.T
+  val delimit: Proof.context -> Pretty.T -> Pretty.T
   val indent: Proof.context -> Pretty.T -> Pretty.T
   val format: Proof.context -> Pretty.T -> string
   val output: Proof.context -> Pretty.T -> Output.output
@@ -42,6 +43,7 @@
 
 val thy_output_display = Attrib.setup_option_bool ("thy_output_display", \<^here>);
 val thy_output_break = Attrib.setup_option_bool ("thy_output_break", \<^here>);
+val thy_output_cartouche = Attrib.setup_option_bool ("thy_output_cartouche", \<^here>);
 val thy_output_quotes = Attrib.setup_option_bool ("thy_output_quotes", \<^here>);
 val thy_output_margin = Attrib.setup_option_int ("thy_output_margin", \<^here>);
 val thy_output_indent = Attrib.setup_option_int ("thy_output_indent", \<^here>);
@@ -69,8 +71,10 @@
 
 (* output *)
 
-fun quote ctxt =
-  Config.get ctxt thy_output_quotes ? Pretty.quote;
+fun delimit ctxt =
+  if Config.get ctxt thy_output_cartouche then Pretty.cartouche
+  else if Config.get ctxt thy_output_quotes then Pretty.quote
+  else I;
 
 fun indent ctxt =
   Config.get ctxt thy_output_display ? Pretty.indent (Config.get ctxt thy_output_indent);
@@ -80,7 +84,7 @@
   then Pretty.string_of_margin (Config.get ctxt thy_output_margin)
   else Pretty.unformatted_string_of;
 
-fun output ctxt = quote ctxt #> indent ctxt #> format ctxt #> Output.output;
+fun output ctxt = delimit ctxt #> indent ctxt #> format ctxt #> Output.output;
 
 
 (* theory data *)
@@ -219,6 +223,7 @@
   setup_option \<^binding>\<open>eta_contract\<close> (Config.put Syntax_Trans.eta_contract o boolean) #>
   setup_option \<^binding>\<open>display\<close> (Config.put thy_output_display o boolean) #>
   setup_option \<^binding>\<open>break\<close> (Config.put thy_output_break o boolean) #>
+  setup_option \<^binding>\<open>cartouche\<close> (Config.put thy_output_cartouche o boolean) #>
   setup_option \<^binding>\<open>quotes\<close> (Config.put thy_output_quotes o boolean) #>
   setup_option \<^binding>\<open>mode\<close> (Config.put thy_output_modes) #>
   setup_option \<^binding>\<open>margin\<close> (Config.put thy_output_margin o integer) #>