# HG changeset patch
# User wenzelm
# Date 1725550785 -7200
# Node ID 4a64fc4d1cde8dd7af1e2b113e4d216add5307db
# Parent  34906b3db920dd9d820ce546d9cee67183e598fb
clarified signature: type ML_Pretty.pretty coincides with PolyML.pretty;

diff -r 34906b3db920 -r 4a64fc4d1cde src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Wed Sep 04 16:21:52 2024 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Thu Sep 05 17:39:45 2024 +0200
@@ -165,7 +165,7 @@
    expect : string}
 
 fun string_of_params (params : params) =
-  YXML.content_of (ML_Pretty.string_of_polyml (ML_system_pretty (params, 100)))
+  YXML.content_of (ML_Pretty.string_of (ML_system_pretty (params, 100)))
 
 fun maybe_filter_out_induction_rules induction_rules : fact list -> fact list =
   induction_rules = Exclude ?
diff -r 34906b3db920 -r 4a64fc4d1cde src/Pure/Concurrent/future.ML
--- a/src/Pure/Concurrent/future.ML	Wed Sep 04 16:21:52 2024 +0200
+++ b/src/Pure/Concurrent/future.ML	Thu Sep 05 17:39:45 2024 +0200
@@ -111,8 +111,8 @@
 val _ =
   ML_system_pp (fn depth => fn pretty => fn x =>
     (case peek x of
-      NONE => PolyML.PrettyString "<future>"
-    | SOME (Exn.Exn _) => PolyML.PrettyString "<failed>"
+      NONE => ML_Pretty.str "<future>"
+    | SOME (Exn.Exn _) => ML_Pretty.str "<failed>"
     | SOME (Exn.Res y) => pretty (y, depth)));
 
 
diff -r 34906b3db920 -r 4a64fc4d1cde src/Pure/Concurrent/lazy.ML
--- a/src/Pure/Concurrent/lazy.ML	Wed Sep 04 16:21:52 2024 +0200
+++ b/src/Pure/Concurrent/lazy.ML	Thu Sep 05 17:39:45 2024 +0200
@@ -157,8 +157,8 @@
 val _ =
   ML_system_pp (fn depth => fn pretty => fn x =>
     (case peek x of
-      NONE => PolyML.PrettyString "<lazy>"
-    | SOME (Exn.Exn _) => PolyML.PrettyString "<failed>"
+      NONE => ML_Pretty.str "<lazy>"
+    | SOME (Exn.Exn _) => ML_Pretty.str "<failed>"
     | SOME (Exn.Res y) => pretty (y, depth)));
 
 end;
diff -r 34906b3db920 -r 4a64fc4d1cde src/Pure/Concurrent/task_queue.ML
--- a/src/Pure/Concurrent/task_queue.ML	Wed Sep 04 16:21:52 2024 +0200
+++ b/src/Pure/Concurrent/task_queue.ML	Thu Sep 05 17:39:45 2024 +0200
@@ -430,7 +430,7 @@
 
 (* toplevel pretty printing *)
 
-val _ = ML_system_pp (fn _ => fn _ => Pretty.to_polyml o Pretty.str o str_of_task);
-val _ = ML_system_pp (fn _ => fn _ => Pretty.to_polyml o Pretty.str o str_of_group);
+val _ = ML_system_pp (fn _ => fn _ => ML_Pretty.str o str_of_task);
+val _ = ML_system_pp (fn _ => fn _ => ML_Pretty.str o str_of_group);
 
 end;
diff -r 34906b3db920 -r 4a64fc4d1cde src/Pure/General/binding.ML
--- a/src/Pure/General/binding.ML	Wed Sep 04 16:21:52 2024 +0200
+++ b/src/Pure/General/binding.ML	Thu Sep 05 17:39:45 2024 +0200
@@ -178,7 +178,7 @@
 
 val print = Pretty.unformatted_string_of o pretty;
 
-val _ = ML_system_pp (fn _ => fn _ => Pretty.to_polyml o pretty o reset_pos);
+val _ = ML_system_pp (fn _ => fn _ => Pretty.to_ML o pretty o reset_pos);
 
 
 (* check *)
diff -r 34906b3db920 -r 4a64fc4d1cde src/Pure/General/bitset.ML
--- a/src/Pure/General/bitset.ML	Wed Sep 04 16:21:52 2024 +0200
+++ b/src/Pure/General/bitset.ML	Thu Sep 05 17:39:45 2024 +0200
@@ -215,8 +215,7 @@
 
 val _ =
   ML_system_pp (fn depth => fn _ => fn set =>
-    ML_Pretty.to_polyml
-      (ML_Pretty.enum "," "{" "}" (ML_Pretty.from_polyml o ML_system_pretty) (dest set, depth)));
+    ML_Pretty.enum "," "{" "}" ML_system_pretty (dest set, depth));
 
 
 (*final declarations of this structure!*)
