# HG changeset patch # User wenzelm # Date 1459882297 -7200 # Node ID 1cec457e0a0375b7db8db6db679f46e57af4c1a1 # Parent 741560a5283b9968e9f3d83ba54dea37a9aa4b0f clarified modules -- simplified bootstrap; diff -r 741560a5283b -r 1cec457e0a03 src/Pure/Isar/attrib.ML --- a/src/Pure/Isar/attrib.ML Tue Apr 05 20:05:05 2016 +0200 +++ b/src/Pure/Isar/attrib.ML Tue Apr 05 20:51:37 2016 +0200 @@ -515,11 +515,11 @@ register_config Name_Space.names_long_raw #> register_config Name_Space.names_short_raw #> register_config Name_Space.names_unique_raw #> + register_config ML_Print_Depth.print_depth_raw #> register_config ML_Options.source_trace_raw #> register_config ML_Options.exception_trace_raw #> register_config ML_Options.exception_debugger_raw #> register_config ML_Options.debugger_raw #> - register_config ML_Options.print_depth_raw #> register_config Proof_Context.show_abbrevs_raw #> register_config Goal_Display.goals_limit_raw #> register_config Goal_Display.show_main_goal_raw #> diff -r 741560a5283b -r 1cec457e0a03 src/Pure/Isar/runtime.ML --- a/src/Pure/Isar/runtime.ML Tue Apr 05 20:05:05 2016 +0200 +++ b/src/Pure/Isar/runtime.ML Tue Apr 05 20:51:37 2016 +0200 @@ -43,7 +43,7 @@ fun pretty_exn (exn: exn) = Pretty.from_ML (ML_Pretty.from_polyml - (ML_system_pretty (exn, FixedInt.fromInt (ML_Options.get_print_depth ())))); + (ML_system_pretty (exn, FixedInt.fromInt (ML_Print_Depth.get_print_depth ())))); (* exn_context *) diff -r 741560a5283b -r 1cec457e0a03 src/Pure/ML/ml_compiler.ML --- a/src/Pure/ML/ml_compiler.ML Tue Apr 05 20:05:05 2016 +0200 +++ b/src/Pure/ML/ml_compiler.ML Tue Apr 05 20:51:37 2016 +0200 @@ -199,7 +199,7 @@ (* results *) - val depth = FixedInt.fromInt (ML_Options.get_print_depth ()); + val depth = FixedInt.fromInt (ML_Print_Depth.get_print_depth ()); fun apply_result {fixes, types, signatures, structures, functors, values} = let @@ -258,7 +258,7 @@ PolyML.Compiler.CPLineNo (the_default 0 o Position.line_of o get_pos), PolyML.Compiler.CPLineOffset (the_default 0 o Position.offset_of o get_pos), PolyML.Compiler.CPFileName location_props, - PolyML.Compiler.CPPrintDepth ML_Options.get_print_depth, + PolyML.Compiler.CPPrintDepth ML_Print_Depth.get_print_depth, PolyML.Compiler.CPCompilerResultFun result_fun, PolyML.Compiler.CPPrintInAlphabeticalOrder false, PolyML.Compiler.CPDebug debug]; diff -r 741560a5283b -r 1cec457e0a03 src/Pure/ML/ml_context.ML --- a/src/Pure/ML/ml_context.ML Tue Apr 05 20:05:05 2016 +0200 +++ b/src/Pure/ML/ml_context.ML Tue Apr 05 20:51:37 2016 +0200 @@ -118,8 +118,8 @@ \val ML_context = Context_Position.set_visible " ^ Bool.toString visible ^ " (Context.the_local_context ());\n\ \val ML_print_depth =\n\ - \ let val default = ML_Options.get_print_depth ()\n\ - \ in fn () => ML_Options.get_print_depth_default default end;\n"), + \ let val default = ML_Print_Depth.get_print_depth ()\n\ + \ in fn () => ML_Print_Depth.get_print_depth_default default end;\n"), ML_Lex.tokenize "end;"); fun reset_env name = ML_Lex.tokenize ("structure " ^ name ^ " = struct end"); diff -r 741560a5283b -r 1cec457e0a03 src/Pure/ML/ml_options.ML --- a/src/Pure/ML/ml_options.ML Tue Apr 05 20:05:05 2016 +0200 +++ b/src/Pure/ML/ml_options.ML Tue Apr 05 20:51:37 2016 +0200 @@ -17,10 +17,6 @@ val debugger_raw: Config.raw val debugger: bool Config.T val debugger_enabled: Context.generic option -> bool - val print_depth_raw: Config.raw - val print_depth: int Config.T - val get_print_depth: unit -> int - val get_print_depth_default: int -> int end; structure ML_Options: ML_OPTIONS = @@ -62,21 +58,4 @@ (Options.default_bool (Config.name_of debugger_raw) handle ERROR _ => false) | debugger_enabled (SOME context) = Config.get_generic context debugger; - -(* print depth *) - -val print_depth_raw = - Config.declare ("ML_print_depth", @{here}) (fn _ => Config.Int (ML_Pretty.get_print_depth ())); -val print_depth = Config.int print_depth_raw; - -fun get_print_depth () = - (case Context.thread_data () of - NONE => ML_Pretty.get_print_depth () - | SOME context => Config.get_generic context print_depth); - -fun get_print_depth_default default = - (case Context.thread_data () of - NONE => default - | SOME context => Config.get_generic context print_depth); - end; diff -r 741560a5283b -r 1cec457e0a03 src/Pure/ML/ml_pretty.ML --- a/src/Pure/ML/ml_pretty.ML Tue Apr 05 20:05:05 2016 +0200 +++ b/src/Pure/ML/ml_pretty.ML Tue Apr 05 20:51:37 2016 +0200 @@ -19,8 +19,6 @@ 'a list * FixedInt.int -> pretty val to_polyml: pretty -> PolyML_Pretty.pretty val from_polyml: PolyML_Pretty.pretty -> pretty - val get_print_depth: unit -> int - val print_depth: int -> unit val format_polyml: int -> PolyML_Pretty.pretty -> string val format: int -> pretty -> string val make_string_fn: string -> string @@ -91,16 +89,6 @@ in convert "" end; -(* default print depth *) - -local - val depth = Unsynchronized.ref 0; -in - fun get_print_depth () = ! depth; - fun print_depth n = (depth := n; PolyML.print_depth n); -end; - - (* format *) fun format_polyml margin prt = @@ -123,8 +111,8 @@ if local_env <> "" then pretty_string_of (pretty_value (local_env ^ ".ML_print_depth ()")) else if List.exists (fn (a, _) => a = "Pretty") (#allStruct ML_Name_Space.global ()) then - pretty_string_of (pretty_value "ML_Pretty.get_print_depth ()") - else "(fn x => ML_Pretty.format_polyml 78 (" ^ pretty_value "ML_Pretty.get_print_depth ()" ^ "))"; + pretty_string_of (pretty_value "ML_Print_Depth.get_print_depth ()") + else "(fn x => ML_Pretty.format_polyml 78 (" ^ pretty_value "ML_Print_Depth.get_print_depth ()" ^ "))"; end; diff -r 741560a5283b -r 1cec457e0a03 src/Pure/ML/ml_print_depth.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/ML/ml_print_depth.ML Tue Apr 05 20:51:37 2016 +0200 @@ -0,0 +1,37 @@ +(* Title: Pure/ML/ml_print_depth0.ML + Author: Makarius + +Print depth for ML toplevel pp: context option with global default. +*) + +signature ML_PRINT_DEPTH = +sig + val set_print_depth: int -> unit + val print_depth_raw: Config.raw + val print_depth: int Config.T + val get_print_depth: unit -> int + val get_print_depth_default: int -> int +end; + +structure ML_Print_Depth: ML_PRINT_DEPTH = +struct + +val set_print_depth = ML_Print_Depth.set_print_depth; + +val print_depth_raw = + Config.declare ("ML_print_depth", @{here}) + (fn _ => Config.Int (ML_Print_Depth.get_print_depth ())); + +val print_depth = Config.int print_depth_raw; + +fun get_print_depth () = + (case Context.thread_data () of + NONE => ML_Print_Depth.get_print_depth () + | SOME context => Config.get_generic context print_depth); + +fun get_print_depth_default default = + (case Context.thread_data () of + NONE => default + | SOME context => Config.get_generic context print_depth); + +end; diff -r 741560a5283b -r 1cec457e0a03 src/Pure/ML/ml_print_depth0.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/ML/ml_print_depth0.ML Tue Apr 05 20:51:37 2016 +0200 @@ -0,0 +1,23 @@ +(* Title: Pure/ML/ml_print_depth0.ML + Author: Makarius + +Print depth for ML toplevel pp -- global default (unsynchronized). +*) + +signature ML_PRINT_DEPTH = +sig + val set_print_depth: int -> unit + val get_print_depth: unit -> int + val get_print_depth_default: int -> int +end; + +structure ML_Print_Depth: ML_PRINT_DEPTH = +struct + +val depth = Unsynchronized.ref 0; + +fun set_print_depth n = (depth := n; PolyML.print_depth n); +fun get_print_depth () = ! depth; +fun get_print_depth_default _ = ! depth; + +end; diff -r 741560a5283b -r 1cec457e0a03 src/Pure/ROOT.ML --- a/src/Pure/ROOT.ML Tue Apr 05 20:05:05 2016 +0200 +++ b/src/Pure/ROOT.ML Tue Apr 05 20:51:37 2016 +0200 @@ -23,6 +23,7 @@ use "ML/ml_heap.ML"; use "ML/ml_profiling.ML"; +use "ML/ml_print_depth0.ML"; use "ML/ml_pretty.ML"; use "ML/ml_compiler0.ML"; use_no_debug "ML/ml_debugger.ML"; @@ -185,6 +186,7 @@ use "ML/ml_syntax.ML"; use "ML/ml_env.ML"; use "ML/ml_options.ML"; +use "ML/ml_print_depth.ML"; use_no_debug "ML/exn_debugger.ML"; use_no_debug "Isar/runtime.ML"; use "PIDE/execution.ML"; diff -r 741560a5283b -r 1cec457e0a03 src/Pure/System/isabelle_process.ML --- a/src/Pure/System/isabelle_process.ML Tue Apr 05 20:05:05 2016 +0200 +++ b/src/Pure/System/isabelle_process.ML Tue Apr 05 20:51:37 2016 +0200 @@ -209,7 +209,7 @@ (* init options *) fun init_options () = - (ML_Pretty.print_depth (Options.default_int "ML_print_depth"); + (ML_Print_Depth.set_print_depth (Options.default_int "ML_print_depth"); Future.ML_statistics := Options.default_bool "ML_statistics"; Multithreading.trace := Options.default_int "threads_trace"; Multithreading.max_threads_update (Options.default_int "threads"); diff -r 741560a5283b -r 1cec457e0a03 src/Pure/System/options.ML --- a/src/Pure/System/options.ML Tue Apr 05 20:05:05 2016 +0200 +++ b/src/Pure/System/options.ML Tue Apr 05 20:51:37 2016 +0200 @@ -222,6 +222,6 @@ end); val _ = load_default (); -val _ = ML_Pretty.print_depth (default_int "ML_print_depth"); +val _ = ML_Print_Depth.set_print_depth (default_int "ML_print_depth"); end; diff -r 741560a5283b -r 1cec457e0a03 src/Pure/Tools/debugger.ML --- a/src/Pure/Tools/debugger.ML Tue Apr 05 20:05:05 2016 +0200 +++ b/src/Pure/Tools/debugger.ML Tue Apr 05 20:51:37 2016 +0200 @@ -190,7 +190,7 @@ fun print x = Pretty.from_polyml - (ML_Name_Space.displayVal (x, FixedInt.fromInt (ML_Options.get_print_depth ()), space)); + (ML_Name_Space.displayVal (x, FixedInt.fromInt (ML_Print_Depth.get_print_depth ()), space)); fun print_all () = #allVal (ML_Debugger.debug_local_name_space (the_debug_state thread_name index)) () |> sort_by #1 |> map (Pretty.item o single o print o #2)