# HG changeset patch
# User wenzelm
# Date 1406836941 -7200
# Node ID 0d295e339f52d94f7d803d94508998d4f11846c3
# Parent  2c2bae3da1c20ecdbbed3981ac742c6944c5f75f
prefer dynamic ML_print_depth if context happens to be available;

diff -r 2c2bae3da1c2 -r 0d295e339f52 src/Doc/Implementation/ML.thy
--- a/src/Doc/Implementation/ML.thy	Thu Jul 31 21:29:31 2014 +0200
+++ b/src/Doc/Implementation/ML.thy	Thu Jul 31 22:02:21 2014 +0200
@@ -725,7 +725,7 @@
   \item @{text "@{make_string}"} inlines a function to print arbitrary values
   similar to the ML toplevel. The result is compiler dependent and may fall
   back on "?" in certain situations. The value of configuration option
-  @{attribute_ref ML_print_depth} is used implicitly at compile-time.
+  @{attribute_ref ML_print_depth} determines further details of output.
 
   \item @{text "@{print f}"} uses the ML function @{text "f: string ->
   unit"} to output the result of @{text "@{make_string}"} above,
diff -r 2c2bae3da1c2 -r 0d295e339f52 src/Pure/ML-Systems/polyml.ML
--- a/src/Pure/ML-Systems/polyml.ML	Thu Jul 31 21:29:31 2014 +0200
+++ b/src/Pure/ML-Systems/polyml.ML	Thu Jul 31 22:02:21 2014 +0200
@@ -174,5 +174,5 @@
     ("PolyML.addPrettyPrinter (fn _ => fn _ => ml_pretty o Pretty.to_ML o (" ^ pp ^ "))");
 
 val ml_make_string =
-  "(fn x => Pretty.string_of (Pretty.from_ML (pretty_ml (PolyML.prettyRepresentation (x, Isabelle.ML_print_depth)))))";
+  "(fn x => Pretty.string_of (Pretty.from_ML (pretty_ml (PolyML.prettyRepresentation (x, Isabelle.ML_print_depth ())))))";
 
diff -r 2c2bae3da1c2 -r 0d295e339f52 src/Pure/ML/ml_context.ML
--- a/src/Pure/ML/ml_context.ML	Thu Jul 31 21:29:31 2014 +0200
+++ b/src/Pure/ML/ml_context.ML	Thu Jul 31 22:02:21 2014 +0200
@@ -94,7 +94,9 @@
     ("structure Isabelle =\nstruct\n\
      \val ML_context = Context_Position.set_visible " ^ Bool.toString visible ^
      " (ML_Context.the_local_context ());\n\
-     \val ML_print_depth = ML_Options.get_print_depth ();\n");
+     \val ML_print_depth =\n\
+     \  let val default = ML_Options.get_print_depth ()\n\
+     \  in fn () => ML_Options.get_print_depth_default default end;\n");
 
 val end_env = ML_Lex.tokenize "end;";
 val reset_env = ML_Lex.tokenize "structure Isabelle = struct end";
diff -r 2c2bae3da1c2 -r 0d295e339f52 src/Pure/ML/ml_options.ML
--- a/src/Pure/ML/ml_options.ML	Thu Jul 31 21:29:31 2014 +0200
+++ b/src/Pure/ML/ml_options.ML	Thu Jul 31 22:02:21 2014 +0200
@@ -14,6 +14,7 @@
   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_Options: ML_OPTIONS =
@@ -47,4 +48,9 @@
     NONE => get_default_print_depth ()
   | SOME context => Config.get_generic context print_depth);
 
+fun get_print_depth_default default =
+  (case Context.thread_data () of
+    NONE => default
+  | SOME context => Config.get_generic context print_depth);
+
 end;