diff -r f7de8392a507 -r 03c3d1a7c3b8 src/Pure/ML/ml_compiler.ML
--- a/src/Pure/ML/ml_compiler.ML	Tue Mar 25 17:59:34 2014 +0100
+++ b/src/Pure/ML/ml_compiler.ML	Tue Mar 25 19:03:02 2014 +0100
@@ -11,6 +11,9 @@
   val exn_message: exn -> string
   val exn_error_message: exn -> unit
   val exn_trace: (unit -> 'a) -> 'a
+  val print_depth_raw: Config.raw
+  val print_depth: int Config.T
+  val get_print_depth: unit -> int
   type flags = {SML: bool, verbose: bool}
   val eval: flags -> Position.T -> ML_Lex.token list -> unit
 end
@@ -18,6 +21,8 @@
 structure ML_Compiler: ML_COMPILER =
 struct
 
+(* exceptions *)
+
 val exn_info =
  {exn_position = fn _: exn => Position.none,
   pretty_exn = Pretty.str o General.exnMessage};
@@ -29,6 +34,21 @@
 val exn_error_message = Output.error_message o exn_message;
 fun exn_trace e = print_exception_trace exn_message e;
 
+
+(* print depth *)
+
+val print_depth_raw =
+  Config.declare "ML_print_depth" (fn _ => Config.Int (get_default_print_depth ()));
+val print_depth = Config.int print_depth_raw;
+
+fun get_print_depth () =
+  (case Context.thread_data () of
+    NONE => get_default_print_depth ()
+  | SOME context => Config.get_generic context print_depth);
+
+
+(* eval *)
+
 type flags = {SML: bool, verbose: bool};
 
 fun eval {SML, verbose} pos toks =