--- 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 ?
--- 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)));
--- 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;
--- 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;
--- 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 *)
--- 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!*)
--- 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;
--- 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;
--- 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));
--- 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;
--- 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 =>
--- 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!*)
--- 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,
--- 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 *)
--- 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);
--- 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) =
--- 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;
--- 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;
--- 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;
--- 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));
--- 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 *)
--- 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;
--- 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 () =
--- 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 *)
--- 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
--- 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;