src/Pure/ML/ml_compiler0.ML
changeset 62716 d80b9f4990e4
parent 62668 360d3464919c
child 62817 744bfd770123
     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};