added document antiquotation option "cartouche";
authorwenzelm
Thu Apr 11 15:44:06 2019 +0200 (5 months ago)
changeset 7012161e26527480e
parent 70120 45ca4006a37f
child 70122 a0b21b4b7a4a
added document antiquotation option "cartouche";
NEWS
etc/options
src/Doc/Isar_Ref/Document_Preparation.thy
src/Doc/antiquote_setup.ML
src/Pure/Thy/document_antiquotation.ML
     1.1 --- a/NEWS	Thu Apr 11 14:22:52 2019 +0200
     1.2 +++ b/NEWS	Thu Apr 11 15:44:06 2019 +0200
     1.3 @@ -126,6 +126,10 @@
     1.4  multiple markers are composed in canonical order, resulting in a
     1.5  reversed list of tags in the presentation context.
     1.6  
     1.7 +* Document antiquotation option "cartouche" indicates if the output
     1.8 +should be delimited as cartouche; this takes precedence over the
     1.9 +analogous option "quotes".
    1.10 +
    1.11  
    1.12  *** Isar ***
    1.13  
     2.1 --- a/etc/options	Thu Apr 11 14:22:52 2019 +0200
     2.2 +++ b/etc/options	Thu Apr 11 15:44:06 2019 +0200
     2.3 @@ -18,8 +18,10 @@
     2.4    -- "indicate output as multi-line display-style material"
     2.5  option thy_output_break : bool = false
     2.6    -- "control line breaks in non-display material"
     2.7 +option thy_output_cartouche : bool = false
     2.8 +  -- "indicate if the output should be delimited as cartouche"
     2.9  option thy_output_quotes : bool = false
    2.10 -  -- "indicate if the output should be enclosed in double quotes"
    2.11 +  -- "indicate if the output should be delimited via double quotes"
    2.12  option thy_output_margin : int = 76
    2.13    -- "right margin / page width for printing of display material"
    2.14  option thy_output_indent : int = 0
     3.1 --- a/src/Doc/Isar_Ref/Document_Preparation.thy	Thu Apr 11 14:22:52 2019 +0200
     3.2 +++ b/src/Doc/Isar_Ref/Document_Preparation.thy	Thu Apr 11 15:44:06 2019 +0200
     3.3 @@ -387,8 +387,13 @@
     3.4      \<^descr> @{antiquotation_option_def break}~\<open>= bool\<close> controls line breaks in
     3.5      non-display material.
     3.6  
     3.7 +    \<^descr> @{antiquotation_option_def cartouche}~\<open>= bool\<close> indicates if the output
     3.8 +    should be delimited as cartouche.
     3.9 +
    3.10      \<^descr> @{antiquotation_option_def quotes}~\<open>= bool\<close> indicates if the output
    3.11 -    should be enclosed in double quotes.
    3.12 +    should be delimited via double quotes (option @{antiquotation_option
    3.13 +    cartouche} takes precedence). Note that the Isabelle {\LaTeX} styles may
    3.14 +    suppress quotes on their own account.
    3.15  
    3.16      \<^descr> @{antiquotation_option_def mode}~\<open>= name\<close> adds \<open>name\<close> to the print mode
    3.17      to be used for presentation. Note that the standard setup for {\LaTeX}
     4.1 --- a/src/Doc/antiquote_setup.ML	Thu Apr 11 14:22:52 2019 +0200
     4.2 +++ b/src/Doc/antiquote_setup.ML	Thu Apr 11 15:44:06 2019 +0200
     4.3 @@ -126,7 +126,7 @@
     4.4        map (fn (thm, name) =>
     4.5          Output.output
     4.6            (Document_Antiquotation.format ctxt
     4.7 -            (Document_Antiquotation.quote ctxt (Thy_Output.pretty_thm ctxt thm))) ^
     4.8 +            (Document_Antiquotation.delimit ctxt (Thy_Output.pretty_thm ctxt thm))) ^
     4.9          enclose "\\rulename{" "}" (Output.output name))
    4.10        #> space_implode "\\par\\smallskip%\n"
    4.11        #> Latex.string #> single
     5.1 --- a/src/Pure/Thy/document_antiquotation.ML	Thu Apr 11 14:22:52 2019 +0200
     5.2 +++ b/src/Pure/Thy/document_antiquotation.ML	Thu Apr 11 15:44:06 2019 +0200
     5.3 @@ -7,6 +7,7 @@
     5.4  signature DOCUMENT_ANTIQUOTATION =
     5.5  sig
     5.6    val thy_output_display: bool Config.T
     5.7 +  val thy_output_cartouche: bool Config.T
     5.8    val thy_output_quotes: bool Config.T
     5.9    val thy_output_margin: int Config.T
    5.10    val thy_output_indent: int Config.T
    5.11 @@ -17,7 +18,7 @@
    5.12    val trim_lines: Proof.context -> string -> string
    5.13    val indent_lines: Proof.context -> string -> string
    5.14    val prepare_lines: Proof.context -> string -> string
    5.15 -  val quote: Proof.context -> Pretty.T -> Pretty.T
    5.16 +  val delimit: Proof.context -> Pretty.T -> Pretty.T
    5.17    val indent: Proof.context -> Pretty.T -> Pretty.T
    5.18    val format: Proof.context -> Pretty.T -> string
    5.19    val output: Proof.context -> Pretty.T -> Output.output
    5.20 @@ -42,6 +43,7 @@
    5.21  
    5.22  val thy_output_display = Attrib.setup_option_bool ("thy_output_display", \<^here>);
    5.23  val thy_output_break = Attrib.setup_option_bool ("thy_output_break", \<^here>);
    5.24 +val thy_output_cartouche = Attrib.setup_option_bool ("thy_output_cartouche", \<^here>);
    5.25  val thy_output_quotes = Attrib.setup_option_bool ("thy_output_quotes", \<^here>);
    5.26  val thy_output_margin = Attrib.setup_option_int ("thy_output_margin", \<^here>);
    5.27  val thy_output_indent = Attrib.setup_option_int ("thy_output_indent", \<^here>);
    5.28 @@ -69,8 +71,10 @@
    5.29  
    5.30  (* output *)
    5.31  
    5.32 -fun quote ctxt =
    5.33 -  Config.get ctxt thy_output_quotes ? Pretty.quote;
    5.34 +fun delimit ctxt =
    5.35 +  if Config.get ctxt thy_output_cartouche then Pretty.cartouche
    5.36 +  else if Config.get ctxt thy_output_quotes then Pretty.quote
    5.37 +  else I;
    5.38  
    5.39  fun indent ctxt =
    5.40    Config.get ctxt thy_output_display ? Pretty.indent (Config.get ctxt thy_output_indent);
    5.41 @@ -80,7 +84,7 @@
    5.42    then Pretty.string_of_margin (Config.get ctxt thy_output_margin)
    5.43    else Pretty.unformatted_string_of;
    5.44  
    5.45 -fun output ctxt = quote ctxt #> indent ctxt #> format ctxt #> Output.output;
    5.46 +fun output ctxt = delimit ctxt #> indent ctxt #> format ctxt #> Output.output;
    5.47  
    5.48  
    5.49  (* theory data *)
    5.50 @@ -219,6 +223,7 @@
    5.51    setup_option \<^binding>\<open>eta_contract\<close> (Config.put Syntax_Trans.eta_contract o boolean) #>
    5.52    setup_option \<^binding>\<open>display\<close> (Config.put thy_output_display o boolean) #>
    5.53    setup_option \<^binding>\<open>break\<close> (Config.put thy_output_break o boolean) #>
    5.54 +  setup_option \<^binding>\<open>cartouche\<close> (Config.put thy_output_cartouche o boolean) #>
    5.55    setup_option \<^binding>\<open>quotes\<close> (Config.put thy_output_quotes o boolean) #>
    5.56    setup_option \<^binding>\<open>mode\<close> (Config.put thy_output_modes) #>
    5.57    setup_option \<^binding>\<open>margin\<close> (Config.put thy_output_margin o integer) #>