--- a/src/Pure/General/linear_set.ML Thu Mar 03 11:54:51 2016 +0100
+++ b/src/Pure/General/linear_set.ML Thu Mar 03 11:59:03 2016 +0100
@@ -137,9 +137,11 @@
val _ =
PolyML.addPrettyPrinter (fn depth => fn pretty => fn set =>
- ml_pretty
+ ML_Pretty.to_polyml
(ML_Pretty.enum "," "{" "}"
- (ML_Pretty.pair (pretty_ml o PolyML.prettyRepresentation) (pretty_ml o pretty))
+ (ML_Pretty.pair
+ (ML_Pretty.from_polyml o PolyML.prettyRepresentation)
+ (ML_Pretty.from_polyml o pretty))
(dest set, depth)));
end;
--- a/src/Pure/General/table.ML Thu Mar 03 11:54:51 2016 +0100
+++ b/src/Pure/General/table.ML Thu Mar 03 11:59:03 2016 +0100
@@ -412,9 +412,11 @@
val _ =
PolyML.addPrettyPrinter (fn depth => fn pretty => fn tab =>
- ml_pretty
+ ML_Pretty.to_polyml
(ML_Pretty.enum "," "{" "}"
- (ML_Pretty.pair (pretty_ml o PolyML.prettyRepresentation) (pretty_ml o pretty))
+ (ML_Pretty.pair
+ (ML_Pretty.from_polyml o PolyML.prettyRepresentation)
+ (ML_Pretty.from_polyml o pretty))
(dest tab, depth)));
--- a/src/Pure/ML/exn_output.ML Thu Mar 03 11:54:51 2016 +0100
+++ b/src/Pure/ML/exn_output.ML Thu Mar 03 11:59:03 2016 +0100
@@ -20,7 +20,7 @@
fun pretty (exn: exn) =
Pretty.from_ML
- (pretty_ml
+ (ML_Pretty.from_polyml
(PolyML.prettyRepresentation (exn, FixedInt.fromInt (ML_Options.get_print_depth ()))));
end;
--- a/src/Pure/ML/install_pp_polyml.ML Thu Mar 03 11:54:51 2016 +0100
+++ b/src/Pure/ML/install_pp_polyml.ML Thu Mar 03 11:59:03 2016 +0100
@@ -5,64 +5,64 @@
*)
PolyML.addPrettyPrinter (fn _ => fn _ => fn _: Pretty.T =>
- ml_pretty (Pretty.to_ML (Pretty.str "<pretty>")));
+ ML_Pretty.to_polyml (Pretty.to_ML (Pretty.str "<pretty>")));
PolyML.addPrettyPrinter (fn _ => fn _ => fn lexicon =>
- ml_pretty (Pretty.to_ML (Lexicon.pp_lexicon lexicon)));
+ ML_Pretty.to_polyml (Pretty.to_ML (Lexicon.pp_lexicon lexicon)));
PolyML.addPrettyPrinter (fn _ => fn _ => fn task =>
- ml_pretty (Pretty.to_ML (Pretty.str (Task_Queue.str_of_task task))));
+ ML_Pretty.to_polyml (Pretty.to_ML (Pretty.str (Task_Queue.str_of_task task))));
PolyML.addPrettyPrinter (fn _ => fn _ => fn group =>
- ml_pretty (Pretty.to_ML (Pretty.str (Task_Queue.str_of_group group))));
+ ML_Pretty.to_polyml (Pretty.to_ML (Pretty.str (Task_Queue.str_of_group group))));
PolyML.addPrettyPrinter (fn _ => fn _ => fn pos =>
- ml_pretty (Pretty.to_ML (Pretty.position pos)));
+ ML_Pretty.to_polyml (Pretty.to_ML (Pretty.position pos)));
PolyML.addPrettyPrinter (fn _ => fn _ => fn binding =>
- ml_pretty (Pretty.to_ML (Binding.pp binding)));
+ ML_Pretty.to_polyml (Pretty.to_ML (Binding.pp binding)));
PolyML.addPrettyPrinter (fn _ => fn _ => fn th =>
- ml_pretty (Pretty.to_ML (Proof_Display.pp_thm Thy_Info.pure_theory th)));
+ ML_Pretty.to_polyml (Pretty.to_ML (Proof_Display.pp_thm Thy_Info.pure_theory th)));
PolyML.addPrettyPrinter (fn _ => fn _ => fn ct =>
- ml_pretty (Pretty.to_ML (Proof_Display.pp_cterm Thy_Info.pure_theory ct)));
+ ML_Pretty.to_polyml (Pretty.to_ML (Proof_Display.pp_cterm Thy_Info.pure_theory ct)));
PolyML.addPrettyPrinter (fn _ => fn _ => fn cT =>
- ml_pretty (Pretty.to_ML (Proof_Display.pp_ctyp Thy_Info.pure_theory cT)));
+ ML_Pretty.to_polyml (Pretty.to_ML (Proof_Display.pp_ctyp Thy_Info.pure_theory cT)));
PolyML.addPrettyPrinter (fn _ => fn _ => fn T =>
- ml_pretty (Pretty.to_ML (Proof_Display.pp_typ Thy_Info.pure_theory T)));
+ ML_Pretty.to_polyml (Pretty.to_ML (Proof_Display.pp_typ Thy_Info.pure_theory T)));
PolyML.addPrettyPrinter (fn _ => fn _ => fn thy =>
- ml_pretty (Pretty.to_ML (Context.pretty_thy thy)));
+ ML_Pretty.to_polyml (Pretty.to_ML (Context.pretty_thy thy)));
PolyML.addPrettyPrinter (fn _ => fn _ => fn ctxt =>
- ml_pretty (Pretty.to_ML (Proof_Display.pp_context ctxt)));
+ ML_Pretty.to_polyml (Pretty.to_ML (Proof_Display.pp_context ctxt)));
PolyML.addPrettyPrinter (fn _ => fn _ => fn ast =>
- ml_pretty (Pretty.to_ML (Ast.pretty_ast ast)));
+ ML_Pretty.to_polyml (Pretty.to_ML (Ast.pretty_ast ast)));
PolyML.addPrettyPrinter (fn _ => fn _ => fn path =>
- ml_pretty (Pretty.to_ML (Path.pretty path)));
+ ML_Pretty.to_polyml (Pretty.to_ML (Path.pretty path)));
PolyML.addPrettyPrinter (fn _ => fn _ => fn digest =>
- ml_pretty (Pretty.to_ML (Pretty.str (quote (SHA1.rep digest)))));
+ ML_Pretty.to_polyml (Pretty.to_ML (Pretty.str (quote (SHA1.rep digest)))));
PolyML.addPrettyPrinter (fn _ => fn _ => fn _: Proof.state =>
- ml_pretty (Pretty.to_ML (Pretty.str "<Proof.state>")));
+ ML_Pretty.to_polyml (Pretty.to_ML (Pretty.str "<Proof.state>")));
PolyML.addPrettyPrinter (fn _ => fn _ => fn st =>
- ml_pretty (Pretty.to_ML (Toplevel.pretty_abstract st)));
+ ML_Pretty.to_polyml (Pretty.to_ML (Toplevel.pretty_abstract st)));
PolyML.addPrettyPrinter (fn _ => fn _ => fn morphism =>
- ml_pretty (Pretty.to_ML (Morphism.pretty morphism)));
+ ML_Pretty.to_polyml (Pretty.to_ML (Morphism.pretty morphism)));
PolyML.addPrettyPrinter (fn depth => fn _ => fn str =>
- ml_pretty (Pretty.to_ML (ML_Syntax.pretty_string (FixedInt.toInt (depth * 100)) str)));
+ ML_Pretty.to_polyml (Pretty.to_ML (ML_Syntax.pretty_string (FixedInt.toInt (depth * 100)) str)));
PolyML.addPrettyPrinter (fn depth => fn _ => fn tree =>
- ml_pretty (Pretty.to_ML (XML.pretty (FixedInt.toInt depth) tree)));
+ ML_Pretty.to_polyml (Pretty.to_ML (XML.pretty (FixedInt.toInt depth) tree)));
PolyML.addPrettyPrinter (fn depth => fn pretty => fn var =>
pretty (Synchronized.value var, depth));
@@ -83,7 +83,7 @@
local
open PolyML;
-val from_ML = Pretty.from_ML o pretty_ml;
+val from_ML = Pretty.from_ML o ML_Pretty.from_polyml;
fun prt_app name prt = Pretty.block [Pretty.str (name ^ " "), prt];
fun prt_apps name = Pretty.enum "," (name ^ " (") ")";
@@ -110,7 +110,7 @@
val _ =
PolyML.addPrettyPrinter (fn depth => fn _ => fn t =>
- ml_pretty (Pretty.to_ML (prt_term false depth t)));
+ ML_Pretty.to_polyml (Pretty.to_ML (prt_term false depth t)));
local
@@ -157,7 +157,7 @@
val _ =
PolyML.addPrettyPrinter (fn depth => fn _ => fn prf =>
- ml_pretty (Pretty.to_ML (prt_proof false depth prf)));
+ ML_Pretty.to_polyml (Pretty.to_ML (prt_proof false depth prf)));
end;
--- a/src/Pure/ML/ml_compiler.ML Thu Mar 03 11:54:51 2016 +0100
+++ b/src/Pure/ML/ml_compiler.ML Thu Mar 03 11:59:03 2016 +0100
@@ -65,7 +65,7 @@
let
val xml =
ML_Name_Space.displayTypeExpression (types, depth, space)
- |> pretty_ml |> Pretty.from_ML |> Pretty.string_of
+ |> ML_Pretty.from_polyml |> 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;
@@ -193,7 +193,7 @@
val pos = Exn_Properties.position_of loc;
val txt =
(if hard then "ML error" else "ML warning") ^ Position.here pos ^ ":\n" ^
- Pretty.string_of (Pretty.from_ML (pretty_ml msg));
+ Pretty.string_of (Pretty.from_ML (ML_Pretty.from_polyml msg));
in if hard then err txt else warn txt end;
@@ -205,7 +205,8 @@
let
fun display disp x =
if depth > 0 then
- (disp x |> pretty_ml |> Pretty.from_ML |> Pretty.string_of |> write; write "\n")
+ (write (disp x |> ML_Pretty.from_polyml |> Pretty.from_ML |> Pretty.string_of);
+ write "\n")
else ();
fun apply_fix (a, b) =
--- a/src/Pure/RAW/ROOT_polyml.ML Thu Mar 03 11:54:51 2016 +0100
+++ b/src/Pure/RAW/ROOT_polyml.ML Thu Mar 03 11:59:03 2016 +0100
@@ -92,43 +92,6 @@
val error_depth = PolyML.error_depth;
-val pretty_ml =
- let
- fun convert _ (PolyML.PrettyBreak (width, offset)) = ML_Pretty.Break (false, width, offset)
- | convert _ (PolyML.PrettyBlock (_, _,
- [PolyML.ContextProperty ("fbrk", _)], [PolyML.PrettyString " "])) =
- ML_Pretty.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 ML_Pretty.Block ((bg, en), consistent, ind, map (convert len') prts) end
- | convert len (PolyML.PrettyString s) =
- ML_Pretty.String
- (s, FixedInt.fromInt (case Int.fromString len of SOME i => i | NONE => size s))
- in convert "" end;
-
-fun ml_pretty (ML_Pretty.Break (false, width, offset)) = PolyML.PrettyBreak (width, offset)
- | ml_pretty (ML_Pretty.Break (true, _, _)) =
- PolyML.PrettyBlock (0, false, [PolyML.ContextProperty ("fbrk", "")],
- [PolyML.PrettyString " "])
- | ml_pretty (ML_Pretty.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 ml_pretty prts) end
- | ml_pretty (ML_Pretty.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]);
-
(* ML compiler *)
@@ -137,7 +100,7 @@
structure ML_Name_Space =
struct
open ML_Name_Space;
- val display_val = pretty_ml o displayVal;
+ val display_val = ML_Pretty.from_polyml o displayVal;
end;
use "RAW/ml_positions.ML";
@@ -150,7 +113,7 @@
PolyML.Compiler.prompt2 := "ML# ";
fun ml_make_string struct_name =
- "(fn x => Pretty.string_of (Pretty.from_ML (pretty_ml (PolyML.prettyRepresentation (x, FixedInt.fromInt (" ^
+ "(fn x => Pretty.string_of (Pretty.from_ML (ML_Pretty.from_polyml (PolyML.prettyRepresentation (x, FixedInt.fromInt (" ^
struct_name ^ ".ML_print_depth ()))))))";
--- a/src/Pure/RAW/ml_debugger.ML Thu Mar 03 11:54:51 2016 +0100
+++ b/src/Pure/RAW/ml_debugger.ML Thu Mar 03 11:59:03 2016 +0100
@@ -44,7 +44,7 @@
val _ =
PolyML.addPrettyPrinter (fn _ => fn _ => fn exn_id =>
let val s = print_exn_id exn_id
- in ml_pretty (ML_Pretty.String (s, FixedInt.fromInt (size s))) end);
+ in ML_Pretty.to_polyml (ML_Pretty.String (s, FixedInt.fromInt (size s))) end);
(* hooks *)
--- a/src/Pure/RAW/ml_pretty.ML Thu Mar 03 11:54:51 2016 +0100
+++ b/src/Pure/RAW/ml_pretty.ML Thu Mar 03 11:59:03 2016 +0100
@@ -1,10 +1,25 @@
(* Title: Pure/RAW/ml_pretty.ML
Author: Makarius
-Minimal support for raw ML pretty printing -- for boot-strapping only.
+Minimal support for raw ML pretty printing, notably for toplevel pp.
*)
-structure ML_Pretty =
+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
+ val block: pretty list -> pretty
+ val str: string -> pretty
+ val brk: FixedInt.int -> pretty
+ val pair: ('a * int -> pretty) -> ('b * int -> pretty) -> ('a * 'b) * int -> pretty
+ val enum: string -> string -> string -> ('a * int -> pretty) -> 'a list * int -> pretty
+ val to_polyml: pretty -> PolyML.pretty
+ val from_polyml: PolyML.pretty -> pretty
+end;
+
+structure ML_Pretty: ML_PRETTY =
struct
datatype pretty =
@@ -27,4 +42,43 @@
| elems d (x :: xs) = pretty (x, d) :: str sep :: brk 1 :: elems (d - 1) xs;
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;
+
end;