--- 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 ***
--- 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
--- 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}
--- 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
--- 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) #>