clarified modules;
authorwenzelm
Thu Mar 17 13:44:18 2016 +0100 (2016-03-17)
changeset 62661c23ff2f45a18
parent 62660 285308563814
child 62662 291cc01f56f5
clarified modules;
src/Pure/ML/ml_options.ML
src/Pure/ML/ml_pretty.ML
src/Pure/ROOT.ML
src/Pure/Tools/ml_process.scala
     1.1 --- a/src/Pure/ML/ml_options.ML	Thu Mar 17 12:32:12 2016 +0100
     1.2 +++ b/src/Pure/ML/ml_options.ML	Thu Mar 17 13:44:18 2016 +0100
     1.3 @@ -66,12 +66,12 @@
     1.4  (* print depth *)
     1.5  
     1.6  val print_depth_raw =
     1.7 -  Config.declare ("ML_print_depth", @{here}) (fn _ => Config.Int (get_default_print_depth ()));
     1.8 +  Config.declare ("ML_print_depth", @{here}) (fn _ => Config.Int (ML_Pretty.get_print_depth ()));
     1.9  val print_depth = Config.int print_depth_raw;
    1.10  
    1.11  fun get_print_depth () =
    1.12    (case Context.thread_data () of
    1.13 -    NONE => get_default_print_depth ()
    1.14 +    NONE => ML_Pretty.get_print_depth ()
    1.15    | SOME context => Config.get_generic context print_depth);
    1.16  
    1.17  fun get_print_depth_default default =
     2.1 --- a/src/Pure/ML/ml_pretty.ML	Thu Mar 17 12:32:12 2016 +0100
     2.2 +++ b/src/Pure/ML/ml_pretty.ML	Thu Mar 17 13:44:18 2016 +0100
     2.3 @@ -17,11 +17,15 @@
     2.4    val enum: string -> string -> string -> ('a * int -> pretty) -> 'a list * int -> pretty
     2.5    val to_polyml: pretty -> PolyML.pretty
     2.6    val from_polyml: PolyML.pretty -> pretty
     2.7 +  val get_print_depth: unit -> int
     2.8 +  val print_depth: int -> unit
     2.9  end;
    2.10  
    2.11  structure ML_Pretty: ML_PRETTY =
    2.12  struct
    2.13  
    2.14 +(* datatype pretty *)
    2.15 +
    2.16  datatype pretty =
    2.17    Block of (string * string) * bool * FixedInt.int * pretty list |
    2.18    String of string * FixedInt.int |
    2.19 @@ -81,4 +85,15 @@
    2.20            String (s, FixedInt.fromInt (case Int.fromString len of SOME i => i | NONE => size s))
    2.21    in convert "" end;
    2.22  
    2.23 +
    2.24 +(* default print depth *)
    2.25 +
    2.26 +local
    2.27 +  val depth = Unsynchronized.ref 0;
    2.28 +in
    2.29 +  fun get_print_depth () = ! depth;
    2.30 +  fun print_depth n = (depth := n; PolyML.print_depth n);
    2.31 +  val _ = print_depth 10;
    2.32  end;
    2.33 +
    2.34 +end;
     3.1 --- a/src/Pure/ROOT.ML	Thu Mar 17 12:32:12 2016 +0100
     3.2 +++ b/src/Pure/ROOT.ML	Thu Mar 17 13:44:18 2016 +0100
     3.3 @@ -56,14 +56,6 @@
     3.4  
     3.5  use "ML/ml_pretty.ML";
     3.6  
     3.7 -local
     3.8 -  val depth = Unsynchronized.ref 10;
     3.9 -in
    3.10 -  fun get_default_print_depth () = ! depth;
    3.11 -  fun default_print_depth n = (depth := n; PolyML.print_depth n);
    3.12 -  val _ = default_print_depth 10;
    3.13 -end;
    3.14 -
    3.15  val error_depth = PolyML.error_depth;
    3.16  
    3.17  
     4.1 --- a/src/Pure/Tools/ml_process.scala	Thu Mar 17 12:32:12 2016 +0100
     4.2 +++ b/src/Pure/Tools/ml_process.scala	Thu Mar 17 13:44:18 2016 +0100
     4.3 @@ -75,9 +75,9 @@
     4.4        else
     4.5          channel match {
     4.6            case None =>
     4.7 -            List("(default_print_depth 10; Isabelle_Process.init_options ())")
     4.8 +            List("(ML_Pretty.print_depth 10; Isabelle_Process.init_options ())")
     4.9            case Some(ch) =>
    4.10 -            List("(default_print_depth 10; Isabelle_Process.init_protocol " +
    4.11 +            List("(ML_Pretty.print_depth 10; Isabelle_Process.init_protocol " +
    4.12                ML_Syntax.print_string0(ch.server_name) + ")")
    4.13          }
    4.14