62978
|
1 |
(* Title: Pure/ML/ml_print_depth.ML
|
62878
|
2 |
Author: Makarius
|
|
3 |
|
|
4 |
Print depth for ML toplevel pp: context option with global default.
|
|
5 |
*)
|
|
6 |
|
|
7 |
signature ML_PRINT_DEPTH =
|
|
8 |
sig
|
|
9 |
val set_print_depth: int -> unit
|
|
10 |
val print_depth_raw: Config.raw
|
|
11 |
val print_depth: int Config.T
|
|
12 |
val get_print_depth: unit -> int
|
|
13 |
end;
|
|
14 |
|
|
15 |
structure ML_Print_Depth: ML_PRINT_DEPTH =
|
|
16 |
struct
|
|
17 |
|
|
18 |
val set_print_depth = ML_Print_Depth.set_print_depth;
|
|
19 |
|
|
20 |
val print_depth_raw =
|
64556
|
21 |
Config.declare ("ML_print_depth", \<^here>)
|
62878
|
22 |
(fn _ => Config.Int (ML_Print_Depth.get_print_depth ()));
|
|
23 |
|
|
24 |
val print_depth = Config.int print_depth_raw;
|
|
25 |
|
|
26 |
fun get_print_depth () =
|
62889
|
27 |
(case Context.get_generic_context () of
|
62878
|
28 |
NONE => ML_Print_Depth.get_print_depth ()
|
|
29 |
| SOME context => Config.get_generic context print_depth);
|
|
30 |
|
|
31 |
end;
|