--- a/NEWS Thu Mar 17 13:44:18 2016 +0100
+++ b/NEWS Thu Mar 17 16:56:44 2016 +0100
@@ -216,6 +216,9 @@
*** ML ***
+* Antiquotation @{make_string} is available during Pure bootstrap --
+with approximative output quality.
+
* Option ML_exception_debugger controls detailed exception trace via the
Poly/ML debugger. Relevant ML modules need to be compiled beforehand
with ML_file_debug, or with ML_file and option ML_debugger enabled. Note
--- a/src/Pure/ML/ml_antiquotation.ML Thu Mar 17 13:44:18 2016 +0100
+++ b/src/Pure/ML/ml_antiquotation.ML Thu Mar 17 16:56:44 2016 +0100
@@ -38,8 +38,10 @@
(fn src => fn () =>
ML_Context.value_decl "position" (ML_Syntax.print_position (#2 (Token.name_of_src src)))) #>
+ inline (Binding.make ("make_string", @{here}))
+ (Args.context >> (ML_Pretty.make_string_fn o ML_Context.struct_name)) #>
+
value (Binding.make ("binding", @{here}))
(Scan.lift (Parse.position Args.name) >> ML_Syntax.make_binding));
end;
-
--- a/src/Pure/ML/ml_antiquotations.ML Thu Mar 17 13:44:18 2016 +0100
+++ b/src/Pure/ML/ml_antiquotations.ML Thu Mar 17 16:56:44 2016 +0100
@@ -21,9 +21,6 @@
ML_Antiquotation.inline @{binding assert}
(Scan.succeed "(fn b => if b then () else raise General.Fail \"Assertion failed\")") #>
- ML_Antiquotation.inline @{binding make_string}
- (Args.context >> (ml_make_string o ML_Context.struct_name)) #>
-
ML_Antiquotation.declaration @{binding print}
(Scan.lift (Scan.optional Args.name "Output.writeln"))
(fn src => fn output => fn ctxt =>
@@ -36,7 +33,8 @@
\ (" ^ output ^ ") o (fn s => s ^ Position.here (" ^
ML_Syntax.print_position pos ^ "));\n";
val body =
- "(fn x => (" ^ struct_name ^ "." ^ a ^ " (" ^ ml_make_string struct_name ^ " x); x))";
+ "(fn x => (" ^ struct_name ^ "." ^ a ^
+ " (" ^ ML_Pretty.make_string_fn struct_name ^ " x); x))";
in (K (env, body), ctxt') end));
--- a/src/Pure/ML/ml_compiler0.ML Thu Mar 17 13:44:18 2016 +0100
+++ b/src/Pure/ML/ml_compiler0.ML Thu Mar 17 16:56:44 2016 +0100
@@ -33,14 +33,17 @@
fun ml_input start_line name txt =
let
- fun positions line (#"@" :: #"{" :: #"h" :: #"e" :: #"r" :: #"e" :: #"}" :: cs) res =
+ fun input line (#"@" :: #"{" :: #"h" :: #"e" :: #"r" :: #"e" :: #"}" :: cs) res =
let val s = "(Position.line_file_only " ^ Int.toString line ^ " \"" ^ name ^ "\")"
- in positions line cs (s :: res) end
- | positions line (#"\\" :: #"<" :: cs) res = positions line cs ("\\\\<" :: res)
- | positions line (#"\n" :: cs) res = positions (line + 1) cs ("\n" :: res)
- | positions line (c :: cs) res = positions line cs (str c :: res)
- | positions _ [] res = rev res;
- in String.concat (positions start_line (String.explode txt) []) end;
+ in input line cs (s :: res) end
+ | input line (#"@" :: #"{" :: #"m" :: #"a" :: #"k" :: #"e" :: #"_" ::
+ #"s" :: #"t" :: #"r" :: #"i" :: #"n" :: #"g" :: #"}" :: cs) res =
+ input line cs (ML_Pretty.make_string_fn "" :: res)
+ | input line (#"\\" :: #"<" :: cs) res = input line cs ("\\\\<" :: res)
+ | input line (#"\n" :: cs) res = input (line + 1) cs ("\n" :: res)
+ | input line (c :: cs) res = input line cs (str c :: res)
+ | input _ [] res = rev res;
+ in String.concat (input start_line (String.explode txt) []) end;
fun use_text ({name_space, here, print, error, ...}: context) {line, file, verbose, debug} text =
let
--- a/src/Pure/ML/ml_pretty.ML Thu Mar 17 13:44:18 2016 +0100
+++ b/src/Pure/ML/ml_pretty.ML Thu Mar 17 16:56:44 2016 +0100
@@ -19,6 +19,9 @@
val from_polyml: PolyML.pretty -> pretty
val get_print_depth: unit -> int
val print_depth: int -> unit
+ val format_polyml: int -> PolyML.pretty -> string
+ val format: int -> pretty -> string
+ val make_string_fn: string -> string
end;
structure ML_Pretty: ML_PRETTY =
@@ -96,4 +99,33 @@
val _ = print_depth 10;
end;
+
+(* format *)
+
+fun format_polyml 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;
+
+
+(* make string *)
+
+local
+ fun pretty_string_of s =
+ "(fn x => Pretty.string_of (Pretty.from_ML (ML_Pretty.from_polyml (" ^ s ^ "))))";
+ fun pretty_value depth = "PolyML.prettyRepresentation (x, FixedInt.fromInt (" ^ depth ^ "))";
+in
+
+fun make_string_fn local_env =
+ if local_env <> "" then
+ pretty_string_of (pretty_value (local_env ^ ".ML_print_depth ()"))
+ else if List.exists (fn (a, _) => a = "Pretty") (#allStruct ML_Name_Space.global ()) then
+ pretty_string_of (pretty_value "ML_Pretty.get_print_depth ()")
+ else "(fn x => ML_Pretty.format_polyml 78 (" ^ pretty_value "ML_Pretty.get_print_depth ()" ^ "))";
+
end;
+
+end;
--- a/src/Pure/ROOT.ML Thu Mar 17 13:44:18 2016 +0100
+++ b/src/Pure/ROOT.ML Thu Mar 17 16:56:44 2016 +0100
@@ -69,10 +69,6 @@
PolyML.Compiler.printInAlphabeticalOrder := false;
PolyML.Compiler.maxInlineSize := 80;
-fun ml_make_string struct_name =
- "(fn x => Pretty.string_of (Pretty.from_ML (ML_Pretty.from_polyml (PolyML.prettyRepresentation (x, FixedInt.fromInt (" ^
- struct_name ^ ".ML_print_depth ()))))))";
-
(* ML debugger *)