src/Pure/ML/ml_print_depth.ML
author wenzelm
Sat Nov 04 15:24:40 2017 +0100 (20 months ago)
changeset 67003 49850a679c2c
parent 64556 851ae0e7b09c
child 69575 f77cc54f6d47
permissions -rw-r--r--
more robust sorted_entries;
wenzelm@62978
     1
(*  Title:      Pure/ML/ml_print_depth.ML
wenzelm@62878
     2
    Author:     Makarius
wenzelm@62878
     3
wenzelm@62878
     4
Print depth for ML toplevel pp: context option with global default.
wenzelm@62878
     5
*)
wenzelm@62878
     6
wenzelm@62878
     7
signature ML_PRINT_DEPTH =
wenzelm@62878
     8
sig
wenzelm@62878
     9
  val set_print_depth: int -> unit
wenzelm@62878
    10
  val print_depth_raw: Config.raw
wenzelm@62878
    11
  val print_depth: int Config.T
wenzelm@62878
    12
  val get_print_depth: unit -> int
wenzelm@62878
    13
end;
wenzelm@62878
    14
wenzelm@62878
    15
structure ML_Print_Depth: ML_PRINT_DEPTH =
wenzelm@62878
    16
struct
wenzelm@62878
    17
wenzelm@62878
    18
val set_print_depth = ML_Print_Depth.set_print_depth;
wenzelm@62878
    19
wenzelm@62878
    20
val print_depth_raw =
wenzelm@64556
    21
  Config.declare ("ML_print_depth", \<^here>)
wenzelm@62878
    22
    (fn _ => Config.Int (ML_Print_Depth.get_print_depth ()));
wenzelm@62878
    23
wenzelm@62878
    24
val print_depth = Config.int print_depth_raw;
wenzelm@62878
    25
wenzelm@62878
    26
fun get_print_depth () =
wenzelm@62889
    27
  (case Context.get_generic_context () of
wenzelm@62878
    28
    NONE => ML_Print_Depth.get_print_depth ()
wenzelm@62878
    29
  | SOME context => Config.get_generic context print_depth);
wenzelm@62878
    30
wenzelm@62878
    31
end;