--- 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;
--- 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) #>
--- 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));
--- 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)
--- 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;