# 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 "" - | SOME (Exn.Exn _) => PolyML.PrettyString "" + NONE => ML_Pretty.str "" + | SOME (Exn.Exn _) => ML_Pretty.str "" | 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 "" - | SOME (Exn.Exn _) => PolyML.PrettyString "" + NONE => ML_Pretty.str "" + | SOME (Exn.Exn _) => ML_Pretty.str "" | 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 "")); + ML_system_pp (fn _ => fn _ => fn _: state => ML_Pretty.str ""); 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 (""); -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 ("")); 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 " \", 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;