diff -r 34906b3db920 -r 4a64fc4d1cde src/Pure/General/linear_set.ML
--- a/src/Pure/General/linear_set.ML	Wed Sep 04 16:21:52 2024 +0200
+++ b/src/Pure/General/linear_set.ML	Thu Sep 05 17:39:45 2024 +0200
@@ -137,12 +137,7 @@
 
 val _ =
   ML_system_pp (fn depth => fn pretty => fn set =>
-    ML_Pretty.to_polyml
-      (ML_Pretty.enum "," "{" "}"
-        (ML_Pretty.pair
-          (ML_Pretty.from_polyml o ML_system_pretty)
-          (ML_Pretty.from_polyml o pretty))
-        (dest set, depth)));
+    ML_Pretty.enum "," "{" "}" (ML_Pretty.pair ML_system_pretty pretty) (dest set, depth));
 
 end;
 
diff -r 34906b3db920 -r 4a64fc4d1cde src/Pure/General/pretty.ML
--- a/src/Pure/General/pretty.ML	Wed Sep 04 16:21:52 2024 +0200
+++ b/src/Pure/General/pretty.ML	Thu Sep 05 17:39:45 2024 +0200
@@ -78,10 +78,9 @@
   val block_enclose: T * T -> T list -> T
   val writeln_chunks: T list -> unit
   val writeln_chunks2: T list -> unit
-  val to_ML: FixedInt.int -> T -> ML_Pretty.pretty
+  val prune_ML: FixedInt.int -> T -> ML_Pretty.pretty
+  val to_ML: T -> ML_Pretty.pretty
   val from_ML: ML_Pretty.pretty -> T
-  val to_polyml: T -> PolyML.pretty
-  val from_polyml: PolyML.pretty -> T
 end;
 
 structure Pretty: PRETTY =
@@ -399,32 +398,48 @@
 
 (** toplevel pretty printing **)
 
-fun to_ML 0 (Block _) = ML_Pretty.str "..."
-  | to_ML depth (Block (m, consistent, indent, prts, _)) =
-      ML_Pretty.Block (m, consistent, FixedInt.fromInt indent, map (to_ML (depth - 1)) prts)
-  | to_ML _ (Break (force, wd, ind)) =
-      ML_Pretty.Break (force, FixedInt.fromInt wd, FixedInt.fromInt ind)
-  | to_ML _ (Str (s, len)) = ML_Pretty.String (s, FixedInt.fromInt len);
+val short_nat = FixedInt.fromInt o force_nat;
+val long_nat = force_nat o FixedInt.toInt;
 
-fun from_ML (ML_Pretty.Block (m, consistent, indent, prts)) =
-      make_block {markup = m, consistent = consistent, indent = FixedInt.toInt indent}
-        (map from_ML prts)
-  | from_ML (ML_Pretty.Break (force, wd, ind)) =
-      Break (force, FixedInt.toInt wd, FixedInt.toInt ind)
-  | from_ML (ML_Pretty.String (s, len)) = Str (s, force_nat (FixedInt.toInt len));
+fun prune_ML 0 (Block _) = ML_Pretty.str "..."
+  | prune_ML depth (Block ((bg, en), consistent, indent, prts, _)) =
+      let
+        val context =
+          (if bg = "" then [] else [ML_Pretty.ContextProperty ("begin", bg)]) @
+          (if en = "" then [] else [ML_Pretty.ContextProperty ("end", en)]);
+        val ind = short_nat indent;
+      in ML_Pretty.PrettyBlock (ind, consistent, context, map (prune_ML (depth - 1)) prts) end
+  | prune_ML _ (Break (true, _, _)) = ML_Pretty.PrettyLineBreak
+  | prune_ML _ (Break (false, wd, ind)) = ML_Pretty.PrettyBreak (short_nat wd, short_nat ind)
+  | prune_ML _ (Str (s, n)) =
+      if size s = n then ML_Pretty.PrettyString s
+      else ML_Pretty.PrettyStringWithWidth (s, short_nat n);
 
