src/Pure/ML/ml_pretty.ML
changeset 62661 c23ff2f45a18
parent 62508 d0b68218ea55
child 62662 291cc01f56f5
     1.1 --- a/src/Pure/ML/ml_pretty.ML	Thu Mar 17 12:32:12 2016 +0100
     1.2 +++ b/src/Pure/ML/ml_pretty.ML	Thu Mar 17 13:44:18 2016 +0100
     1.3 @@ -17,11 +17,15 @@
     1.4    val enum: string -> string -> string -> ('a * int -> pretty) -> 'a list * int -> pretty
     1.5    val to_polyml: pretty -> PolyML.pretty
     1.6    val from_polyml: PolyML.pretty -> pretty
     1.7 +  val get_print_depth: unit -> int
     1.8 +  val print_depth: int -> unit
     1.9  end;
    1.10  
    1.11  structure ML_Pretty: ML_PRETTY =
    1.12  struct
    1.13  
    1.14 +(* datatype pretty *)
    1.15 +
    1.16  datatype pretty =
    1.17    Block of (string * string) * bool * FixedInt.int * pretty list |
    1.18    String of string * FixedInt.int |
    1.19 @@ -81,4 +85,15 @@
    1.20            String (s, FixedInt.fromInt (case Int.fromString len of SOME i => i | NONE => size s))
    1.21    in convert "" end;
    1.22  
    1.23 +
    1.24 +(* default print depth *)
    1.25 +
    1.26 +local
    1.27 +  val depth = Unsynchronized.ref 0;
    1.28 +in
    1.29 +  fun get_print_depth () = ! depth;
    1.30 +  fun print_depth n = (depth := n; PolyML.print_depth n);
    1.31 +  val _ = print_depth 10;
    1.32  end;
    1.33 +
    1.34 +end;