# HG changeset patch # User wenzelm # Date 1726082715 -7200 # Node ID 9de19e3a723155b313ed5d9bdecab8894f0f4037 # Parent 64dc09f7f189927ed32f9e01e232c00900b3eb53 dismantle print_mode operations for Markup/Pretty: hardwired check of "print_mode_active Print_Mode.PIDE"; diff -r 64dc09f7f189 -r 9de19e3a7231 src/Pure/General/pretty.ML --- a/src/Pure/General/pretty.ML Wed Sep 11 20:45:17 2024 +0200 +++ b/src/Pure/General/pretty.ML Wed Sep 11 21:25:15 2024 +0200 @@ -20,15 +20,6 @@ signature PRETTY = sig - type ops = - {symbolic: bool, - markup: Markup.output -> Markup.output, - indent: string -> int -> Output.output}; - val pure_ops: ops - val markup_ops: ops - val symbolic_ops: ops - val add_mode: string -> ops -> unit - val get_mode: unit -> ops type T val to_ML: T -> ML_Pretty.pretty val from_ML: ML_Pretty.pretty -> T @@ -98,34 +89,6 @@ structure Pretty: PRETTY = struct -(** print mode operations **) - -type ops = - {symbolic: bool, - markup: Markup.output -> Markup.output, - indent: string -> int -> string}; - -fun default_indent (_: string) = Symbol.spaces; - -val pure_ops: ops = {symbolic = false, markup = K Markup.no_output, indent = default_indent}; -val markup_ops: ops = {symbolic = false, markup = I, indent = default_indent}; -val symbolic_ops: ops = {symbolic = true, markup = I, indent = default_indent}; - -local - val modes = Synchronized.var "Pretty.modes" (Symtab.make [("", pure_ops)]); -in - fun add_mode name ops = - Synchronized.change modes (fn tab => - (if not (Symtab.defined tab name) then () - else warning ("Redefining pretty mode " ^ quote name); - Symtab.update (name, ops) tab)); - fun get_mode () = - the_default pure_ops - (Library.get_first (Symtab.lookup (Synchronized.value modes)) (print_mode_value ())); -end; - - - (** Pretty.T **) (* abstype: ML_Pretty.pretty without (op =) *) @@ -234,7 +197,7 @@ (** formatting **) -(* output operations: default via print_mode *) +(* output operations *) type output_ops = {symbolic: bool, @@ -243,17 +206,21 @@ indent: string -> int -> Output.output, margin: int}; -fun make_output_ops ({symbolic, markup, indent}: ops) opt_margin : output_ops = +fun make_output_ops {symbolic, markup} opt_margin : output_ops = {symbolic = symbolic, output = fn s => (s, size s), markup = markup, - indent = indent, + indent = fn _ => Symbol.spaces, margin = ML_Pretty.get_margin opt_margin}; -fun output_ops opt_margin = make_output_ops (get_mode ()) opt_margin; -val pure_output_ops = make_output_ops pure_ops; -val markup_output_ops = make_output_ops markup_ops; -val symbolic_output_ops = make_output_ops symbolic_ops NONE; +val pure_output_ops = make_output_ops {symbolic = false, markup = K Markup.no_output}; +val markup_output_ops = make_output_ops {symbolic = false, markup = I}; +val symbolic_output_ops = make_output_ops {symbolic = true, markup = I} NONE; + +(*default via print_mode*) +fun output_ops opt_margin = + if print_mode_active Print_Mode.PIDE then symbolic_output_ops + else pure_output_ops opt_margin; fun output_newline (ops: output_ops) = #1 (#output ops "\n"); diff -r 64dc09f7f189 -r 9de19e3a7231 src/Pure/General/print_mode.ML --- a/src/Pure/General/print_mode.ML Wed Sep 11 20:45:17 2024 +0200 +++ b/src/Pure/General/print_mode.ML Wed Sep 11 21:25:15 2024 +0200 @@ -18,8 +18,9 @@ sig include BASIC_PRINT_MODE val input: string + val internal: string val ASCII: string - val internal: string + val PIDE: string val setmp: string list -> ('a -> 'b) -> 'a -> 'b val with_modes: string list -> ('a -> 'b) -> 'a -> 'b val closure: ('a -> 'b) -> 'a -> 'b @@ -30,8 +31,9 @@ struct val input = "input"; +val internal = "internal"; val ASCII = "ASCII"; -val internal = "internal"; +val PIDE = "PIDE"; val print_mode = Unsynchronized.ref ([]: string list); val print_mode_var = Thread_Data.var () : string list Thread_Data.var; diff -r 64dc09f7f189 -r 9de19e3a7231 src/Pure/PIDE/markup.ML --- a/src/Pure/PIDE/markup.ML Wed Sep 11 20:45:17 2024 +0200 +++ b/src/Pure/PIDE/markup.ML Wed Sep 11 21:25:15 2024 +0200 @@ -279,10 +279,7 @@ val code_presentationN: string val stmt_nameN: string type output = Output.output * Output.output - type ops = {output: T -> output} val no_output: output - val add_mode: string -> ops -> unit - val get_mode: unit -> ops val output: T -> output val markup: T -> string -> string val markups: T list -> string -> string @@ -847,30 +844,15 @@ -(** print mode operations **) +(** output depending on print_mode **) type output = Output.output * Output.output; -type ops = {output: T -> output}; - -val default_ops: ops = {output = Output_Primitives.markup_fn}; - val no_output = ("", ""); -local - val modes = Synchronized.var "Markup.modes" (Symtab.make [("", default_ops)]); -in - fun add_mode name ops = - Synchronized.change modes (fn tab => - (if not (Symtab.defined tab name) then () - else Output.warning ("Redefining markup mode " ^ quote name); - Symtab.update (name, ops) tab)); - fun get_mode () = - the_default default_ops - (Library.get_first (Symtab.lookup (Synchronized.value modes)) (print_mode_value ())); -end; - -fun output m = if is_empty m then no_output else #output (get_mode ()) m; +fun output m = + if not (is_empty m) andalso print_mode_active Print_Mode.PIDE + then YXML.output_markup m else no_output; fun markup m = output m |-> Library.enclose; diff -r 64dc09f7f189 -r 9de19e3a7231 src/Pure/PIDE/yxml.ML --- a/src/Pure/PIDE/yxml.ML Wed Sep 11 20:45:17 2024 +0200 +++ b/src/Pure/PIDE/yxml.ML Wed Sep 11 21:25:15 2024 +0200 @@ -27,7 +27,6 @@ val write_body: Path.T -> XML.body -> unit val output_markup_only: Markup.T -> string val output_markup_elem: Markup.T -> (string * string) * string - val markup_ops: Markup.ops val parse_body: string -> XML.body val parse_body_bytes: Bytes.T -> XML.body val parse: string -> XML.tree @@ -85,8 +84,6 @@ let val [bg1, bg2, en] = space_explode Z (string_of (XML.wrap_elem ((markup, Z_text), Z_text))) in ((bg1, bg2), en) end; -val markup_ops: Markup.ops = {output = output_markup}; - (** efficient YXML parsing **) diff -r 64dc09f7f189 -r 9de19e3a7231 src/Pure/System/isabelle_process.ML --- a/src/Pure/System/isabelle_process.ML Wed Sep 11 20:45:17 2024 +0200 +++ b/src/Pure/System/isabelle_process.ML Wed Sep 11 21:25:15 2024 +0200 @@ -6,7 +6,6 @@ signature ISABELLE_PROCESS = sig - val is_active: unit -> bool val reset_tracing: Document_ID.exec -> unit val crashes: exn list Synchronized.var val init_options: unit -> unit @@ -18,17 +17,10 @@ structure Isabelle_Process: ISABELLE_PROCESS = struct -(* print mode *) - -val isabelle_processN = "isabelle_process"; - -fun is_active () = Print_Mode.print_mode_active isabelle_processN; - -val _ = Markup.add_mode isabelle_processN YXML.markup_ops; -val _ = Pretty.add_mode isabelle_processN Pretty.symbolic_ops; +(* print modes *) val protocol_modes1 = [Syntax_Trans.no_bracketsN, Syntax_Trans.no_type_bracketsN]; -val protocol_modes2 = [isabelle_processN]; +val protocol_modes2 = [Print_Mode.PIDE]; (* restricted tracing messages *)