# HG changeset patch # User wenzelm # Date 1725991065 -7200 # Node ID 9ed32b8a03a962ab025e5e5441b54069e97db136 # Parent da20e00050abb9b18a45615cb8ece5533b0e7e09 clarified print mode "latex": no longer impact Output/Markup/Pretty operations; renamed Output.output to Output.output_; removed Output.escape; diff -r da20e00050ab -r 9ed32b8a03a9 NEWS --- a/NEWS Tue Sep 10 16:06:38 2024 +0200 +++ b/NEWS Tue Sep 10 19:57:45 2024 +0200 @@ -91,6 +91,26 @@ variants), while the underlying Pretty.output operation supports an explicit Pretty.output_ops argument for alternative applications. +* The print_mode "latex" only affects inner syntax variants, while its +impact on Output/Markup/Pretty operations has been removed. Instead, +there are explicit operations Latex.output_, Latex.escape, and +Latex.output_ops. Output.output has been renamed to Output.output_ to +indicate statically where Isabelle/ML implementations may have to be +changed. Rare INCOMPATIBILITY for ambitious document antiquotations that +generate LaTeX source on their own account, instead of using regular +Pretty.T interfaces. The following operations need to be adjusted as +follows: + + Output.output + becomes Output.output_ or Latex.output_ + Output.escape + is omitted or becomes Latex.escape + Pretty.string_of with implicit "latex" print_mode + becomes Pretty.string_of_ops with explicit Latex.output_ops + +Note that basic Markup.markup cannot be used for Latex output: proper +Pretty.T operations are required (e.g. Pretty.mark_str). + *** System *** diff -r da20e00050ab -r 9ed32b8a03a9 src/Doc/antiquote_setup.ML --- a/src/Doc/antiquote_setup.ML Tue Sep 10 16:06:38 2024 +0200 +++ b/src/Doc/antiquote_setup.ML Tue Sep 10 19:57:45 2024 +0200 @@ -40,10 +40,10 @@ (Scan.repeat (Attrib.thm -- Scan.lift (Args.parens Args.name))) (fn ctxt => map (fn (thm, name) => - Output.output + Latex.output_ (Document_Antiquotation.format ctxt (Document_Antiquotation.delimit ctxt (Document_Output.pretty_thm ctxt thm))) ^ - enclose "\\rulename{" "}" (Output.output name)) + enclose "\\rulename{" "}" (Latex.output_ name)) #> space_implode "\\par\\smallskip%\n" #> Latex.string #> Document_Output.isabelle ctxt)); @@ -87,7 +87,7 @@ if Context_Position.is_reported ctxt pos then ignore (check ctxt (name, pos)) else (); val latex = idx ^ - (Output.output name + (Latex.output_ name |> (if markup = "" then I else enclose ("\\" ^ markup ^ "{") "}") |> hyper o enclose "\\mbox{\\isa{" "}}"); in Latex.string latex end); diff -r da20e00050ab -r 9ed32b8a03a9 src/HOL/TPTP/TPTP_Proof_Reconstruction.thy --- a/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy Tue Sep 10 16:06:38 2024 +0200 +++ b/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy Tue Sep 10 19:57:45 2024 +0200 @@ -422,7 +422,7 @@ val thy = Proof_Context.theory_of ctxt fun term_to_string t = Print_Mode.with_modes [""] - (fn () => Output.output (Syntax.string_of_term ctxt t)) () + (fn () => Output.output_ (Syntax.string_of_term ctxt t)) () val ordered_instances = TPTP_Reconstruct.interpret_bindings prob_name thy ordered_binds [] |> map (snd #> term_to_string) diff -r da20e00050ab -r 9ed32b8a03a9 src/Pure/General/latex.ML --- a/src/Pure/General/latex.ML Tue Sep 10 16:06:38 2024 +0200 +++ b/src/Pure/General/latex.ML Tue Sep 10 19:57:45 2024 +0200 @@ -29,6 +29,10 @@ val index_entry: index_entry -> text val index_variants: (binding -> bool option -> 'a -> 'a) -> binding -> 'a -> 'a val latexN: string + val output_: string -> Output.output + val output_width: string -> Output.output * int + val escape: Output.output -> string + val output_ops: int option -> Pretty.output_ops end; structure Latex: LATEX = @@ -233,18 +237,23 @@ val latexN = "latex"; + +(* markup and formatting *) + +val output_ = output_symbols o Symbol.explode; + +fun output_width str = + let val syms = Symbol.explode str + in (output_symbols syms, length_symbols syms) end; + +val escape = enclose (Symbol.latex ^ Symbol.open_) Symbol.close; + local val command_markup = YXML.output_markup (Markup.latex_macro "isacommand"); val keyword_markup = YXML.output_markup (Markup.latex_macro "isakeyword"); val indent_markup = YXML.output_markup (Markup.latex_macro "isaindent"); -fun latex_output str = - let val syms = Symbol.explode str - in (output_symbols syms, length_symbols syms) end; - -fun latex_escape ss = Symbol.latex :: Symbol.open_ :: ss @ [Symbol.close]; - fun latex_markup (s, _: Properties.T) = if member (op =) [Markup.commandN, Markup.keyword1N, Markup.keyword3N] s then command_markup else if s = Markup.keyword2N then keyword_markup @@ -260,9 +269,11 @@ in -val _ = Output.add_mode latexN {output = latex_output, escape = latex_escape}; -val _ = Markup.add_mode latexN {output = latex_markup}; -val _ = Pretty.add_mode latexN {markup = latex_markup_output, indent = latex_indent}; +fun output_ops opt_margin : Pretty.output_ops = + {output = output_width, + markup = latex_markup_output, + indent = latex_indent, + margin = ML_Pretty.get_margin opt_margin}; end; diff -r da20e00050ab -r 9ed32b8a03a9 src/Pure/General/output.ML --- a/src/Pure/General/output.ML Tue Sep 10 16:06:38 2024 +0200 +++ b/src/Pure/General/output.ML Tue Sep 10 19:57:45 2024 +0200 @@ -16,13 +16,12 @@ sig include BASIC_OUTPUT type output = string - type ops = {output: string -> output * int, escape: output list -> string list} + type ops = {output: string -> output * int} val default_ops: ops val add_mode: string -> ops -> unit val get_mode: unit -> ops val output_width: string -> output * int - val output: string -> output - val escape: output list -> string list + val output_: string -> output val physical_stdout: output -> unit val physical_stderr: output -> unit val physical_writeln: output -> unit @@ -66,9 +65,9 @@ type output = string; (*raw system output*) -type ops = {output: string -> output * int, escape: output list -> string list}; +type ops = {output: string -> output * int}; -val default_ops: ops = {output = fn s => (s, size s), escape = I}; +val default_ops: ops = {output = fn s => (s, size s)}; local val modes = Synchronized.var "Output.modes" (Symtab.make [("", default_ops)]); @@ -82,9 +81,7 @@ end; fun output_width x = #output (get_mode ()) x; -val output = #1 o output_width; - -fun escape x = #escape (get_mode ()) x; +val output_ = #1 o output_width; @@ -140,19 +137,19 @@ val _ = if Thread_Data.is_virtual then () else init_channels (); -fun writelns ss = ! writeln_fn (map output ss); +fun writelns ss = ! writeln_fn (map output_ ss); fun writeln s = writelns [s]; -fun state s = ! state_fn [output s]; -fun information s = ! information_fn [output s]; -fun tracing s = ! tracing_fn [output s]; -fun warning s = ! warning_fn [output s]; -fun legacy_feature s = ! legacy_fn [output ("Legacy feature! " ^ s)]; -fun error_message' (i, s) = ! error_message_fn (i, [output s]); +fun state s = ! state_fn [output_ s]; +fun information s = ! information_fn [output_ s]; +fun tracing s = ! tracing_fn [output_ s]; +fun warning s = ! warning_fn [output_ s]; +fun legacy_feature s = ! legacy_fn [output_ ("Legacy feature! " ^ s)]; +fun error_message' (i, s) = ! error_message_fn (i, [output_ s]); fun error_message s = error_message' (serial (), s); -fun system_message s = ! system_message_fn [output s]; -fun status ss = ! status_fn (map output ss); -fun report ss = ! report_fn (map output ss); -fun result props ss = ! result_fn props (map output ss); +fun system_message s = ! system_message_fn [output_ s]; +fun status ss = ! status_fn (map output_ ss); +fun report ss = ! report_fn (map output_ ss); +fun result props ss = ! result_fn props (map output_ ss); fun protocol_message props body = ! protocol_message_fn props body; fun try_protocol_message props body = protocol_message props body handle Protocol_Message _ => (); diff -r da20e00050ab -r 9ed32b8a03a9 src/Pure/General/pretty.ML --- a/src/Pure/General/pretty.ML Tue Sep 10 16:06:38 2024 +0200 +++ b/src/Pure/General/pretty.ML Tue Sep 10 19:57:45 2024 +0200 @@ -68,7 +68,6 @@ val unbreakable: T -> T type output_ops = {output: string -> Output.output * int, - escape: Output.output list -> string list, markup: Markup.output -> Markup.output, indent: string -> int -> Output.output, margin: int} @@ -231,21 +230,19 @@ type output_ops = {output: string -> Output.output * int, - escape: Output.output list -> string list, markup: Markup.output -> Markup.output, indent: string -> int -> Output.output, margin: int}; fun output_ops opt_margin : output_ops = let - val {output, escape} = Output.get_mode (); + val {output} = Output.get_mode (); val {markup, indent} = get_mode (); val margin = ML_Pretty.get_margin opt_margin; - in {output = output, escape = escape, markup = markup, indent = indent, margin = margin} end; + in {output = output, markup = markup, indent = indent, margin = margin} end; fun markup_output_ops opt_margin : output_ops = {output = #output Output.default_ops, - escape = #escape Output.default_ops, markup = #markup markup_ops, indent = #indent markup_ops, margin = ML_Pretty.get_margin opt_margin}; @@ -454,8 +451,7 @@ in Buffer.build o out o output_tree ops false end; fun unformatted_string_of prt = - let val ops = output_ops NONE - in implode (#escape ops (Buffer.contents (unformatted ops prt))) end; + Buffer.content (unformatted (output_ops NONE) prt); (* output interfaces *) @@ -470,12 +466,12 @@ val output = Buffer.contents oo output_buffer; -fun string_of_ops ops = implode o #escape ops o output ops; +fun string_of_ops ops = implode o output ops; fun string_of prt = string_of_ops (output_ops NONE) prt; fun writeln prt = let val ops = output_ops NONE - in Output.writelns (#escape ops (output ops prt)) end; + in Output.writelns (output ops prt) end; (* chunks *) diff -r da20e00050ab -r 9ed32b8a03a9 src/Pure/ML/ml_compiler.ML --- a/src/Pure/ML/ml_compiler.ML Tue Sep 10 16:06:38 2024 +0200 +++ b/src/Pure/ML/ml_compiler.ML Tue Sep 10 19:57:45 2024 +0200 @@ -67,7 +67,7 @@ val xml = PolyML.NameSpace.Values.printType (types, depth, SOME name_space) |> Pretty.from_ML |> Pretty.string_of - |> Output.output |> YXML.parse_body; + |> Output.output_ |> YXML.parse_body; in cons (pos, fn () => Markup.ML_typing, fn () => YXML.string_of_body xml) end end; diff -r da20e00050ab -r 9ed32b8a03a9 src/Pure/PIDE/markup.ML --- a/src/Pure/PIDE/markup.ML Tue Sep 10 16:06:38 2024 +0200 +++ b/src/Pure/PIDE/markup.ML Tue Sep 10 19:57:45 2024 +0200 @@ -864,9 +864,7 @@ fun output m = if is_empty m then no_output else #output (get_mode ()) m; -fun markup m = - let val (bg, en) = output m |> apply2 (single #> Output.escape #> implode); - in Library.enclose bg en end; +fun markup m = output m |-> Library.enclose; val markups = fold_rev markup; diff -r da20e00050ab -r 9ed32b8a03a9 src/Pure/Thy/document_antiquotation.ML --- a/src/Pure/Thy/document_antiquotation.ML Tue Sep 10 16:06:38 2024 +0200 +++ b/src/Pure/Thy/document_antiquotation.ML Tue Sep 10 19:57:45 2024 +0200 @@ -85,10 +85,10 @@ fun format ctxt = let val breakable = Config.get ctxt thy_output_display orelse Config.get ctxt thy_output_break; - val ops = Pretty.output_ops (SOME (Config.get ctxt thy_output_margin)); - in not breakable ? Pretty.unbreakable #> Pretty.string_of_ops ops end; + val ops = Latex.output_ops (SOME (Config.get ctxt thy_output_margin)); + in not breakable ? Pretty.unbreakable #> Pretty.output ops #> implode #> Latex.escape end; -fun output ctxt = delimit ctxt #> indent ctxt #> format ctxt #> Output.output; +fun output ctxt = delimit ctxt #> indent ctxt #> format ctxt #> Latex.output_; (* theory data *) diff -r da20e00050ab -r 9ed32b8a03a9 src/Pure/Thy/document_antiquotations.ML --- a/src/Pure/Thy/document_antiquotations.ML Tue Sep 10 16:06:38 2024 +0200 +++ b/src/Pure/Thy/document_antiquotations.ML Tue Sep 10 19:57:45 2024 +0200 @@ -434,7 +434,7 @@ Document_Output.antiquotation_raw name (Scan.lift Args.name_position) (fn ctxt => fn (name, pos) => let val _ = check ctxt (name, pos) - in Latex.macro macro (Latex.string (Output.output name)) end); + in Latex.macro macro (Latex.string (Latex.output_ name)) end); val _ = Theory.setup diff -r da20e00050ab -r 9ed32b8a03a9 src/Pure/Tools/rail.ML --- a/src/Pure/Tools/rail.ML Tue Sep 10 16:06:38 2024 +0200 +++ b/src/Pure/Tools/rail.ML Tue Sep 10 19:57:45 2024 +0200 @@ -332,7 +332,7 @@ Antiquote.Antiq #> Document_Antiquotation.evaluate Latex.symbols ctxt; fun output_text b s = - Latex.string (Output.output s) + Latex.string (Latex.output_ s) |> b ? Latex.macro "isakeyword" |> Latex.macro "isa";