src/Pure/ML/ml_context.ML
changeset 57832 5b48f2047c24
parent 56434 7acc933bd7cc
child 57834 0d295e339f52
--- 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";