explicit print_depth for the sake of Spec_Check.determine_type;

--- a/src/Pure/ML/ml_compiler0.ML	Sat Mar 26 14:27:58 2016 +0100
+++ b/src/Pure/ML/ml_compiler0.ML	Sat Mar 26 16:14:46 2016 +0100
@@ -8,6 +8,7 @@
 sig
   type context =
    {name_space: ML_Name_Space.T,
+    print_depth: int option,
     here: int -> string -> string,
     print: string -> unit,
     error: string -> unit}
@@ -23,6 +24,7 @@
 
 type context =
  {name_space: ML_Name_Space.T,
+  print_depth: int option,
   here: int -> string -> string,
   print: string -> unit,
   error: string -> unit};
@@ -45,7 +47,8 @@
       | input _ [] res = rev res;
   in String.concat (input start_line (String.explode txt) []) end;
 
-fun use_text ({name_space, here, print, error, ...}: context) {line, file, verbose, debug} text =
+fun use_text ({name_space, print_depth, here, print, error, ...}: context)
+    {line, file, verbose, debug} text =
   let
     val current_line = Unsynchronized.ref line;
     val in_buffer = Unsynchronized.ref (String.explode (ml_input line file text));
@@ -71,7 +74,8 @@
       PolyML.Compiler.CPLineNo (fn () => ! current_line),
       PolyML.Compiler.CPFileName file,
       PolyML.Compiler.CPPrintInAlphabeticalOrder false,
-      PolyML.Compiler.CPDebug debug];
+      PolyML.Compiler.CPDebug debug] @
+     (case print_depth of NONE => [] | SOME d => [PolyML.Compiler.CPPrintDepth (fn () => d)]);
     val _ =
       (while not (List.null (! in_buffer)) do
         PolyML.compiler (get, parameters) ())
@@ -101,6 +105,7 @@
   let
     val context: ML_Compiler0.context =
      {name_space = ML_Name_Space.global,
+      print_depth = NONE,
       here = fn line => fn file => " (line " ^ Int.toString line ^ " of \"" ^ file ^ "\")",
       print = fn s => (TextIO.output (TextIO.stdOut, s ^ "\n"); TextIO.flushOut TextIO.stdOut),
       error = fn s => error s};

--- a/src/Pure/ML/ml_env.ML	Sat Mar 26 14:27:58 2016 +0100
+++ b/src/Pure/ML/ml_env.ML	Sat Mar 26 16:14:46 2016 +0100
@@ -164,6 +164,7 @@
 
 val context: ML_Compiler0.context =
  {name_space = make_name_space {SML = false, exchange = false},
+  print_depth = NONE,
   here = Position.here oo Position.line_file,
   print = writeln,
   error = error};

--- a/src/Pure/ROOT.ML	Sat Mar 26 14:27:58 2016 +0100
+++ b/src/Pure/ROOT.ML	Sat Mar 26 16:14:46 2016 +0100
@@ -105,6 +105,7 @@
   let
     val context: ML_Compiler0.context =
      {name_space = ML_Name_Space.global,
+      print_depth = NONE,
       here = Position.here oo Position.line_file,
       print = writeln,
       error = error};

--- a/src/Tools/Code/code_runtime.ML	Sat Mar 26 14:27:58 2016 +0100
+++ b/src/Tools/Code/code_runtime.ML	Sat Mar 26 16:14:46 2016 +0100
@@ -524,6 +524,7 @@
     allStruct    = #allStruct ML_Env.name_space,
     allSig       = #allSig ML_Env.name_space,
     allFunct     = #allFunct ML_Env.name_space},
+  print_depth = NONE,
   here = #here ML_Env.context,
   print = #print ML_Env.context,
   error = #error ML_Env.context};

--- a/src/Tools/Spec_Check/spec_check.ML	Sat Mar 26 14:27:58 2016 +0100
+++ b/src/Tools/Spec_Check/spec_check.ML	Sat Mar 26 16:14:46 2016 +0100
@@ -129,6 +129,7 @@
     val return = Unsynchronized.ref "return"
     val context : ML_Compiler0.context =
      {name_space = #name_space ML_Env.context,
+      print_depth = SOME 1000000,
       here = #here ML_Env.context,
       print = fn r => return := r,
       error = #error ML_Env.context}