# HG changeset patch
# User wenzelm
# Date 1406833150 -7200
# Node ID 5b48f2047c24debc374958f55a10384a90e472e9
# Parent  885888a880fb9789ff1318025bf464c7658e9be5
clarified compile-time use of ML_print_depth;

diff -r 885888a880fb -r 5b48f2047c24 src/Doc/Implementation/ML.thy
--- a/src/Doc/Implementation/ML.thy	Thu Jul 31 20:09:30 2014 +0200
+++ b/src/Doc/Implementation/ML.thy	Thu Jul 31 20:59:10 2014 +0200
@@ -722,9 +722,10 @@
 
   \begin{description}
 
-  \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.
+  \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.
 
   \item @{text "@{print f}"} uses the ML function @{text "f: string ->
   unit"} to output the result of @{text "@{make_string}"} above,
diff -r 885888a880fb -r 5b48f2047c24 src/Pure/ML-Systems/polyml.ML
--- a/src/Pure/ML-Systems/polyml.ML	Thu Jul 31 20:09:30 2014 +0200
+++ b/src/Pure/ML-Systems/polyml.ML	Thu Jul 31 20:59:10 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, ML_Options.get_print_depth ())))))";
+  "(fn x => Pretty.string_of (Pretty.from_ML (pretty_ml (PolyML.prettyRepresentation (x, Isabelle.ML_print_depth)))))";
 
diff -r 885888a880fb -r 5b48f2047c24 src/Pure/ML/ml_antiquotation.ML
--- a/src/Pure/ML/ml_antiquotation.ML	Thu Jul 31 20:09:30 2014 +0200
+++ b/src/Pure/ML/ml_antiquotation.ML	Thu Jul 31 20:59:10 2014 +0200
@@ -19,7 +19,7 @@
 
 (* unique names *)
 
-val init_context = ML_Syntax.reserved |> Name.declare "ML_context";
+val init_context = ML_Syntax.reserved |> fold Name.declare ["ML_context", "ML_print_depth"];
 
 structure Names = Proof_Data
 (
diff -r 885888a880fb -r 5b48f2047c24 src/Pure/ML/ml_context.ML
--- a/src/Pure/ML/ml_context.ML	Thu Jul 31 20:09:30 2014 +0200
+++ b/src/Pure/ML/ml_context.ML	Thu Jul 31 20:59:10 2014 +0200
@@ -93,7 +93,8 @@
   ML_Lex.tokenize
     ("structure Isabelle =\nstruct\n\
      \val ML_context = Context_Position.set_visible " ^ Bool.toString visible ^
-     " (ML_Context.the_local_context ());\n");
+     " (ML_Context.the_local_context ());\n\
+     \val ML_print_depth = ML_Options.get_print_depth ();\n");
 
 val end_env = ML_Lex.tokenize "end;";
 val reset_env = ML_Lex.tokenize "structure Isabelle = struct end";