-val to_polyml = to_ML ~1 #> ML_Pretty.to_polyml;
-val from_polyml = ML_Pretty.from_polyml #> from_ML;
+val to_ML = prune_ML ~1;
+
+fun from_ML (ML_Pretty.PrettyBlock (ind, consistent, context, body)) =
+      let
+        fun prop name (ML_Pretty.ContextProperty (a, b)) = if name = a then SOME b else NONE
+          | prop _ _ = NONE;
+        fun property name = the_default "" (get_first (prop name) context);
+        val m = (property "begin", property "end");
+      in
+        make_block {markup = m, consistent = consistent, indent = long_nat ind} (map from_ML body)
+      end
+  | from_ML (ML_Pretty.PrettyBreak (wd, ind)) = Break (false, long_nat wd, long_nat ind)
+  | from_ML ML_Pretty.PrettyLineBreak = fbrk
+  | from_ML (ML_Pretty.PrettyString s) = str s
+  | from_ML (ML_Pretty.PrettyStringWithWidth (s, n)) = Str (s, long_nat n);
 
 end;
 
-val _ = ML_system_pp (fn d => fn _ => ML_Pretty.to_polyml o to_ML (d + 1) o quote);
-val _ = ML_system_pp (fn _ => fn _ => to_polyml o position);
+val _ = ML_system_pp (fn d => fn _ => prune_ML (d + 1) o quote);
+val _ = ML_system_pp (fn _ => fn _ => to_ML o position);
 
 end;
 
-structure ML_Pretty =
+structure ML_Pretty: ML_PRETTY =
 struct
   open ML_Pretty;
-  val string_of_polyml = Pretty.string_of o Pretty.from_polyml;
+  val string_of = Pretty.string_of o Pretty.from_ML;
 end;
diff -r 34906b3db920 -r 4a64fc4d1cde src/Pure/General/rat.ML
--- a/src/Pure/General/rat.ML	Wed Sep 04 16:21:52 2024 +0200
+++ b/src/Pure/General/rat.ML	Thu Sep 05 17:39:45 2024 +0200
@@ -104,4 +104,4 @@
 ML_system_overload Rat.neg "~";
 ML_system_overload Rat.abs "abs";
 
-ML_system_pp (fn _ => fn _ => fn x => Pretty.to_polyml (Pretty.str ("@" ^ Rat.string_of_rat x)));
+ML_system_pp (fn _ => fn _ => fn x => ML_Pretty.str ("@" ^ Rat.string_of_rat x));
diff -r 34906b3db920 -r 4a64fc4d1cde src/Pure/General/set.ML
--- a/src/Pure/General/set.ML	Wed Sep 04 16:21:52 2024 +0200
+++ b/src/Pure/General/set.ML	Thu Sep 05 17:39:45 2024 +0200
@@ -501,8 +501,7 @@
 
 val _ =
   ML_system_pp (fn depth => fn _ => fn set =>
-    ML_Pretty.to_polyml
-      (ML_Pretty.enum "," "{" "}" (ML_Pretty.from_polyml o ML_system_pretty) (dest set, depth)));
+    ML_Pretty.enum "," "{" "}" ML_system_pretty (dest set, depth));
 
 (*final declarations of this structure!*)
 val fold = fold_set;
diff -r 34906b3db920 -r 4a64fc4d1cde src/Pure/General/sha1.ML
--- a/src/Pure/General/sha1.ML	Wed Sep 04 16:21:52 2024 +0200
+++ b/src/Pure/General/sha1.ML	Thu Sep 05 17:39:45 2024 +0200
@@ -188,7 +188,7 @@
 fun rep (Digest s) = s;
 val fake = Digest;
 
-val _ = ML_system_pp (fn _ => fn _ => Pretty.to_polyml o Pretty.str o quote o rep);
+val _ = ML_system_pp (fn _ => fn _ => ML_Pretty.str o quote o rep);
 
 fun digest_string str = digest_string_external str
   handle Foreign.Foreign msg =>
diff -r 34906b3db920 -r 4a64fc4d1cde src/Pure/General/table.ML
--- a/src/Pure/General/table.ML	Wed Sep 04 16:21:52 2024 +0200
+++ b/src/Pure/General/table.ML	Thu Sep 05 17:39:45 2024 +0200
@@ -617,12 +617,7 @@
 
 val _ =
   ML_system_pp (fn depth => fn pretty => fn tab =>
-    ML_Pretty.to_polyml
-      (ML_Pretty.enum "," "{" "}"
-        (ML_Pretty.pair
-          (ML_Pretty.from_polyml o ML_system_pretty)
-          (ML_Pretty.from_polyml o pretty))
-        (dest tab, depth)));
+    ML_Pretty.enum "," "{" "}" (ML_Pretty.pair ML_system_pretty pretty) (dest tab, depth));
 
 
 (*final declarations of this structure!*)
