clarified modules -- simplified bootstrap;
authorwenzelm
Tue Apr 05 20:51:37 2016 +0200 (2016-04-05)
changeset 628781cec457e0a03
parent 62877 741560a5283b
child 62879 4764473c9b8d
clarified modules -- simplified bootstrap;
src/Pure/Isar/attrib.ML
src/Pure/Isar/runtime.ML
src/Pure/ML/ml_compiler.ML
src/Pure/ML/ml_context.ML
src/Pure/ML/ml_options.ML
src/Pure/ML/ml_pretty.ML
src/Pure/ML/ml_print_depth.ML
src/Pure/ML/ml_print_depth0.ML
src/Pure/ROOT.ML
src/Pure/System/isabelle_process.ML
src/Pure/System/options.ML
src/Pure/Tools/debugger.ML
     1.1 --- a/src/Pure/Isar/attrib.ML	Tue Apr 05 20:05:05 2016 +0200
     1.2 +++ b/src/Pure/Isar/attrib.ML	Tue Apr 05 20:51:37 2016 +0200
     1.3 @@ -515,11 +515,11 @@
     1.4    register_config Name_Space.names_long_raw #>
     1.5    register_config Name_Space.names_short_raw #>
     1.6    register_config Name_Space.names_unique_raw #>
     1.7 +  register_config ML_Print_Depth.print_depth_raw #>
     1.8    register_config ML_Options.source_trace_raw #>
     1.9    register_config ML_Options.exception_trace_raw #>
    1.10    register_config ML_Options.exception_debugger_raw #>
    1.11    register_config ML_Options.debugger_raw #>
    1.12 -  register_config ML_Options.print_depth_raw #>
    1.13    register_config Proof_Context.show_abbrevs_raw #>
    1.14    register_config Goal_Display.goals_limit_raw #>
    1.15    register_config Goal_Display.show_main_goal_raw #>
     2.1 --- a/src/Pure/Isar/runtime.ML	Tue Apr 05 20:05:05 2016 +0200
     2.2 +++ b/src/Pure/Isar/runtime.ML	Tue Apr 05 20:51:37 2016 +0200
     2.3 @@ -43,7 +43,7 @@
     2.4  fun pretty_exn (exn: exn) =
     2.5    Pretty.from_ML
     2.6      (ML_Pretty.from_polyml
     2.7 -      (ML_system_pretty (exn, FixedInt.fromInt (ML_Options.get_print_depth ()))));
     2.8 +      (ML_system_pretty (exn, FixedInt.fromInt (ML_Print_Depth.get_print_depth ()))));
     2.9  
    2.10  
    2.11  (* exn_context *)
     3.1 --- a/src/Pure/ML/ml_compiler.ML	Tue Apr 05 20:05:05 2016 +0200
     3.2 +++ b/src/Pure/ML/ml_compiler.ML	Tue Apr 05 20:51:37 2016 +0200
     3.3 @@ -199,7 +199,7 @@
     3.4  
     3.5      (* results *)
     3.6  
     3.7 -    val depth = FixedInt.fromInt (ML_Options.get_print_depth ());
     3.8 +    val depth = FixedInt.fromInt (ML_Print_Depth.get_print_depth ());
     3.9  
    3.10      fun apply_result {fixes, types, signatures, structures, functors, values} =
    3.11        let
    3.12 @@ -258,7 +258,7 @@
    3.13        PolyML.Compiler.CPLineNo (the_default 0 o Position.line_of o get_pos),
    3.14        PolyML.Compiler.CPLineOffset (the_default 0 o Position.offset_of o get_pos),
    3.15        PolyML.Compiler.CPFileName location_props,
    3.16 -      PolyML.Compiler.CPPrintDepth ML_Options.get_print_depth,
    3.17 +      PolyML.Compiler.CPPrintDepth ML_Print_Depth.get_print_depth,
    3.18        PolyML.Compiler.CPCompilerResultFun result_fun,
    3.19        PolyML.Compiler.CPPrintInAlphabeticalOrder false,
    3.20        PolyML.Compiler.CPDebug debug];
     4.1 --- a/src/Pure/ML/ml_context.ML	Tue Apr 05 20:05:05 2016 +0200
     4.2 +++ b/src/Pure/ML/ml_context.ML	Tue Apr 05 20:51:37 2016 +0200
     4.3 @@ -118,8 +118,8 @@
     4.4       \val ML_context = Context_Position.set_visible " ^ Bool.toString visible ^
     4.5       " (Context.the_local_context ());\n\
     4.6       \val ML_print_depth =\n\
     4.7 -     \  let val default = ML_Options.get_print_depth ()\n\
     4.8 -     \  in fn () => ML_Options.get_print_depth_default default end;\n"),
     4.9 +     \  let val default = ML_Print_Depth.get_print_depth ()\n\
    4.10 +     \  in fn () => ML_Print_Depth.get_print_depth_default default end;\n"),
    4.11     ML_Lex.tokenize "end;");
    4.12  
    4.13  fun reset_env name = ML_Lex.tokenize ("structure " ^ name ^ " = struct end");
     5.1 --- a/src/Pure/ML/ml_options.ML	Tue Apr 05 20:05:05 2016 +0200
     5.2 +++ b/src/Pure/ML/ml_options.ML	Tue Apr 05 20:51:37 2016 +0200
     5.3 @@ -17,10 +17,6 @@
     5.4    val debugger_raw: Config.raw
     5.5    val debugger: bool Config.T
     5.6    val debugger_enabled: Context.generic option -> bool
     5.7 -  val print_depth_raw: Config.raw
     5.8 -  val print_depth: int Config.T
     5.9 -  val get_print_depth: unit -> int
    5.10 -  val get_print_depth_default: int -> int
    5.11  end;
    5.12  
    5.13  structure ML_Options: ML_OPTIONS =
    5.14 @@ -62,21 +58,4 @@
    5.15        (Options.default_bool (Config.name_of debugger_raw) handle ERROR _ => false)
    5.16    | debugger_enabled (SOME context) = Config.get_generic context debugger;
    5.17  
    5.18 -
    5.19 -(* print depth *)
    5.20 -
    5.21 -val print_depth_raw =
    5.22 -  Config.declare ("ML_print_depth", @{here}) (fn _ => Config.Int (ML_Pretty.get_print_depth ()));
    5.23 -val print_depth = Config.int print_depth_raw;
    5.24 -
    5.25 -fun get_print_depth () =
    5.26 -  (case Context.thread_data () of
    5.27 -    NONE => ML_Pretty.get_print_depth ()
    5.28 -  | SOME context => Config.get_generic context print_depth);
    5.29 -
    5.30 -fun get_print_depth_default default =
    5.31 -  (case Context.thread_data () of
    5.32 -    NONE => default
    5.33 -  | SOME context => Config.get_generic context print_depth);
    5.34 -
    5.35  end;
     6.1 --- a/src/Pure/ML/ml_pretty.ML	Tue Apr 05 20:05:05 2016 +0200
     6.2 +++ b/src/Pure/ML/ml_pretty.ML	Tue Apr 05 20:51:37 2016 +0200
     6.3 @@ -19,8 +19,6 @@
     6.4      'a list * FixedInt.int -> pretty
     6.5    val to_polyml: pretty -> PolyML_Pretty.pretty
     6.6    val from_polyml: PolyML_Pretty.pretty -> pretty
     6.7 -  val get_print_depth: unit -> int
     6.8 -  val print_depth: int -> unit
     6.9    val format_polyml: int -> PolyML_Pretty.pretty -> string
    6.10    val format: int -> pretty -> string
    6.11    val make_string_fn: string -> string
    6.12 @@ -91,16 +89,6 @@
    6.13    in convert "" end;
    6.14  
    6.15  
    6.16 -(* default print depth *)
    6.17 -
    6.18 -local
    6.19 -  val depth = Unsynchronized.ref 0;
    6.20 -in
    6.21 -  fun get_print_depth () = ! depth;
    6.22 -  fun print_depth n = (depth := n; PolyML.print_depth n);
    6.23 -end;
    6.24 -
    6.25 -
    6.26  (* format *)
    6.27  
    6.28  fun format_polyml margin prt =
    6.29 @@ -123,8 +111,8 @@
    6.30    if local_env <> "" then
    6.31      pretty_string_of (pretty_value (local_env ^ ".ML_print_depth ()"))
    6.32    else if List.exists (fn (a, _) => a = "Pretty") (#allStruct ML_Name_Space.global ()) then
    6.33 -    pretty_string_of (pretty_value "ML_Pretty.get_print_depth ()")
    6.34 -  else "(fn x => ML_Pretty.format_polyml 78 (" ^ pretty_value "ML_Pretty.get_print_depth ()" ^ "))";
    6.35 +    pretty_string_of (pretty_value "ML_Print_Depth.get_print_depth ()")
    6.36 +  else "(fn x => ML_Pretty.format_polyml 78 (" ^ pretty_value "ML_Print_Depth.get_print_depth ()" ^ "))";
    6.37  
    6.38  end;
    6.39  
     7.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.2 +++ b/src/Pure/ML/ml_print_depth.ML	Tue Apr 05 20:51:37 2016 +0200
     7.3 @@ -0,0 +1,37 @@
     7.4 +(*  Title:      Pure/ML/ml_print_depth0.ML
     7.5 +    Author:     Makarius
     7.6 +
     7.7 +Print depth for ML toplevel pp: context option with global default.
     7.8 +*)
     7.9 +
    7.10 +signature ML_PRINT_DEPTH =
    7.11 +sig
    7.12 +  val set_print_depth: int -> unit
    7.13 +  val print_depth_raw: Config.raw
    7.14 +  val print_depth: int Config.T
    7.15 +  val get_print_depth: unit -> int
    7.16 +  val get_print_depth_default: int -> int
    7.17 +end;
    7.18 +
    7.19 +structure ML_Print_Depth: ML_PRINT_DEPTH =
    7.20 +struct
    7.21 +
    7.22 +val set_print_depth = ML_Print_Depth.set_print_depth;
    7.23 +
    7.24 +val print_depth_raw =
    7.25 +  Config.declare ("ML_print_depth", @{here})
    7.26 +    (fn _ => Config.Int (ML_Print_Depth.get_print_depth ()));
    7.27 +
    7.28 +val print_depth = Config.int print_depth_raw;
    7.29 +
    7.30 +fun get_print_depth () =
    7.31 +  (case Context.thread_data () of
    7.32 +    NONE => ML_Print_Depth.get_print_depth ()
    7.33 +  | SOME context => Config.get_generic context print_depth);
    7.34 +
    7.35 +fun get_print_depth_default default =
    7.36 +  (case Context.thread_data () of
    7.37 +    NONE => default
    7.38 +  | SOME context => Config.get_generic context print_depth);
    7.39 +
    7.40 +end;
     8.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.2 +++ b/src/Pure/ML/ml_print_depth0.ML	Tue Apr 05 20:51:37 2016 +0200
     8.3 @@ -0,0 +1,23 @@
     8.4 +(*  Title:      Pure/ML/ml_print_depth0.ML
     8.5 +    Author:     Makarius
     8.6 +
     8.7 +Print depth for ML toplevel pp -- global default (unsynchronized).
     8.8 +*)
     8.9 +
    8.10 +signature ML_PRINT_DEPTH =
    8.11 +sig
    8.12 +  val set_print_depth: int -> unit
    8.13 +  val get_print_depth: unit -> int
    8.14 +  val get_print_depth_default: int -> int
    8.15 +end;
    8.16 +
    8.17 +structure ML_Print_Depth: ML_PRINT_DEPTH =
    8.18 +struct
    8.19 +
    8.20 +val depth = Unsynchronized.ref 0;
    8.21 +
    8.22 +fun set_print_depth n = (depth := n; PolyML.print_depth n);
    8.23 +fun get_print_depth () = ! depth;
    8.24 +fun get_print_depth_default _ = ! depth;
    8.25 +
    8.26 +end;
     9.1 --- a/src/Pure/ROOT.ML	Tue Apr 05 20:05:05 2016 +0200
     9.2 +++ b/src/Pure/ROOT.ML	Tue Apr 05 20:51:37 2016 +0200
     9.3 @@ -23,6 +23,7 @@
     9.4  
     9.5  use "ML/ml_heap.ML";
     9.6  use "ML/ml_profiling.ML";
     9.7 +use "ML/ml_print_depth0.ML";
     9.8  use "ML/ml_pretty.ML";
     9.9  use "ML/ml_compiler0.ML";
    9.10  use_no_debug "ML/ml_debugger.ML";
    9.11 @@ -185,6 +186,7 @@
    9.12  use "ML/ml_syntax.ML";
    9.13  use "ML/ml_env.ML";
    9.14  use "ML/ml_options.ML";
    9.15 +use "ML/ml_print_depth.ML";
    9.16  use_no_debug "ML/exn_debugger.ML";
    9.17  use_no_debug "Isar/runtime.ML";
    9.18  use "PIDE/execution.ML";
    10.1 --- a/src/Pure/System/isabelle_process.ML	Tue Apr 05 20:05:05 2016 +0200
    10.2 +++ b/src/Pure/System/isabelle_process.ML	Tue Apr 05 20:51:37 2016 +0200
    10.3 @@ -209,7 +209,7 @@
    10.4  (* init options *)
    10.5  
    10.6  fun init_options () =
    10.7 - (ML_Pretty.print_depth (Options.default_int "ML_print_depth");
    10.8 + (ML_Print_Depth.set_print_depth (Options.default_int "ML_print_depth");
    10.9    Future.ML_statistics := Options.default_bool "ML_statistics";
   10.10    Multithreading.trace := Options.default_int "threads_trace";
   10.11    Multithreading.max_threads_update (Options.default_int "threads");
    11.1 --- a/src/Pure/System/options.ML	Tue Apr 05 20:05:05 2016 +0200
    11.2 +++ b/src/Pure/System/options.ML	Tue Apr 05 20:51:37 2016 +0200
    11.3 @@ -222,6 +222,6 @@
    11.4        end);
    11.5  
    11.6  val _ = load_default ();
    11.7 -val _ = ML_Pretty.print_depth (default_int "ML_print_depth");
    11.8 +val _ = ML_Print_Depth.set_print_depth (default_int "ML_print_depth");
    11.9  
   11.10  end;
    12.1 --- a/src/Pure/Tools/debugger.ML	Tue Apr 05 20:05:05 2016 +0200
    12.2 +++ b/src/Pure/Tools/debugger.ML	Tue Apr 05 20:51:37 2016 +0200
    12.3 @@ -190,7 +190,7 @@
    12.4  
    12.5      fun print x =
    12.6        Pretty.from_polyml
    12.7 -        (ML_Name_Space.displayVal (x, FixedInt.fromInt (ML_Options.get_print_depth ()), space));
    12.8 +        (ML_Name_Space.displayVal (x, FixedInt.fromInt (ML_Print_Depth.get_print_depth ()), space));
    12.9      fun print_all () =
   12.10        #allVal (ML_Debugger.debug_local_name_space (the_debug_state thread_name index)) ()
   12.11        |> sort_by #1 |> map (Pretty.item o single o print o #2)