# HG changeset patch
# User wenzelm
# Date 1460030042 -7200
# Node ID c641bf9402fdac98f880868bdf6b0e53b7639f27
# Parent  845ed4584e212d664fc5a6e080681f2bf26a13f1
simplified default print_depth: context is usually available, in contrast to 0d295e339f52;

diff -r 845ed4584e21 -r c641bf9402fd src/Pure/ML/ml_antiquotation.ML
--- a/src/Pure/ML/ml_antiquotation.ML	Thu Apr 07 13:35:08 2016 +0200
+++ b/src/Pure/ML/ml_antiquotation.ML	Thu Apr 07 13:54:02 2016 +0200
@@ -38,8 +38,7 @@
     (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_local o ML_Context.struct_name)) #>
+  inline (Binding.make ("make_string", @{here})) (Args.context >> K ML_Pretty.make_string_fn) #>
 
   value (Binding.make ("binding", @{here}))
     (Scan.lift (Parse.position Args.name) >> ML_Syntax.make_binding) #>
diff -r 845ed4584e21 -r c641bf9402fd src/Pure/ML/ml_antiquotations.ML
--- a/src/Pure/ML/ml_antiquotations.ML	Thu Apr 07 13:35:08 2016 +0200
+++ b/src/Pure/ML/ml_antiquotations.ML	Thu Apr 07 13:54:02 2016 +0200
@@ -28,8 +28,7 @@
             \  (" ^ output ^ ") o (fn s => s ^ Position.here (" ^
             ML_Syntax.print_position pos ^ "));\n";
           val body =
-            "(fn x => (" ^ struct_name ^ "." ^ a ^
-              " (" ^ ML_Pretty.make_string_local struct_name ^ " x); x))";
+            "(fn x => (" ^ struct_name ^ "." ^ a ^ " (" ^ ML_Pretty.make_string_fn ^ " x); x))";
         in (K (env, body), ctxt') end));
 
 
diff -r 845ed4584e21 -r c641bf9402fd src/Pure/ML/ml_compiler0.ML
--- a/src/Pure/ML/ml_compiler0.ML	Thu Apr 07 13:35:08 2016 +0200
+++ b/src/Pure/ML/ml_compiler0.ML	Thu Apr 07 13:54:02 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_global :: res)
+          input line cs (ML_Pretty.make_string_fn :: 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 845ed4584e21 -r c641bf9402fd src/Pure/ML/ml_context.ML
--- a/src/Pure/ML/ml_context.ML	Thu Apr 07 13:35:08 2016 +0200
+++ b/src/Pure/ML/ml_context.ML	Thu Apr 07 13:54:02 2016 +0200
@@ -50,7 +50,7 @@
 structure Names = Proof_Data
 (
   type T = string * Name.context;
-  val init_names = ML_Syntax.reserved |> fold Name.declare ["ML_context", "ML_print_depth"];
+  val init_names = ML_Syntax.reserved |> Name.declare "ML_context";
   fun init _ = ("Isabelle0", init_names);
 );
 
@@ -117,10 +117,7 @@
   (ML_Lex.tokenize
     ("structure " ^ name ^ " =\nstruct\n\
      \val ML_context = Context_Position.set_visible " ^ Bool.toString visible ^
-     " (Context.the_local_context ());\n\
-     \val ML_print_depth =\n\
-     \  let val default = ML_Print_Depth.get_print_depth ()\n\
-     \  in fn () => ML_Print_Depth.get_print_depth_default default end;\n"),
+     " (Context.the_local_context ());\n"),
    ML_Lex.tokenize "end;");
 
 fun reset_env name = ML_Lex.tokenize ("structure " ^ name ^ " = struct end");
diff -r 845ed4584e21 -r c641bf9402fd src/Pure/ML/ml_pretty.ML
--- a/src/Pure/ML/ml_pretty.ML	Thu Apr 07 13:35:08 2016 +0200
+++ b/src/Pure/ML/ml_pretty.ML	Thu Apr 07 13:54:02 2016 +0200
@@ -23,8 +23,7 @@
   val format: int -> pretty -> string
   val default_margin: int
   val string_of_polyml: PolyML_Pretty.pretty -> string
-  val make_string_global: string
-  val make_string_local: string -> string
+  val make_string_fn: string
 end;
 
 structure ML_Pretty: ML_PRETTY =
@@ -109,10 +108,8 @@
 
 val string_of_polyml = format_polyml default_margin;
 
-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 ()");
+val make_string_fn =
+  "(fn x => ML_Pretty.string_of_polyml (ML_system_pretty \
+    \(x, FixedInt.fromInt (ML_Print_Depth.get_print_depth ()))))";
 
 end;
diff -r 845ed4584e21 -r c641bf9402fd src/Pure/ML/ml_print_depth.ML
--- a/src/Pure/ML/ml_print_depth.ML	Thu Apr 07 13:35:08 2016 +0200
+++ b/src/Pure/ML/ml_print_depth.ML	Thu Apr 07 13:54:02 2016 +0200
@@ -10,7 +10,6 @@
   val print_depth_raw: Config.raw
   val print_depth: int Config.T
   val get_print_depth: unit -> int
-  val get_print_depth_default: int -> int
 end;
 
 structure ML_Print_Depth: ML_PRINT_DEPTH =
@@ -29,9 +28,4 @@
     NONE => ML_Print_Depth.get_print_depth ()
   | SOME context => Config.get_generic context print_depth);
 
-fun get_print_depth_default default =
-  (case Context.get_generic_context () of
-    NONE => default
-  | SOME context => Config.get_generic context print_depth);
-
 end;
diff -r 845ed4584e21 -r c641bf9402fd src/Pure/ML/ml_print_depth0.ML
--- a/src/Pure/ML/ml_print_depth0.ML	Thu Apr 07 13:35:08 2016 +0200
+++ b/src/Pure/ML/ml_print_depth0.ML	Thu Apr 07 13:54:02 2016 +0200
@@ -8,7 +8,6 @@
 sig
   val set_print_depth: int -> unit
   val get_print_depth: unit -> int
-  val get_print_depth_default: int -> int
 end;
 
 structure ML_Print_Depth: ML_PRINT_DEPTH =
@@ -18,6 +17,5 @@
 
 fun set_print_depth n = (depth := n; PolyML.print_depth n);
 fun get_print_depth () = ! depth;
-fun get_print_depth_default _ = ! depth;
 
 end;
diff -r 845ed4584e21 -r c641bf9402fd src/Pure/ML/ml_thms.ML
--- a/src/Pure/ML/ml_thms.ML	Thu Apr 07 13:35:08 2016 +0200
+++ b/src/Pure/ML/ml_thms.ML	Thu Apr 07 13:54:02 2016 +0200
@@ -138,4 +138,3 @@
 fun bind_thms (name, thms) = store_thms (name, map Drule.export_without_context thms);
 
 end;
-