diff -r 34906b3db920 -r 4a64fc4d1cde src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Wed Sep 04 16:21:52 2024 +0200
+++ b/src/Pure/Isar/proof.ML	Thu Sep 05 17:39:45 2024 +0200
@@ -180,8 +180,7 @@
       (context * thm list list -> context -> context)};
 
 val _ =
-  ML_system_pp (fn _ => fn _ => fn _: state =>
-    Pretty.to_polyml (Pretty.str "<Proof.state>"));
+  ML_system_pp (fn _ => fn _ => fn _: state => ML_Pretty.str "<Proof.state>");
 
 fun make_goal (statement, using, goal, before_qed, after_qed) =
   Goal {statement = statement, using = using, goal = goal,
diff -r 34906b3db920 -r 4a64fc4d1cde src/Pure/Isar/runtime.ML
--- a/src/Pure/Isar/runtime.ML	Wed Sep 04 16:21:52 2024 +0200
+++ b/src/Pure/Isar/runtime.ML	Thu Sep 05 17:39:45 2024 +0200
@@ -41,9 +41,7 @@
 (* pretty *)
 
 fun pretty_exn (exn: exn) =
-  Pretty.from_ML
-    (ML_Pretty.from_polyml
-      (ML_system_pretty (exn, FixedInt.fromInt (ML_Print_Depth.get_print_depth ()))));
+  Pretty.from_ML (ML_system_pretty (exn, FixedInt.fromInt (ML_Print_Depth.get_print_depth ())));
 
 
 (* exn_context *)
diff -r 34906b3db920 -r 4a64fc4d1cde src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Wed Sep 04 16:21:52 2024 +0200
+++ b/src/Pure/Isar/toplevel.ML	Thu Sep 05 17:39:45 2024 +0200
@@ -247,7 +247,7 @@
 
 fun pretty_abstract state = Pretty.str ("<Isar " ^ str_of_state state ^ ">");
 
-val _ = ML_system_pp (fn _ => fn _ => Pretty.to_polyml o pretty_abstract);
+val _ = ML_system_pp (fn _ => fn _ => Pretty.to_ML o pretty_abstract);
 
 
 
diff -r 34906b3db920 -r 4a64fc4d1cde src/Pure/ML/ml_compiler.ML
--- a/src/Pure/ML/ml_compiler.ML	Wed Sep 04 16:21:52 2024 +0200
+++ b/src/Pure/ML/ml_compiler.ML	Thu Sep 05 17:39:45 2024 +0200
@@ -66,7 +66,7 @@
           let
             val xml =
               PolyML.NameSpace.Values.printType (types, depth, SOME name_space)
-              |> Pretty.from_polyml |> Pretty.string_of
+              |> Pretty.from_ML |> Pretty.string_of
               |> Output.output |> YXML.parse_body;
           in cons (pos, fn () => Markup.ML_typing, fn () => YXML.string_of_body xml) end
       end;
@@ -215,7 +215,7 @@
     fun message {message = msg, hard, location = loc, context = _} =
       let
         val pos = Exn_Properties.position_of_polyml_location loc;
-        val s = Pretty.string_of (Pretty.from_polyml msg);
+        val s = Pretty.string_of (Pretty.from_ML msg);
         val catch_all =
           #catch_all flags orelse
             (case opt_context of
@@ -237,7 +237,7 @@
       let
         fun display disp x =
           if depth > 0 then
-            (write (disp x |> Pretty.from_polyml |> Pretty.string_of); write "\n")
+            (write (disp x |> Pretty.from_ML |> Pretty.string_of); write "\n")
           else ();
 
         fun apply_fix (a, b) =
diff -r 34906b3db920 -r 4a64fc4d1cde src/Pure/ML/ml_pp.ML
--- a/src/Pure/ML/ml_pp.ML	Wed Sep 04 16:21:52 2024 +0200
+++ b/src/Pure/ML/ml_pp.ML	Thu Sep 05 17:39:45 2024 +0200
@@ -9,40 +9,35 @@
 
 val _ =
   ML_system_pp (fn _ => fn _ => fn bytes =>
-    PolyML.PrettyString
+    ML_Pretty.str
      (if Bytes.is_empty bytes then "Bytes.empty"
       else "Bytes {size = " ^ string_of_int (Bytes.size bytes) ^ "}"));
 
 val _ =
-  ML_system_pp (fn _ => fn _ => Pretty.to_polyml o Pretty.mark_str o Path.print_markup);
+  ML_system_pp (fn _ => fn _ => Pretty.to_ML o Pretty.mark_str o Path.print_markup);
 
 val _ =
   ML_system_pp (fn _ => fn _ => fn t =>
-    PolyML.PrettyString ("<thread " ^ quote (Isabelle_Thread.print t) ^
+    ML_Pretty.str ("<thread " ^ quote (Isabelle_Thread.print t) ^
       (if Isabelle_Thread.is_active t then "" else " (inactive)") ^ ">"));
 
 val _ =
-  ML_system_pp (fn _ => fn _ => Pretty.to_polyml o Proof_Display.pp_context);
+  ML_system_pp (fn _ => fn _ => Pretty.to_ML o Proof_Display.pp_context);
 
 val _ =
-  ML_system_pp (fn depth => fn _ =>
-    ML_Pretty.to_polyml o Pretty.to_ML depth o Proof_Display.pp_thm);
-
-val _ =
-  ML_system_pp (fn depth => fn _ =>
-    ML_Pretty.to_polyml o Pretty.to_ML depth o Proof_Display.pp_cterm);
+  ML_system_pp (fn depth => fn _ => Pretty.prune_ML depth o Proof_Display.pp_thm);
 
 val _ =
-  ML_system_pp (fn depth => fn _ =>
-    ML_Pretty.to_polyml o Pretty.to_ML depth o Proof_Display.pp_ctyp);
+  ML_system_pp (fn depth => fn _ => Pretty.prune_ML depth o Proof_Display.pp_cterm);
 
 val _ =
-  ML_system_pp (fn depth => fn _ =>
-    ML_Pretty.to_polyml o Pretty.to_ML depth o Proof_Display.pp_typ);
+  ML_system_pp (fn depth => fn _ => Pretty.prune_ML depth o Proof_Display.pp_ctyp);
 
 val _ =
-  ML_system_pp (fn depth => fn _ =>
-    ML_Pretty.to_polyml o Pretty.to_ML depth o Proof_Display.pp_ztyp);
+  ML_system_pp (fn depth => fn _ => Pretty.prune_ML depth o Proof_Display.pp_typ);
+
+val _ =
+  ML_system_pp (fn depth => fn _ => Pretty.prune_ML depth o Proof_Display.pp_ztyp);
 
 
 local
@@ -61,17 +56,17 @@
         |> (if parens then Pretty.enclose "(" ")" else Pretty.block)
     | Abs (a, T, b) =>
         prt_apps "Abs"
-         [Pretty.from_polyml (ML_system_pretty (a, dp - 1)),
-          Pretty.from_polyml (ML_system_pretty (T, dp - 2)),
+         [Pretty.from_ML (ML_system_pretty (a, dp - 1)),
+          Pretty.from_ML (ML_system_pretty (T, dp - 2)),
           prt_term false (dp - 3) b]
-    | Const a => prt_app "Const" (Pretty.from_polyml (ML_system_pretty (a, dp - 1)))
-    | Free a => prt_app "Free" (Pretty.from_polyml (ML_system_pretty (a, dp - 1)))
-    | Var a => prt_app "Var" (Pretty.from_polyml (ML_system_pretty (a, dp - 1)))
-    | Bound a => prt_app "Bound" (Pretty.from_polyml (ML_system_pretty (a, dp - 1))));
+    | Const a => prt_app "Const" (Pretty.from_ML (ML_system_pretty (a, dp - 1)))
+    | Free a => prt_app "Free" (Pretty.from_ML (ML_system_pretty (a, dp - 1)))
+    | Var a => prt_app "Var" (Pretty.from_ML (ML_system_pretty (a, dp - 1)))
+    | Bound a => prt_app "Bound" (Pretty.from_ML (ML_system_pretty (a, dp - 1))));
 
 in
 
-val _ = ML_system_pp (fn depth => fn _ => Pretty.to_polyml o prt_term false depth);
+val _ = ML_system_pp (fn depth => fn _ => Pretty.to_ML o prt_term false depth);
 
 
 local
@@ -84,21 +79,21 @@
     | _ %% _ => prt_proofs parens dp prf
     | Abst (a, T, b) =>
         prt_apps "Abst"
-         [Pretty.from_polyml (ML_system_pretty (a, dp - 1)),
-          Pretty.from_polyml (ML_system_pretty (T, dp - 2)),
+         [Pretty.from_ML (ML_system_pretty (a, dp - 1)),
+          Pretty.from_ML (ML_system_pretty (T, dp - 2)),
           prt_proof false (dp - 3) b]
     | AbsP (a, t, b) =>
         prt_apps "AbsP"
-         [Pretty.from_polyml (ML_system_pretty (a, dp - 1)),
-          Pretty.from_polyml (ML_system_pretty (t, dp - 2)),
+         [Pretty.from_ML (ML_system_pretty (a, dp - 1)),
+          Pretty.from_ML (ML_system_pretty (t, dp - 2)),
           prt_proof false (dp - 3) b]
     | Hyp t => prt_app "Hyp" (prt_term true (dp - 1) t)
     | MinProof => Pretty.str "MinProof"
-    | PBound a => prt_app "PBound" (Pretty.from_polyml (ML_system_pretty (a, dp - 1)))
-    | PAxm a => prt_app "PAxm" (Pretty.from_polyml (ML_system_pretty (a, dp - 1)))
-    | PClass a => prt_app "PClass" (Pretty.from_polyml (ML_system_pretty (a, dp - 1)))
-    | Oracle a => prt_app "Oracle" (Pretty.from_polyml (ML_system_pretty (a, dp - 1)))
-    | PThm a => prt_app "PThm" (Pretty.from_polyml (ML_system_pretty (a, dp - 1))))
+    | PBound a => prt_app "PBound" (Pretty.from_ML (ML_system_pretty (a, dp - 1)))
+    | PAxm a => prt_app "PAxm" (Pretty.from_ML (ML_system_pretty (a, dp - 1)))
+    | PClass a => prt_app "PClass" (Pretty.from_ML (ML_system_pretty (a, dp - 1)))
+    | Oracle a => prt_app "Oracle" (Pretty.from_ML (ML_system_pretty (a, dp - 1)))
+    | PThm a => prt_app "PThm" (Pretty.from_ML (ML_system_pretty (a, dp - 1))))
 
 and prt_proofs parens dp prf =
   let
@@ -111,7 +106,7 @@
       strip_proof p
         ((fn d =>
           [Pretty.str " %", Pretty.brk 1,
-            Pretty.from_polyml (ML_system_pretty (t, d))]) :: res)
+            Pretty.from_ML (ML_system_pretty (t, d))]) :: res)
   | strip_proof (p %% q) res =
       strip_proof p ((fn d => [Pretty.str " %%", Pretty.brk 1, prt_proof true d q]) :: res)
   | strip_proof p res = (fn d => prt_proof true d p, res);
