dismantle print_mode operations for Markup/Pretty: hardwired check of "print_mode_active Print_Mode.PIDE";

--- 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");
 

--- 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;

--- 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;
 

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

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