# HG changeset patch
# User wenzelm
# Date 1458230204 -3600
# Node ID 291cc01f56f5464930528221e687aadc891afba7
# Parent  c23ff2f45a1863b8d4f7c6dc5cae13b58bd1dc1d
@{make_string} is available during Pure bootstrap;

diff -r c23ff2f45a18 -r 291cc01f56f5 NEWS
--- 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
diff -r c23ff2f45a18 -r 291cc01f56f5 src/Pure/ML/ml_antiquotation.ML
--- 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;
-
diff -r c23ff2f45a18 -r 291cc01f56f5 src/Pure/ML/ml_antiquotations.ML
--- 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));
 
 
diff -r c23ff2f45a18 -r 291cc01f56f5 src/Pure/ML/ml_compiler0.ML
--- 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
diff -r c23ff2f45a18 -r 291cc01f56f5 src/Pure/ML/ml_pretty.ML
--- 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;
diff -r c23ff2f45a18 -r 291cc01f56f5 src/Pure/ROOT.ML
--- 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 *)