# HG changeset patch
# User wenzelm
# Date 1460028908 -7200
# Node ID 845ed4584e212d664fc5a6e080681f2bf26a13f1
# Parent  fdc290b68ecd9792d43deceebbea8c6883ba0bf7
clarified bootstrap of @{make_string} -- avoid query on ML environment;

diff -r fdc290b68ecd -r 845ed4584e21 src/Pure/General/pretty.ML
--- a/src/Pure/General/pretty.ML	Thu Apr 07 12:13:11 2016 +0200
+++ b/src/Pure/General/pretty.ML	Thu Apr 07 13:35:08 2016 +0200
@@ -334,7 +334,7 @@
 
 (* output interfaces *)
 
-val margin_default = Unsynchronized.ref 76;  (*right margin, or page width*)
+val margin_default = Unsynchronized.ref ML_Pretty.default_margin;  (*right margin, or page width*)
 
 val symbolicN = "pretty_symbolic";
 
@@ -406,3 +406,9 @@
 val _ = ML_system_pp (fn _ => fn _ => to_polyml o position);
 
 end;
+
+structure ML_Pretty =
+struct
+  open ML_Pretty;
+  val string_of_polyml = Pretty.string_of o Pretty.from_polyml;
+end;
diff -r fdc290b68ecd -r 845ed4584e21 src/Pure/ML/ml_antiquotation.ML
--- a/src/Pure/ML/ml_antiquotation.ML	Thu Apr 07 12:13:11 2016 +0200
+++ b/src/Pure/ML/ml_antiquotation.ML	Thu Apr 07 13:35:08 2016 +0200
@@ -39,7 +39,7 @@
       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)) #>
+    (Args.context >> (ML_Pretty.make_string_local o ML_Context.struct_name)) #>
 
   value (Binding.make ("binding", @{here}))
     (Scan.lift (Parse.position Args.name) >> ML_Syntax.make_binding) #>
diff -r fdc290b68ecd -r 845ed4584e21 src/Pure/ML/ml_antiquotations.ML
--- a/src/Pure/ML/ml_antiquotations.ML	Thu Apr 07 12:13:11 2016 +0200
+++ b/src/Pure/ML/ml_antiquotations.ML	Thu Apr 07 13:35:08 2016 +0200
@@ -29,7 +29,7 @@
             ML_Syntax.print_position pos ^ "));\n";
           val body =
             "(fn x => (" ^ struct_name ^ "." ^ a ^
-              " (" ^ ML_Pretty.make_string_fn struct_name ^ " x); x))";
+              " (" ^ ML_Pretty.make_string_local struct_name ^ " x); x))";
         in (K (env, body), ctxt') end));
 
 
diff -r fdc290b68ecd -r 845ed4584e21 src/Pure/ML/ml_compiler0.ML
--- a/src/Pure/ML/ml_compiler0.ML	Thu Apr 07 12:13:11 2016 +0200
+++ b/src/Pure/ML/ml_compiler0.ML	Thu Apr 07 13:35:08 2016 +0200
@@ -68,7 +68,7 @@
           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 (ML_Pretty.make_string_global :: res)
       | input line (#"\\" :: #"<" :: cs) res = input line cs ("\092\092<" :: res)
       | input line (#"\n" :: cs) res = input (line + 1) cs ("\n" :: res)
       | input line (c :: cs) res = input line cs (str c :: res)
diff -r fdc290b68ecd -r 845ed4584e21 src/Pure/ML/ml_pretty.ML
--- a/src/Pure/ML/ml_pretty.ML	Thu Apr 07 12:13:11 2016 +0200
+++ b/src/Pure/ML/ml_pretty.ML	Thu Apr 07 13:35:08 2016 +0200
@@ -21,7 +21,10 @@
   val from_polyml: PolyML_Pretty.pretty -> pretty
   val format_polyml: int -> PolyML_Pretty.pretty -> string
   val format: int -> pretty -> string
-  val make_string_fn: string -> string
+  val default_margin: int
+  val string_of_polyml: PolyML_Pretty.pretty -> string
+  val make_string_global: string
+  val make_string_local: string -> string
 end;
 
 structure ML_Pretty: ML_PRETTY =
@@ -99,21 +102,17 @@
 
 fun format margin = format_polyml margin o to_polyml;
 
+val default_margin = 76;
+
 
 (* make string *)
 
-local
-  fun pretty_string_of s = "(fn x => Pretty.string_of (Pretty.from_polyml (" ^ s ^ ")))";
-  fun pretty_value depth = "ML_system_pretty (x, FixedInt.fromInt (" ^ depth ^ "))";
-in
+val string_of_polyml = format_polyml default_margin;
 
-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_Print_Depth.get_print_depth ()")
-  else "(fn x => ML_Pretty.format_polyml 78 (" ^ pretty_value "ML_Print_Depth.get_print_depth ()" ^ "))";
+fun make_string depth =
+  "(fn x => ML_Pretty.string_of_polyml (ML_system_pretty (x, FixedInt.fromInt (" ^ depth ^ "))))";
+
+val make_string_global = make_string "ML_Print_Depth.get_print_depth ()";
+fun make_string_local local_env = make_string (local_env ^ ".ML_print_depth ()");
 
 end;
-
-end;