# HG changeset patch # User paulson # Date 1554997795 -3600 # Node ID 538d9854ca2f721834237bd10352e892677f28bd # Parent af4f723823d82c2acc6b0b128a2c7835c978b751# Parent e0ac5e71a964e5d478ad6350563d87df7f871838 merged diff -r e0ac5e71a964 -r 538d9854ca2f NEWS --- a/NEWS Thu Apr 11 15:26:19 2019 +0100 +++ b/NEWS Thu Apr 11 16:49:55 2019 +0100 @@ -126,6 +126,17 @@ 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". + +* Many document antiquotations are internally categorized as "embedded" +and expect one cartouche argument, which is typically used with the +\<^control>\cartouche\ notation (e.g. \<^term>\\x y. x\). 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] \\x y. x\}. + *** Isar *** diff -r e0ac5e71a964 -r 538d9854ca2f etc/options --- a/etc/options Thu Apr 11 15:26:19 2019 +0100 +++ b/etc/options Thu Apr 11 16:49:55 2019 +0100 @@ -18,14 +18,18 @@ -- "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 -- "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 e0ac5e71a964 -r 538d9854ca2f src/Doc/Isar_Ref/Document_Preparation.thy --- a/src/Doc/Isar_Ref/Document_Preparation.thy Thu Apr 11 15:26:19 2019 +0100 +++ b/src/Doc/Isar_Ref/Document_Preparation.thy Thu Apr 11 16:49:55 2019 +0100 @@ -387,8 +387,13 @@ \<^descr> @{antiquotation_option_def break}~\= bool\ controls line breaks in non-display material. + \<^descr> @{antiquotation_option_def cartouche}~\= bool\ indicates if the output + should be delimited as cartouche. + \<^descr> @{antiquotation_option_def quotes}~\= bool\ 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}~\= name\ adds \name\ to the print mode to be used for presentation. Note that the standard setup for {\LaTeX} @@ -417,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, ``\name = true\'' may be abbreviated as ``\name\''. All of the above flags are disabled by default, unless changed specifically for a logic session in the corresponding \<^verbatim>\ROOT\ file. diff -r e0ac5e71a964 -r 538d9854ca2f src/Doc/antiquote_setup.ML --- a/src/Doc/antiquote_setup.ML Thu Apr 11 15:26:19 2019 +0100 +++ b/src/Doc/antiquote_setup.ML Thu Apr 11 16:49:55 2019 +0100 @@ -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 e0ac5e71a964 -r 538d9854ca2f src/Pure/Isar/keyword.scala --- a/src/Pure/Isar/keyword.scala Thu Apr 11 15:26:19 2019 +0100 +++ b/src/Pure/Isar/keyword.scala Thu Apr 11 16:49:55 2019 +0100 @@ -50,7 +50,7 @@ /* command categories */ - val vacous = Set(DIAG, DOCUMENT_HEADING, DOCUMENT_BODY, DOCUMENT_RAW) + val vacuous = Set(DIAG, DOCUMENT_HEADING, DOCUMENT_BODY, DOCUMENT_RAW) val diag = Set(DIAG) diff -r e0ac5e71a964 -r 538d9854ca2f src/Pure/Thy/document_antiquotation.ML --- a/src/Pure/Thy/document_antiquotation.ML Thu Apr 11 15:26:19 2019 +0100 +++ b/src/Pure/Thy/document_antiquotation.ML Thu Apr 11 16:49:55 2019 +0100 @@ -7,17 +7,19 @@ 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 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 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,10 +44,12 @@ 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>); 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>); @@ -69,8 +73,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 +86,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,11 +225,13 @@ setup_option \<^binding>\eta_contract\ (Config.put Syntax_Trans.eta_contract o boolean) #> setup_option \<^binding>\display\ (Config.put thy_output_display o boolean) #> setup_option \<^binding>\break\ (Config.put thy_output_break o boolean) #> + setup_option \<^binding>\cartouche\ (Config.put thy_output_cartouche o boolean) #> setup_option \<^binding>\quotes\ (Config.put thy_output_quotes o boolean) #> setup_option \<^binding>\mode\ (Config.put thy_output_modes) #> setup_option \<^binding>\margin\ (Config.put thy_output_margin o integer) #> setup_option \<^binding>\indent\ (Config.put thy_output_indent o integer) #> setup_option \<^binding>\source\ (Config.put thy_output_source o boolean) #> + setup_option \<^binding>\source_cartouche\ (Config.put thy_output_source_cartouche o boolean) #> setup_option \<^binding>\goals_limit\ (Config.put Goal_Display.goals_limit o integer)); end; diff -r e0ac5e71a964 -r 538d9854ca2f src/Pure/Thy/document_antiquotations.ML --- a/src/Pure/Thy/document_antiquotations.ML Thu Apr 11 15:26:19 2019 +0100 +++ b/src/Pure/Thy/document_antiquotations.ML Thu Apr 11 16:49:55 2019 +0100 @@ -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>\full_prf\ Attrib.thms (pretty_prf true) #> Document_Antiquotation.setup \<^binding>\thm\ (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 e0ac5e71a964 -r 538d9854ca2f src/Pure/Thy/thy_output.ML --- a/src/Pure/Thy/thy_output.ML Thu Apr 11 15:26:19 2019 +0100 +++ b/src/Pure/Thy/thy_output.ML Thu Apr 11 16:49:55 2019 +0100 @@ -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); diff -r e0ac5e71a964 -r 538d9854ca2f src/Tools/jEdit/src/jEdit.props --- a/src/Tools/jEdit/src/jEdit.props Thu Apr 11 15:26:19 2019 +0100 +++ b/src/Tools/jEdit/src/jEdit.props Thu Apr 11 16:49:55 2019 +0100 @@ -292,7 +292,6 @@ toggle-rect-select.shortcut2=A+NUMBER_SIGN twoStageSave=false vfs.browser.dock-position=left -vfs.browser.sortMixFilesAndDirs=true vfs.favorite.0.type=1 vfs.favorite.0=$ISABELLE_HOME vfs.favorite.1.type=1 diff -r e0ac5e71a964 -r 538d9854ca2f src/Tools/jEdit/src/syntax_style.scala --- a/src/Tools/jEdit/src/syntax_style.scala Thu Apr 11 15:26:19 2019 +0100 +++ b/src/Tools/jEdit/src/syntax_style.scala Thu Apr 11 16:49:55 2019 +0100 @@ -87,7 +87,7 @@ new_styles(hidden) = new SyntaxStyle(hidden_color, null, GUI.transform_font(new Font(font0.getFamily, 0, 1), - AffineTransform.getScaleInstance(1.0, font0.getSize.toDouble))) + AffineTransform.getScaleInstance(2.0, font0.getSize.toDouble))) new_styles(control) = new SyntaxStyle(style0.getForegroundColor, style0.getBackgroundColor, { val font_style =