1.1 --- a/src/Doc/Implementation/ML.thy	Thu Jul 31 20:09:30 2014 +0200
     1.2 +++ b/src/Doc/Implementation/ML.thy	Thu Jul 31 20:59:10 2014 +0200
     1.3 @@ -722,9 +722,10 @@
     1.4  
     1.5    \begin{description}
     1.6  
     1.7 -  \item @{text "@{make_string}"} inlines a function to print arbitrary
     1.8 -  values similar to the ML toplevel.  The result is compiler dependent
     1.9 -  and may fall back on "?" in certain situations.
    1.10 +  \item @{text "@{make_string}"} inlines a function to print arbitrary values
    1.11 +  similar to the ML toplevel. The result is compiler dependent and may fall
    1.12 +  back on "?" in certain situations. The value of configuration option
    1.13 +  @{attribute_ref ML_print_depth} is used implicitly at compile-time.
    1.14  
    1.15    \item @{text "@{print f}"} uses the ML function @{text "f: string ->
    1.16    unit"} to output the result of @{text "@{make_string}"} above,

     2.1 --- a/src/Pure/ML-Systems/polyml.ML	Thu Jul 31 20:09:30 2014 +0200
     2.2 +++ b/src/Pure/ML-Systems/polyml.ML	Thu Jul 31 20:59:10 2014 +0200
     2.3 @@ -174,5 +174,5 @@
     2.4      ("PolyML.addPrettyPrinter (fn _ => fn _ => ml_pretty o Pretty.to_ML o (" ^ pp ^ "))");
     2.5  
     2.6  val ml_make_string =
     2.7 -  "(fn x => Pretty.string_of (Pretty.from_ML (pretty_ml (PolyML.prettyRepresentation (x, ML_Options.get_print_depth ())))))";
     2.8 +  "(fn x => Pretty.string_of (Pretty.from_ML (pretty_ml (PolyML.prettyRepresentation (x, Isabelle.ML_print_depth)))))";
     2.9  

     3.1 --- a/src/Pure/ML/ml_antiquotation.ML	Thu Jul 31 20:09:30 2014 +0200
     3.2 +++ b/src/Pure/ML/ml_antiquotation.ML	Thu Jul 31 20:59:10 2014 +0200
     3.3 @@ -19,7 +19,7 @@
     3.4  
     3.5  (* unique names *)
     3.6  
     3.7 -val init_context = ML_Syntax.reserved |> Name.declare "ML_context";
     3.8 +val init_context = ML_Syntax.reserved |> fold Name.declare ["ML_context", "ML_print_depth"];
     3.9  
    3.10  structure Names = Proof_Data
    3.11  (

     4.1 --- a/src/Pure/ML/ml_context.ML	Thu Jul 31 20:09:30 2014 +0200
     4.2 +++ b/src/Pure/ML/ml_context.ML	Thu Jul 31 20:59:10 2014 +0200
     4.3 @@ -93,7 +93,8 @@
     4.4    ML_Lex.tokenize
     4.5      ("structure Isabelle =\nstruct\n\
     4.6       \val ML_context = Context_Position.set_visible " ^ Bool.toString visible ^
     4.7 -     " (ML_Context.the_local_context ());\n");
     4.8 +     " (ML_Context.the_local_context ());\n\
     4.9 +     \val ML_print_depth = ML_Options.get_print_depth ();\n");
    4.10  
    4.11  val end_env = ML_Lex.tokenize "end;";
    4.12  val reset_env = ML_Lex.tokenize "structure Isabelle = struct end";