explicit print_depth for the sake of Spec_Check.determine_type;
authorwenzelm
Sat Mar 26 16:14:46 2016 +0100 (2016-03-26)
changeset 62716d80b9f4990e4
parent 62715 8312e5d8d217
child 62717 8adf274f5988
explicit print_depth for the sake of Spec_Check.determine_type;
src/Pure/ML/ml_compiler0.ML
src/Pure/ML/ml_env.ML
src/Pure/ROOT.ML
src/Tools/Code/code_runtime.ML
src/Tools/Spec_Check/spec_check.ML
     1.1 --- a/src/Pure/ML/ml_compiler0.ML	Sat Mar 26 14:27:58 2016 +0100
     1.2 +++ b/src/Pure/ML/ml_compiler0.ML	Sat Mar 26 16:14:46 2016 +0100
     1.3 @@ -8,6 +8,7 @@
     1.4  sig
     1.5    type context =
     1.6     {name_space: ML_Name_Space.T,
     1.7 +    print_depth: int option,
     1.8      here: int -> string -> string,
     1.9      print: string -> unit,
    1.10      error: string -> unit}
    1.11 @@ -23,6 +24,7 @@
    1.12  
    1.13  type context =
    1.14   {name_space: ML_Name_Space.T,
    1.15 +  print_depth: int option,
    1.16    here: int -> string -> string,
    1.17    print: string -> unit,
    1.18    error: string -> unit};
    1.19 @@ -45,7 +47,8 @@
    1.20        | input _ [] res = rev res;
    1.21    in String.concat (input start_line (String.explode txt) []) end;
    1.22  
    1.23 -fun use_text ({name_space, here, print, error, ...}: context) {line, file, verbose, debug} text =
    1.24 +fun use_text ({name_space, print_depth, here, print, error, ...}: context)
    1.25 +    {line, file, verbose, debug} text =
    1.26    let
    1.27      val current_line = Unsynchronized.ref line;
    1.28      val in_buffer = Unsynchronized.ref (String.explode (ml_input line file text));
    1.29 @@ -71,7 +74,8 @@
    1.30        PolyML.Compiler.CPLineNo (fn () => ! current_line),
    1.31        PolyML.Compiler.CPFileName file,
    1.32        PolyML.Compiler.CPPrintInAlphabeticalOrder false,
    1.33 -      PolyML.Compiler.CPDebug debug];
    1.34 +      PolyML.Compiler.CPDebug debug] @
    1.35 +     (case print_depth of NONE => [] | SOME d => [PolyML.Compiler.CPPrintDepth (fn () => d)]);
    1.36      val _ =
    1.37        (while not (List.null (! in_buffer)) do
    1.38          PolyML.compiler (get, parameters) ())
    1.39 @@ -101,6 +105,7 @@
    1.40    let
    1.41      val context: ML_Compiler0.context =
    1.42       {name_space = ML_Name_Space.global,
    1.43 +      print_depth = NONE,
    1.44        here = fn line => fn file => " (line " ^ Int.toString line ^ " of \"" ^ file ^ "\")",
    1.45        print = fn s => (TextIO.output (TextIO.stdOut, s ^ "\n"); TextIO.flushOut TextIO.stdOut),
    1.46        error = fn s => error s};
     2.1 --- a/src/Pure/ML/ml_env.ML	Sat Mar 26 14:27:58 2016 +0100
     2.2 +++ b/src/Pure/ML/ml_env.ML	Sat Mar 26 16:14:46 2016 +0100
     2.3 @@ -164,6 +164,7 @@
     2.4  
     2.5  val context: ML_Compiler0.context =
     2.6   {name_space = make_name_space {SML = false, exchange = false},
     2.7 +  print_depth = NONE,
     2.8    here = Position.here oo Position.line_file,
     2.9    print = writeln,
    2.10    error = error};
     3.1 --- a/src/Pure/ROOT.ML	Sat Mar 26 14:27:58 2016 +0100
     3.2 +++ b/src/Pure/ROOT.ML	Sat Mar 26 16:14:46 2016 +0100
     3.3 @@ -105,6 +105,7 @@
     3.4    let
     3.5      val context: ML_Compiler0.context =
     3.6       {name_space = ML_Name_Space.global,
     3.7 +      print_depth = NONE,
     3.8        here = Position.here oo Position.line_file,
     3.9        print = writeln,
    3.10        error = error};
     4.1 --- a/src/Tools/Code/code_runtime.ML	Sat Mar 26 14:27:58 2016 +0100
     4.2 +++ b/src/Tools/Code/code_runtime.ML	Sat Mar 26 16:14:46 2016 +0100
     4.3 @@ -524,6 +524,7 @@
     4.4      allStruct    = #allStruct ML_Env.name_space,
     4.5      allSig       = #allSig ML_Env.name_space,
     4.6      allFunct     = #allFunct ML_Env.name_space},
     4.7 +  print_depth = NONE,
     4.8    here = #here ML_Env.context,
     4.9    print = #print ML_Env.context,
    4.10    error = #error ML_Env.context};
     5.1 --- a/src/Tools/Spec_Check/spec_check.ML	Sat Mar 26 14:27:58 2016 +0100
     5.2 +++ b/src/Tools/Spec_Check/spec_check.ML	Sat Mar 26 16:14:46 2016 +0100
     5.3 @@ -129,6 +129,7 @@
     5.4      val return = Unsynchronized.ref "return"
     5.5      val context : ML_Compiler0.context =
     5.6       {name_space = #name_space ML_Env.context,
     5.7 +      print_depth = SOME 1000000,
     5.8        here = #here ML_Env.context,
     5.9        print = fn r => return := r,
    5.10        error = #error ML_Env.context}