@@ -119,8 +114,7 @@
 in
 
 val _ =
-  ML_system_pp (fn depth => fn _ => fn prf =>
-    ML_Pretty.to_polyml (Pretty.to_ML ~1 (prt_proof false depth prf)));
+  ML_system_pp (fn depth => fn _ => fn prf => Pretty.to_ML (prt_proof false depth prf));
 
 end;
 
diff -r 34906b3db920 -r 4a64fc4d1cde src/Pure/ML/ml_pretty.ML
--- a/src/Pure/ML/ml_pretty.ML	Wed Sep 04 16:21:52 2024 +0200
+++ b/src/Pure/ML/ml_pretty.ML	Thu Sep 05 17:39:45 2024 +0200
@@ -6,10 +6,8 @@
 
 signature ML_PRETTY =
 sig
-  datatype pretty =
-    Block of (string * string) * bool * FixedInt.int * pretty list |
-    String of string * FixedInt.int |
-    Break of bool * FixedInt.int * FixedInt.int
+  datatype context = datatype PolyML.context
+  datatype pretty = datatype PolyML.pretty
   val block: pretty list -> pretty
   val str: string -> pretty
   val brk: FixedInt.int -> pretty
@@ -17,28 +15,23 @@
     ('a * 'b) * FixedInt.int -> pretty
   val enum: string -> string -> string -> ('a * FixedInt.int -> pretty) ->
     'a list * FixedInt.int -> pretty
-  val to_polyml: pretty -> PolyML.pretty
-  val from_polyml: PolyML.pretty -> pretty
-  val format_polyml: int -> PolyML.pretty -> string
   val format: int -> pretty -> string
   val default_margin: int
-  val string_of_polyml: PolyML.pretty -> string
+  val string_of: pretty -> string
   val make_string_fn: string
 end;
 
 structure ML_Pretty: ML_PRETTY =
 struct
 
-(* datatype pretty *)
+(* datatype pretty with derived operations *)
 
-datatype pretty =
-  Block of (string * string) * bool * FixedInt.int * pretty list |
-  String of string * FixedInt.int |
-  Break of bool * FixedInt.int * FixedInt.int;
+datatype context = datatype PolyML.context;
+datatype pretty = datatype PolyML.pretty;
 
-fun block prts = Block (("", ""), false, 2, prts);
-fun str s = String (s, FixedInt.fromInt (size s));
-fun brk width = Break (false, width, 0);
+fun block prts = PrettyBlock (2, false, [], prts);
+val str = PrettyString;
+fun brk width = PrettyBreak (width, 0);
 
 fun pair pretty1 pretty2 ((x, y), depth: FixedInt.int) =
   block [str "(", pretty1 (x, depth), str ",", brk 1, pretty2 (y, depth - 1), str ")"];
@@ -52,64 +45,23 @@
   in block (str lpar :: (elems (FixedInt.max (depth, 0)) args @ [str rpar])) end;
 
 
-(* convert *)
-
-fun to_polyml (Break (false, width, offset)) = PolyML.PrettyBreak (width, offset)
-  | to_polyml (Break (true, _, _)) =
-      PolyML.PrettyBlock (0, false, [PolyML.ContextProperty ("fbrk", "")],
-        [PolyML.PrettyString " "])
-  | to_polyml (Block ((bg, en), consistent, ind, prts)) =
-      let val context =
-        (if bg = "" then [] else [PolyML.ContextProperty ("begin", bg)]) @
-        (if en = "" then [] else [PolyML.ContextProperty ("end", en)])
-      in PolyML.PrettyBlock (ind, consistent, context, map to_polyml prts) end
-  | to_polyml (String (s, len)) =
-      if len = FixedInt.fromInt (size s) then PolyML.PrettyString s
-      else
-        PolyML.PrettyBlock
-          (0, false,
-            [PolyML.ContextProperty ("length", FixedInt.toString len)], [PolyML.PrettyString s]);
-
-val from_polyml =
-  let
-    fun convert _ (PolyML.PrettyBreak (width, offset)) = Break (false, width, offset)
-      | convert _ (PolyML.PrettyBlock (_, _,
-            [PolyML.ContextProperty ("fbrk", _)], [PolyML.PrettyString " "])) =
-          Break (true, 1, 0)
-      | convert len (PolyML.PrettyBlock (ind, consistent, context, prts)) =
-          let
-            fun property name default =
-              (case List.find (fn PolyML.ContextProperty (a, _) => name = a | _ => false) context of
-                SOME (PolyML.ContextProperty (_, b)) => b
-              | _ => default);
-            val bg = property "begin" "";
-            val en = property "end" "";
-            val len' = property "length" len;
-          in Block ((bg, en), consistent, ind, map (convert len') prts) end
-      | convert len (PolyML.PrettyString s) =
-          String (s, FixedInt.fromInt (case Int.fromString len of SOME i => i | NONE => size s))
-  in convert "" end;
-
-
 (* format *)
 
-fun format_polyml margin prt =
+fun format margin prt =
   let
     val result = Unsynchronized.ref [];
-    val () = PolyML.prettyPrint (fn s => result := s :: ! result, margin) prt
-  in String.concat (List.rev (! result)) end;
-
-fun format margin = format_polyml margin o to_polyml;
+    val () = PolyML.prettyPrint (fn s => result := s :: ! result, margin) prt;
+  in implode (rev (! result)) end;
 
 val default_margin = 76;
 
 
 (* make string *)
 
-val string_of_polyml = format_polyml default_margin;
+val string_of = format default_margin;
 
 val make_string_fn =
-  "(fn x => ML_Pretty.string_of_polyml (ML_system_pretty \
+  "(fn x => ML_Pretty.string_of (ML_system_pretty \
     \(x, FixedInt.fromInt (ML_Print_Depth.get_print_depth ()))))";
 
 end;
diff -r 34906b3db920 -r 4a64fc4d1cde src/Pure/ML/ml_syntax.ML
--- a/src/Pure/ML/ml_syntax.ML	Wed Sep 04 16:21:52 2024 +0200
+++ b/src/Pure/ML/ml_syntax.ML	Thu Sep 05 17:39:45 2024 +0200
@@ -147,10 +147,10 @@
 
 val _ =
   ML_system_pp (fn depth => fn _ => fn str =>
-    Pretty.to_polyml (pretty_string' depth str));
+    Pretty.to_ML (pretty_string' depth str));
 
 val _ =
   ML_system_pp (fn depth => fn _ => fn chunks =>
-    Pretty.to_polyml (pretty_string' depth (Long_Name.implode_chunks chunks)));
+    Pretty.to_ML (pretty_string' depth (Long_Name.implode_chunks chunks)));
 
 end;
diff -r 34906b3db920 -r 4a64fc4d1cde src/Pure/PIDE/xml.ML
--- a/src/Pure/PIDE/xml.ML	Wed Sep 04 16:21:52 2024 +0200
+++ b/src/Pure/PIDE/xml.ML	Thu Sep 05 17:39:45 2024 +0200
@@ -171,7 +171,7 @@
 
 fun pretty depth tree = Pretty.str (content_depth (Int.max (0, depth)) tree);
 
-val _ = ML_system_pp (fn depth => fn _ => Pretty.to_polyml o pretty (FixedInt.toInt depth));
+val _ = ML_system_pp (fn depth => fn _ => Pretty.to_ML o pretty (FixedInt.toInt depth));
 
 
 
diff -r 34906b3db920 -r 4a64fc4d1cde src/Pure/Syntax/ast.ML
--- a/src/Pure/Syntax/ast.ML	Wed Sep 04 16:21:52 2024 +0200
+++ b/src/Pure/Syntax/ast.ML	Thu Sep 05 17:39:45 2024 +0200
@@ -64,7 +64,7 @@
 fun pretty_rule (lhs, rhs) =
   Pretty.block [pretty_ast lhs, Pretty.str " \<leadsto>", Pretty.brk 1, pretty_ast rhs];
 
-val _ = ML_system_pp (fn _ => fn _ => Pretty.to_polyml o pretty_ast);
+val _ = ML_system_pp (fn _ => fn _ => Pretty.to_ML o pretty_ast);
 
 
 (* strip_positions *)
diff -r 34906b3db920 -r 4a64fc4d1cde src/Pure/Syntax/lexicon.ML
--- a/src/Pure/Syntax/lexicon.ML	Wed Sep 04 16:21:52 2024 +0200
+++ b/src/Pure/Syntax/lexicon.ML	Thu Sep 05 17:39:45 2024 +0200
@@ -491,6 +491,6 @@
 
 val _ =
   ML_system_pp (fn _ => fn _ =>
-    Pretty.to_polyml o Pretty.str_list "{" "}" o map quote o Scan.dest_lexicon);
+    Pretty.to_ML o Pretty.str_list "{" "}" o map quote o Scan.dest_lexicon);
 
 end;
diff -r 34906b3db920 -r 4a64fc4d1cde src/Pure/Tools/debugger.ML
--- a/src/Pure/Tools/debugger.ML	Wed Sep 04 16:21:52 2024 +0200
+++ b/src/Pure/Tools/debugger.ML	Thu Sep 05 17:39:45 2024 +0200
@@ -183,7 +183,7 @@
     val space = PolyML.DebuggerInterface.debugNameSpace (the_debug_state thread_name index);
 
     fun print x =
-      Pretty.from_polyml
+      Pretty.from_ML
         (PolyML.NameSpace.Values.printWithType
           (x, FixedInt.fromInt (ML_Print_Depth.get_print_depth ()), SOME space));
     fun print_all () =
diff -r 34906b3db920 -r 4a64fc4d1cde src/Pure/Tools/prismjs.ML
--- a/src/Pure/Tools/prismjs.ML	Wed Sep 04 16:21:52 2024 +0200
+++ b/src/Pure/Tools/prismjs.ML	Thu Sep 05 17:39:45 2024 +0200
@@ -50,7 +50,7 @@
 
 end;
 
-val _ = ML_system_pp (fn _ => fn _ => Pretty.to_polyml o Pretty.str o quote o language_name);
+val _ = ML_system_pp (fn _ => fn _ => ML_Pretty.str o quote o language_name);
 
 
 (* tokenize *)
diff -r 34906b3db920 -r 4a64fc4d1cde src/Pure/context.ML
--- a/src/Pure/context.ML	Wed Sep 04 16:21:52 2024 +0200
+++ b/src/Pure/context.ML	Thu Sep 05 17:39:45 2024 +0200
@@ -336,7 +336,7 @@
 
 val pretty_thy = Pretty.str_list "{" "}" o display_names;
 
-val _ = ML_system_pp (fn _ => fn _ => Pretty.to_polyml o pretty_thy);
+val _ = ML_system_pp (fn _ => fn _ => Pretty.to_ML o pretty_thy);
 
 fun pretty_abbrev_thy thy =
   let
diff -r 34906b3db920 -r 4a64fc4d1cde src/Pure/morphism.ML
--- a/src/Pure/morphism.ML	Wed Sep 04 16:21:52 2024 +0200
+++ b/src/Pure/morphism.ML	Thu Sep 05 17:39:45 2024 +0200
@@ -140,7 +140,7 @@
 
 fun pretty phi = Pretty.enum ";" "{" "}" (map Pretty.str (rev (#names (rep phi))));
 
-val _ = ML_system_pp (fn _ => fn _ => Pretty.to_polyml o pretty);
+val _ = ML_system_pp (fn _ => fn _ => Pretty.to_ML o pretty);
 
 val binding = apply #binding;
 fun binding_prefix morph = Binding.name "x" |> binding morph |> Binding.prefix_of;