--- a/NEWS Wed Mar 26 11:05:25 2014 -0700
+++ b/NEWS Thu Mar 27 21:38:45 2014 +0100
@@ -541,6 +541,9 @@
*** ML ***
+* Moved ML_Compiler.exn_trace and other operations on exceptions to
+structure Runtime. Minor INCOMPATIBILITY.
+
* Discontinued old Toplevel.debug in favour of system option
"ML_exception_trace", which may be also declared within the context via
"declare [[ML_exception_trace = true]]". Minor INCOMPATIBILITY.
--- a/src/Doc/IsarImplementation/ML.thy Wed Mar 26 11:05:25 2014 -0700
+++ b/src/Doc/IsarImplementation/ML.thy Thu Mar 27 21:38:45 2014 +0100
@@ -1163,7 +1163,7 @@
@{index_ML_exception Fail: string} \\
@{index_ML Exn.is_interrupt: "exn -> bool"} \\
@{index_ML reraise: "exn -> 'a"} \\
- @{index_ML ML_Compiler.exn_trace: "(unit -> 'a) -> 'a"} \\
+ @{index_ML Runtime.exn_trace: "(unit -> 'a) -> 'a"} \\
\end{mldecls}
\begin{description}
@@ -1191,12 +1191,12 @@
while preserving its implicit position information (if possible,
depending on the ML platform).
- \item @{ML ML_Compiler.exn_trace}~@{ML_text "(fn () =>"}~@{text
+ \item @{ML Runtime.exn_trace}~@{ML_text "(fn () =>"}~@{text
"e"}@{ML_text ")"} evaluates expression @{text "e"} while printing
a full trace of its stack of nested exceptions (if possible,
depending on the ML platform).
- Inserting @{ML ML_Compiler.exn_trace} into ML code temporarily is
+ Inserting @{ML Runtime.exn_trace} into ML code temporarily is
useful for debugging, but not suitable for production code.
\end{description}
--- a/src/Doc/antiquote_setup.ML Wed Mar 26 11:05:25 2014 -0700
+++ b/src/Doc/antiquote_setup.ML Thu Mar 27 21:38:45 2014 +0100
@@ -100,8 +100,7 @@
val txt' = if kind = "" then txt else kind ^ " " ^ txt;
val _ =
- ML_Context.eval_in (SOME ctxt) {SML = false, verbose = false} (#pos source1)
- (ml (toks1, toks2));
+ ML_Context.eval_in (SOME ctxt) ML_Compiler.flags (#pos source1) (ml (toks1, toks2));
val kind' = if kind = "" then "ML" else "ML " ^ kind;
in
"\\indexdef{}{" ^ kind' ^ "}{" ^ clean_string (ml_name txt1) ^ "}" ^
@@ -192,17 +191,17 @@
fun no_check _ _ = true;
-fun check_command (name, pos) =
+fun check_command ctxt (name, pos) =
is_some (Keyword.command_keyword name) andalso
let
val markup =
Outer_Syntax.scan Position.none name
|> maps (Outer_Syntax.command_reports (#2 (Outer_Syntax.get_syntax ())))
|> map (snd o fst);
- val _ = List.app (Position.report pos) markup;
+ val _ = Context_Position.reports ctxt (map (pair pos) markup);
in true end;
-fun check_tool (name, pos) =
+fun check_tool ctxt (name, pos) =
let
fun tool dir =
let val path = Path.append dir (Path.basic name)
@@ -210,7 +209,7 @@
in
(case get_first tool (Path.split (getenv "ISABELLE_TOOLS")) of
NONE => false
- | SOME path => (Position.report pos (Markup.path (Path.implode path)); true))
+ | SOME path => (Context_Position.report ctxt pos (Markup.path (Path.implode path)); true))
end;
val arg = enclose "{" "}" o clean_string;
@@ -255,7 +254,7 @@
val _ =
Theory.setup
(entity_antiqs no_check "" @{binding syntax} #>
- entity_antiqs (K check_command) "isacommand" @{binding command} #>
+ entity_antiqs check_command "isacommand" @{binding command} #>
entity_antiqs (K (Keyword.is_keyword o #1)) "isakeyword" @{binding keyword} #>
entity_antiqs (K (Keyword.is_keyword o #1)) "isakeyword" @{binding element} #>
entity_antiqs (can o Method.check_name) "" @{binding method} #>
@@ -269,7 +268,7 @@
entity_antiqs no_check "isatt" @{binding system_option} #>
entity_antiqs no_check "" @{binding inference} #>
entity_antiqs no_check "isatt" @{binding executable} #>
- entity_antiqs (K check_tool) "isatool" @{binding tool} #>
+ entity_antiqs check_tool "isatool" @{binding tool} #>
entity_antiqs (can o ML_Context.check_antiquotation) "" @{binding ML_antiquotation} #>
entity_antiqs (K (is_action o #1)) "isatt" @{binding action});
--- a/src/HOL/TPTP/TPTP_Interpret_Test.thy Wed Mar 26 11:05:25 2014 -0700
+++ b/src/HOL/TPTP/TPTP_Interpret_Test.thy Thu Mar 27 21:38:45 2014 +0100
@@ -132,7 +132,7 @@
if Exn.is_interrupt exn then reraise exn
else
(warning (" test: file " ^ Path.print file ^
- " raised exception: " ^ ML_Compiler.exn_message exn);
+ " raised exception: " ^ Runtime.exn_message exn);
{gc = Time.zeroTime, cpu = Time.zeroTime, elapsed = Time.zeroTime})
val to_real = Time.toReal
val diff_elapsed =
--- a/src/HOL/TPTP/TPTP_Test.thy Wed Mar 26 11:05:25 2014 -0700
+++ b/src/HOL/TPTP/TPTP_Test.thy Thu Mar 27 21:38:45 2014 +0100
@@ -63,7 +63,7 @@
reraise exn
else
(report ctxt (msg ^ " test: file " ^ Path.print file_name ^
- " raised exception: " ^ ML_Compiler.exn_message exn);
+ " raised exception: " ^ Runtime.exn_message exn);
default_val)
end
--- a/src/HOL/Tools/SMT/smt_config.ML Wed Mar 26 11:05:25 2014 -0700
+++ b/src/HOL/Tools/SMT/smt_config.ML Thu Mar 27 21:38:45 2014 +0100
@@ -101,8 +101,9 @@
filter (is_available ctxt) (all_solvers_of ctxt)
fun warn_solver (Context.Proof ctxt) name =
- Context_Position.if_visible ctxt
+ if Context_Position.is_visible ctxt then
warning ("The SMT solver " ^ quote name ^ " is not installed.")
+ else ()
| warn_solver _ _ = ();
fun select_solver name context =
--- a/src/HOL/Tools/SMT2/smt2_config.ML Wed Mar 26 11:05:25 2014 -0700
+++ b/src/HOL/Tools/SMT2/smt2_config.ML Thu Mar 27 21:38:45 2014 +0100
@@ -99,8 +99,9 @@
filter (is_available ctxt) (all_solvers_of ctxt)
fun warn_solver (Context.Proof ctxt) name =
- Context_Position.if_visible ctxt
+ if Context_Position.is_visible ctxt then
warning ("The SMT solver " ^ quote name ^ " is not installed.")
+ else ()
| warn_solver _ _ = ();
fun select_solver name context =
--- a/src/HOL/Tools/Sledgehammer/async_manager.ML Wed Mar 26 11:05:25 2014 -0700
+++ b/src/HOL/Tools/Sledgehammer/async_manager.ML Thu Mar 27 21:38:45 2014 +0100
@@ -130,7 +130,7 @@
fun check_thread_manager () = Synchronized.change global_state
(fn state as {manager, timeout_heap, active, canceling, messages, store} =>
if (case manager of SOME thread => Thread.isActive thread | NONE => false) then state
- else let val manager = SOME (Toplevel.thread false (fn () =>
+ else let val manager = SOME (Runtime.thread false (fn () =>
let
fun time_limit timeout_heap =
(case try Thread_Heap.min timeout_heap of
@@ -183,7 +183,7 @@
fun thread tool birth_time death_time desc f =
- (Toplevel.thread true
+ (Runtime.thread true
(fn () =>
let
val self = Thread.self ()
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Wed Mar 26 11:05:25 2014 -0700
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Thu Mar 27 21:38:45 2014 +0100
@@ -157,7 +157,7 @@
reraise exn
else
(unknownN, fn () => "Internal error:\n" ^
- ML_Compiler.exn_message exn ^ "\n"))
+ Runtime.exn_message exn ^ "\n"))
val _ =
(* The "expect" argument is deliberately ignored if the prover is
missing so that the "Metis_Examples" can be processed on any
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Wed Mar 26 11:05:25 2014 -0700
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Thu Mar 27 21:38:45 2014 +0100
@@ -337,7 +337,7 @@
else
(trace_msg ctxt (fn () =>
"Internal error when " ^ when ^ ":\n" ^
- ML_Compiler.exn_message exn); def)
+ Runtime.exn_message exn); def)
fun graph_info G =
string_of_int (length (Graph.keys G)) ^ " node(s), " ^
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML Wed Mar 26 11:05:25 2014 -0700
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML Thu Mar 27 21:38:45 2014 +0100
@@ -159,7 +159,7 @@
|> (fn {outcome, used_facts} => (outcome, used_facts))
handle exn =>
if Exn.is_interrupt exn then reraise exn
- else (ML_Compiler.exn_message exn |> SMT_Failure.Other_Failure |> SOME, [])
+ else (Runtime.exn_message exn |> SMT_Failure.Other_Failure |> SOME, [])
val death = Timer.checkRealTimer timer
val outcome0 = if is_none outcome0 then SOME outcome else outcome0
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML Wed Mar 26 11:05:25 2014 -0700
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML Thu Mar 27 21:38:45 2014 +0100
@@ -160,7 +160,7 @@
if Exn.is_interrupt exn orelse debug then
reraise exn
else
- {outcome = SOME (SMT2_Failure.Other_Failure (ML_Compiler.exn_message exn)),
+ {outcome = SOME (SMT2_Failure.Other_Failure (Runtime.exn_message exn)),
rewrite_rules = [], conjecture_id = ~1, helper_ids = [], fact_ids = [],
z3_proof = []}
--- a/src/HOL/ex/Cartouche_Examples.thy Wed Mar 26 11:05:25 2014 -0700
+++ b/src/HOL/ex/Cartouche_Examples.thy Thu Mar 27 21:38:45 2014 +0100
@@ -120,7 +120,7 @@
ML_Lex.read Position.none "fn _ => (" @
ML_Lex.read_source false source @
ML_Lex.read Position.none ");";
- val _ = ML_Context.eval_in (SOME context) {SML = false, verbose = false} (#pos source) toks;
+ val _ = ML_Context.eval_in (SOME context) ML_Compiler.flags (#pos source) toks;
in "" end);
*}
--- a/src/Pure/General/completion.ML Wed Mar 26 11:05:25 2014 -0700
+++ b/src/Pure/General/completion.ML Thu Mar 27 21:38:45 2014 +0100
@@ -10,7 +10,6 @@
val names: Position.T -> (string * (string * string)) list -> T
val none: T
val reported_text: T -> string
- val report: T -> unit
val suppress_abbrevs: string -> Markup.T list
end;
@@ -46,8 +45,6 @@
else ""
end;
-val report = Output.report o reported_text;
-
(* suppress short abbreviations *)
--- a/src/Pure/Isar/attrib.ML Wed Mar 26 11:05:25 2014 -0700
+++ b/src/Pure/Isar/attrib.ML Thu Mar 27 21:38:45 2014 +0100
@@ -457,9 +457,9 @@
register_config Name_Space.names_long_raw #>
register_config Name_Space.names_short_raw #>
register_config Name_Space.names_unique_raw #>
- register_config ML_Context.source_trace_raw #>
- register_config ML_Compiler.print_depth_raw #>
- register_config Runtime.exception_trace_raw #>
+ register_config ML_Options.source_trace_raw #>
+ register_config ML_Options.exception_trace_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 #>
--- a/src/Pure/Isar/generic_target.ML Wed Mar 26 11:05:25 2014 -0700
+++ b/src/Pure/Isar/generic_target.ML Thu Mar 27 21:38:45 2014 +0100
@@ -57,12 +57,13 @@
fun check_mixfix ctxt (b, extra_tfrees) mx =
if null extra_tfrees then mx
else
- (Context_Position.if_visible ctxt warning
- ("Additional type variable(s) in specification of " ^ Binding.print b ^ ": " ^
- commas (map (Syntax.string_of_typ ctxt o TFree) (sort_wrt #1 extra_tfrees)) ^
- (if mx = NoSyn then ""
- else "\nDropping mixfix syntax " ^ Pretty.string_of (Mixfix.pretty_mixfix mx)));
- NoSyn);
+ (if Context_Position.is_visible ctxt then
+ warning
+ ("Additional type variable(s) in specification of " ^ Binding.print b ^ ": " ^
+ commas (map (Syntax.string_of_typ ctxt o TFree) (sort_wrt #1 extra_tfrees)) ^
+ (if mx = NoSyn then ""
+ else "\nDropping mixfix syntax " ^ Pretty.string_of (Mixfix.pretty_mixfix mx)))
+ else (); NoSyn);
fun check_mixfix_global (b, no_params) mx =
if no_params orelse mx = NoSyn then mx
--- a/src/Pure/Isar/isar_cmd.ML Wed Mar 26 11:05:25 2014 -0700
+++ b/src/Pure/Isar/isar_cmd.ML Thu Mar 27 21:38:45 2014 +0100
@@ -145,8 +145,10 @@
\ val " ^ name ^
" = snd (Context.>>> (Context.map_theory_result (Thm.add_oracle (binding, body))));\n\
\end;\n");
- val flags = {SML = false, verbose = false};
- in Context.theory_map (ML_Context.exec (fn () => ML_Context.eval flags (#pos source) ants)) end;
+ in
+ Context.theory_map
+ (ML_Context.exec (fn () => ML_Context.eval ML_Compiler.flags (#pos source) ants))
+ end;
(* old-style defs *)
@@ -236,10 +238,12 @@
);
fun ml_diag verbose source = Toplevel.keep (fn state =>
- let val opt_ctxt =
- try Toplevel.generic_theory_of state
- |> Option.map (Context.proof_of #> Diag_State.put state)
- in ML_Context.eval_source_in opt_ctxt {SML = false, verbose = verbose} source end);
+ let
+ val opt_ctxt =
+ try Toplevel.generic_theory_of state
+ |> Option.map (Context.proof_of #> Diag_State.put state);
+ val flags = ML_Compiler.verbose verbose ML_Compiler.flags;
+ in ML_Context.eval_source_in opt_ctxt flags source end);
val diag_state = Diag_State.get;
--- a/src/Pure/Isar/isar_syn.ML Wed Mar 26 11:05:25 2014 -0700
+++ b/src/Pure/Isar/isar_syn.ML Thu Mar 27 21:38:45 2014 +0100
@@ -273,23 +273,26 @@
let
val ([{lines, pos, ...}], thy') = files thy;
val source = {delimited = true, text = cat_lines lines, pos = pos};
+ val flags = {SML = true, redirect = true, verbose = true};
in
thy' |> Context.theory_map
- (ML_Context.exec (fn () => ML_Context.eval_source {SML = true, verbose = true} source))
+ (ML_Context.exec (fn () => ML_Context.eval_source flags source))
end)));
val _ =
Outer_Syntax.command @{command_spec "ML"} "ML text within theory or local theory"
(Parse.ML_source >> (fn source =>
Toplevel.generic_theory
- (ML_Context.exec (fn () => ML_Context.eval_source {SML = false, verbose = true} source) #>
+ (ML_Context.exec (fn () =>
+ ML_Context.eval_source (ML_Compiler.verbose true ML_Compiler.flags) source) #>
Local_Theory.propagate_ml_env)));
val _ =
Outer_Syntax.command @{command_spec "ML_prf"} "ML text within proof"
(Parse.ML_source >> (fn source =>
Toplevel.proof (Proof.map_context (Context.proof_map
- (ML_Context.exec (fn () => ML_Context.eval_source {SML = false, verbose = true} source))) #>
+ (ML_Context.exec (fn () =>
+ ML_Context.eval_source (ML_Compiler.verbose true ML_Compiler.flags) source))) #>
Proof.propagate_ml_env)));
val _ =
--- a/src/Pure/Isar/outer_syntax.ML Wed Mar 26 11:05:25 2014 -0700
+++ b/src/Pure/Isar/outer_syntax.ML Thu Mar 27 21:38:45 2014 +0100
@@ -143,7 +143,8 @@
fun add_command (name, kind) cmd = CRITICAL (fn () =>
let
- val thy = ML_Context.the_global_context ();
+ val context = ML_Context.the_generic_context ();
+ val thy = Context.theory_of context;
val Command {pos, ...} = cmd;
val _ =
(case try (Thy_Header.the_keyword thy) name of
@@ -155,7 +156,7 @@
if Context.theory_name thy = Context.PureN
then Keyword.define (name, SOME kind)
else error ("Undeclared outer syntax command " ^ quote name ^ Position.here pos));
- val _ = Position.report pos (command_markup true (name, cmd));
+ val _ = Context_Position.report_generic context pos (command_markup true (name, cmd));
fun redefining () =
"Redefining outer syntax command " ^ quote name ^ Position.here (Position.thread_data ());
--- a/src/Pure/Isar/proof_context.ML Wed Mar 26 11:05:25 2014 -0700
+++ b/src/Pure/Isar/proof_context.ML Thu Mar 27 21:38:45 2014 +0100
@@ -718,7 +718,7 @@
fun check_tfree ctxt v =
let
val (sorting_report, [TFree a]) = prepare_sortsT ctxt [TFree v];
- val _ = Context_Position.if_visible ctxt Output.report sorting_report;
+ val _ = if Context_Position.is_visible ctxt then Output.report sorting_report else ();
in a end;
end;
--- a/src/Pure/Isar/runtime.ML Wed Mar 26 11:05:25 2014 -0700
+++ b/src/Pure/Isar/runtime.ML Thu Mar 27 21:38:45 2014 +0100
@@ -11,16 +11,17 @@
exception EXCURSION_FAIL of exn * string
exception TOPLEVEL_ERROR
val exn_context: Proof.context option -> exn -> exn
- type exn_info = {exn_position: exn -> Position.T, pretty_exn: exn -> Pretty.T}
type error = ((serial * string) * string option)
- val exn_messages_ids: exn_info -> exn -> error list
- val exn_messages: exn_info -> exn -> (serial * string) list
- val exn_message: exn_info -> exn -> string
- val exception_trace_raw: Config.raw
- val exception_trace: bool Config.T
- val debugging: (exn -> string) -> Context.generic option -> ('a -> 'b) -> 'a -> 'b
- val controlled_execution: (exn -> string) -> Context.generic option -> ('a -> 'b) -> 'a -> 'b
+ val exn_messages_ids: exn -> error list
+ val exn_messages: exn -> (serial * string) list
+ val exn_message: exn -> string
+ val exn_error_message: exn -> unit
+ val exn_trace: (unit -> 'a) -> 'a
+ val debugging: Context.generic option -> ('a -> 'b) -> 'a -> 'b
+ val controlled_execution: Context.generic option -> ('a -> 'b) -> 'a -> 'b
val toplevel_error: (exn -> unit) -> ('a -> 'b) -> 'a -> 'b
+ val toplevel_program: (unit -> 'a) -> 'a
+ val thread: bool -> (unit -> unit) -> Thread.thread
end;
structure Runtime: RUNTIME =
@@ -44,7 +45,6 @@
(* exn_message *)
-type exn_info = {exn_position: exn -> Position.T, pretty_exn: exn -> Pretty.T};
type error = ((serial * string) * string option);
local
@@ -75,10 +75,10 @@
in
-fun exn_messages_ids {exn_position, pretty_exn} e =
+fun exn_messages_ids e =
let
fun raised exn name msgs =
- let val pos = Position.here (exn_position exn) in
+ let val pos = Position.here (Exn_Output.position exn) in
(case msgs of
[] => "exception " ^ name ^ " raised" ^ pos
| [msg] => "exception " ^ name ^ " raised" ^ pos ^ ": " ^ msg
@@ -117,7 +117,7 @@
| THM (msg, i, thms) =>
raised exn ("THM " ^ string_of_int i)
(msg :: robust_context context Display.string_of_thm thms)
- | _ => raised exn (robust (Pretty.string_of o pretty_exn) exn) []);
+ | _ => raised exn (robust (Pretty.string_of o Exn_Output.pretty) exn) []);
in [((i, msg), id)] end)
and sorted_msgs context exn =
sort_distinct (int_ord o pairself (fst o fst)) (maps exn_msgs (flatten context exn));
@@ -126,30 +126,27 @@
end;
-fun exn_messages exn_info exn = map #1 (exn_messages_ids exn_info exn);
+fun exn_messages exn = map #1 (exn_messages_ids exn);
-fun exn_message exn_info exn =
- (case exn_messages exn_info exn of
+fun exn_message exn =
+ (case exn_messages exn of
[] => "Interrupt"
| msgs => cat_lines (map snd msgs));
+val exn_error_message = Output.error_message o exn_message;
+fun exn_trace e = print_exception_trace exn_message e;
+
+
(** controlled execution **)
-val exception_trace_raw = Config.declare_option "ML_exception_trace";
-val exception_trace = Config.bool exception_trace_raw;
-
-fun exception_trace_enabled NONE =
- (Options.default_bool (Config.name_of exception_trace_raw) handle ERROR _ => false)
- | exception_trace_enabled (SOME context) = Config.get_generic context exception_trace;
-
-fun debugging exn_message opt_context f x =
- if exception_trace_enabled opt_context
+fun debugging opt_context f x =
+ if ML_Options.exception_trace_enabled opt_context
then print_exception_trace exn_message (fn () => f x)
else f x;
-fun controlled_execution exn_message opt_context f x =
- (f |> debugging exn_message opt_context |> Future.interruptible_task) x;
+fun controlled_execution opt_context f x =
+ (f |> debugging opt_context |> Future.interruptible_task) x;
fun toplevel_error output_exn f x = f x
handle exn =>
@@ -163,5 +160,17 @@
val _ = output_exn (exn_context opt_ctxt exn);
in raise TOPLEVEL_ERROR end;
+fun toplevel_program body =
+ (body |> controlled_execution NONE |> toplevel_error exn_error_message) ();
+
+(*Proof General legacy*)
+fun thread interrupts body =
+ Thread.fork
+ (((fn () => body () handle exn => if Exn.is_interrupt exn then () else reraise exn)
+ |> debugging NONE
+ |> toplevel_error
+ (fn exn => Output.urgent_message ("## INTERNAL ERROR ##\n" ^ exn_message exn))),
+ Simple_Thread.attributes interrupts);
+
end;
--- a/src/Pure/Isar/toplevel.ML Wed Mar 26 11:05:25 2014 -0700
+++ b/src/Pure/Isar/toplevel.ML Thu Mar 27 21:38:45 2014 +0100
@@ -29,10 +29,6 @@
val interact: bool Unsynchronized.ref
val timing: bool Unsynchronized.ref
val profiling: int Unsynchronized.ref
- val debugging: Context.generic option -> ('a -> 'b) -> 'a -> 'b
- val controlled_execution: Context.generic option -> ('a -> 'b) -> 'a -> 'b
- val program: (unit -> 'a) -> 'a
- val thread: bool -> (unit -> unit) -> Thread.thread
type transition
val empty: transition
val print_of: transition -> bool
@@ -232,26 +228,6 @@
val profiling = Unsynchronized.ref 0;
-(* controlled execution *)
-
-fun debugging arg = Runtime.debugging ML_Compiler.exn_message arg;
-fun controlled_execution arg = Runtime.controlled_execution ML_Compiler.exn_message arg;
-
-fun program body =
- (body
- |> controlled_execution NONE
- |> Runtime.toplevel_error ML_Compiler.exn_error_message) ();
-
-fun thread interrupts body =
- Thread.fork
- (((fn () => body () handle exn => if Exn.is_interrupt exn then () else reraise exn)
- |> debugging NONE
- |> Runtime.toplevel_error
- (fn exn =>
- Output.urgent_message ("## INTERNAL ERROR ##\n" ^ ML_Compiler.exn_message exn))),
- Simple_Thread.attributes interrupts);
-
-
(* node transactions -- maintaining stable checkpoints *)
exception FAILURE of state * exn;
@@ -275,7 +251,7 @@
val (result, err) =
cont_node
- |> controlled_execution (SOME context) f
+ |> Runtime.controlled_execution (SOME context) f
|> state_error NONE
handle exn => state_error (SOME exn) cont_node;
in
@@ -304,11 +280,11 @@
local
fun apply_tr _ (Init f) (State (NONE, _)) =
- State (SOME (Theory (Context.Theory (controlled_execution NONE f ()), NONE)), NONE)
+ State (SOME (Theory (Context.Theory (Runtime.controlled_execution NONE f ()), NONE)), NONE)
| apply_tr _ Exit (State (SOME (state as Theory (Context.Theory _, _)), _)) =
exit_transaction state
| apply_tr int (Keep f) state =
- controlled_execution (try generic_theory_of state) (fn x => tap (f int) x) state
+ Runtime.controlled_execution (try generic_theory_of state) (fn x => tap (f int) x) state
| apply_tr int (Transaction (f, g)) (State (SOME state, _)) =
apply_transaction (fn x => f int x) g state
| apply_tr _ _ _ = raise UNDEF;
@@ -649,8 +625,8 @@
fun command_errors int tr st =
(case transition int tr st of
SOME (st', NONE) => ([], SOME st')
- | SOME (_, SOME (exn, _)) => (ML_Compiler.exn_messages_ids exn, NONE)
- | NONE => (ML_Compiler.exn_messages_ids Runtime.TERMINATE, NONE));
+ | SOME (_, SOME (exn, _)) => (Runtime.exn_messages_ids exn, NONE)
+ | NONE => (Runtime.exn_messages_ids Runtime.TERMINATE, NONE));
fun command_exception int tr st =
(case transition int tr st of
--- a/src/Pure/Isar/typedecl.ML Wed Mar 26 11:05:25 2014 -0700
+++ b/src/Pure/Isar/typedecl.ML Thu Mar 27 21:38:45 2014 +0100
@@ -102,11 +102,12 @@
val rhs = Proof_Context.read_typ_syntax (ctxt |> Proof_Context.set_defsort []) raw_rhs;
val ignored = Term.fold_atyps_sorts (fn (_, []) => I | (T, _) => insert (op =) T) rhs [];
val _ =
- if null ignored then ()
- else Context_Position.if_visible ctxt warning
- ("Ignoring sort constraints in type variables(s): " ^
- commas_quote (map (Syntax.string_of_typ ctxt) (rev ignored)) ^
- "\nin type abbreviation " ^ Binding.print b);
+ if not (null ignored) andalso Context_Position.is_visible ctxt then
+ warning
+ ("Ignoring sort constraints in type variables(s): " ^
+ commas_quote (map (Syntax.string_of_typ ctxt) (rev ignored)) ^
+ "\nin type abbreviation " ^ Binding.print b)
+ else ();
in rhs end;
in
--- a/src/Pure/ML-Systems/polyml.ML Wed Mar 26 11:05:25 2014 -0700
+++ b/src/Pure/ML-Systems/polyml.ML Thu Mar 27 21:38:45 2014 +0100
@@ -175,5 +175,5 @@
("PolyML.addPrettyPrinter (fn _ => fn _ => ml_pretty o Pretty.to_ML o (" ^ pp ^ "))");
val ml_make_string =
- "(fn x => Pretty.string_of (Pretty.from_ML (pretty_ml (PolyML.prettyRepresentation (x, ML_Compiler.get_print_depth ())))))";
+ "(fn x => Pretty.string_of (Pretty.from_ML (pretty_ml (PolyML.prettyRepresentation (x, ML_Options.get_print_depth ())))))";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML/exn_output.ML Thu Mar 27 21:38:45 2014 +0100
@@ -0,0 +1,20 @@
+(* Title: Pure/ML/exn_output.ML
+ Author: Makarius
+
+Auxiliary operations for exception output -- generic version.
+*)
+
+signature EXN_OUTPUT =
+sig
+ val position: exn -> Position.T
+ val pretty: exn -> Pretty.T
+end
+
+structure Exn_Output: EXN_OUTPUT =
+struct
+
+fun position (_: exn) = Position.none
+val pretty = Pretty.str o General.exnMessage;
+
+end;
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML/exn_output_polyml.ML Thu Mar 27 21:38:45 2014 +0100
@@ -0,0 +1,19 @@
+(* Title: Pure/ML/exn_output_polyml.ML
+ Author: Makarius
+
+Auxiliary operations for exception output -- Poly/ML version.
+*)
+
+structure Exn_Output: EXN_OUTPUT =
+struct
+
+fun position exn =
+ (case PolyML.exceptionLocation exn of
+ NONE => Position.none
+ | SOME loc => Exn_Properties.position_of loc);
+
+fun pretty (exn: exn) =
+ Pretty.from_ML (pretty_ml (PolyML.prettyRepresentation (exn, ML_Options.get_print_depth ())));
+
+end;
+
--- a/src/Pure/ML/exn_properties_polyml.ML Wed Mar 26 11:05:25 2014 -0700
+++ b/src/Pure/ML/exn_properties_polyml.ML Thu Mar 27 21:38:45 2014 +0100
@@ -6,7 +6,7 @@
signature EXN_PROPERTIES =
sig
- val of_location: PolyML.location -> Properties.T
+ val position_of: PolyML.location -> Position.T
val get: exn -> Properties.T
val update: Properties.entry list -> exn -> exn
end;
@@ -14,23 +14,35 @@
structure Exn_Properties: EXN_PROPERTIES =
struct
-fun of_location (loc: PolyML.location) =
+(* source locations *)
+
+fun props_of (loc: PolyML.location) =
(case YXML.parse_body (#file loc) of
[] => []
| [XML.Text file] => [(Markup.fileN, file)]
| body => XML.Decode.properties body);
+fun position_of loc =
+ Position.make
+ {line = #startLine loc,
+ offset = #startPosition loc,
+ end_offset = #endPosition loc,
+ props = props_of loc};
+
+
+(* exception properties *)
+
fun get exn =
(case PolyML.exceptionLocation exn of
NONE => []
- | SOME loc => of_location loc);
+ | SOME loc => props_of loc);
fun update entries exn =
let
val loc =
the_default {file = "", startLine = 0, endLine = 0, startPosition = 0, endPosition = 0}
(PolyML.exceptionLocation exn);
- val props = of_location loc;
+ val props = props_of loc;
val props' = fold Properties.put entries props;
in
if props = props' then exn
--- a/src/Pure/ML/ml_compiler.ML Wed Mar 26 11:05:25 2014 -0700
+++ b/src/Pure/ML/ml_compiler.ML Thu Mar 27 21:38:45 2014 +0100
@@ -1,63 +1,31 @@
(* Title: Pure/ML/ml_compiler.ML
Author: Makarius
-Runtime compilation -- generic version.
+Runtime compilation and evaluation -- generic version.
*)
signature ML_COMPILER =
sig
- val exn_messages_ids: exn -> Runtime.error list
- val exn_messages: exn -> (serial * string) list
- val exn_message: exn -> string
- val exn_error_message: exn -> unit
- val exn_trace: (unit -> 'a) -> 'a
- val print_depth_raw: Config.raw
- val print_depth: int Config.T
- val get_print_depth: unit -> int
- type flags = {SML: bool, verbose: bool}
+ type flags = {SML: bool, redirect: bool, verbose: bool}
+ val flags: flags
+ val verbose: bool -> flags -> flags
val eval: flags -> Position.T -> ML_Lex.token list -> unit
end
structure ML_Compiler: ML_COMPILER =
struct
-(* exceptions *)
-
-val exn_info =
- {exn_position = fn _: exn => Position.none,
- pretty_exn = Pretty.str o General.exnMessage};
-
-val exn_messages_ids = Runtime.exn_messages_ids exn_info;
-val exn_messages = Runtime.exn_messages exn_info;
-val exn_message = Runtime.exn_message exn_info;
-
-val exn_error_message = Output.error_message o exn_message;
-fun exn_trace e = print_exception_trace exn_message e;
-
-
-(* print depth *)
+type flags = {SML: bool, redirect: bool, verbose: bool};
+val flags = {SML = false, redirect = false, verbose = false};
+fun verbose v (flags: flags) = {SML = #SML flags, redirect = #redirect flags, verbose = v};
-val print_depth_raw =
- Config.declare "ML_print_depth" (fn _ => Config.Int (get_default_print_depth ()));
-val print_depth = Config.int print_depth_raw;
-
-fun get_print_depth () =
- (case Context.thread_data () of
- NONE => get_default_print_depth ()
- | SOME context => Config.get_generic context print_depth);
-
-
-(* eval *)
-
-type flags = {SML: bool, verbose: bool};
-
-fun eval {SML, verbose} pos toks =
+fun eval (flags: flags) pos toks =
let
- val _ = if SML then error ("Standard ML is unsupported on " ^ ML_System.name) else ();
+ val _ = if #SML flags then error ("Standard ML is unsupported on " ^ ML_System.name) else ();
val line = the_default 1 (Position.line_of pos);
val file = the_default "ML" (Position.file_of pos);
val text = ML_Lex.flatten toks;
- in Secure.use_text ML_Env.local_context (line, file) verbose text end;
+ in Secure.use_text ML_Env.local_context (line, file) (#verbose flags) text end;
end;
--- a/src/Pure/ML/ml_compiler_polyml.ML Wed Mar 26 11:05:25 2014 -0700
+++ b/src/Pure/ML/ml_compiler_polyml.ML Thu Mar 27 21:38:45 2014 +0100
@@ -1,7 +1,7 @@
(* Title: Pure/ML/ml_compiler_polyml.ML
Author: Makarius
-Advanced runtime compilation for Poly/ML.
+Runtime compilation and evaluation -- Poly/ML version.
*)
structure ML_Compiler: ML_COMPILER =
@@ -10,77 +10,67 @@
open ML_Compiler;
-(* source locations *)
-
-fun position_of (loc: PolyML.location) =
- let
- val {startLine = line, startPosition = offset, endPosition = end_offset, ...} = loc;
- val props = Exn_Properties.of_location loc;
- in
- Position.make {line = line, offset = offset, end_offset = end_offset, props = props}
- end;
-
-
-(* exn_info *)
-
-fun exn_position exn =
- (case PolyML.exceptionLocation exn of
- NONE => Position.none
- | SOME loc => position_of loc);
-
-fun pretty_exn (exn: exn) =
- Pretty.from_ML (pretty_ml (PolyML.prettyRepresentation (exn, get_print_depth ())));
-
-val exn_info = {exn_position = exn_position, pretty_exn = pretty_exn};
-
-
-(* exn_message *)
-
-val exn_messages_ids = Runtime.exn_messages_ids exn_info;
-val exn_messages = Runtime.exn_messages exn_info;
-val exn_message = Runtime.exn_message exn_info;
-
-val exn_error_message = Output.error_message o exn_message;
-fun exn_trace e = print_exception_trace exn_message e;
-
-
(* parse trees *)
-fun report_parse_tree depth space =
+fun report_parse_tree redirect depth space parse_tree =
let
- val reported_text =
+ val is_visible =
(case Context.thread_data () of
- SOME (Context.Proof ctxt) => Context_Position.reported_text ctxt
- | _ => Position.reported_text);
+ SOME context => Context_Position.is_visible_generic context
+ | NONE => true);
+ fun is_reported pos = is_visible andalso Position.is_reported pos;
+
+ fun reported_types loc types =
+ let val pos = Exn_Properties.position_of loc in
+ is_reported pos ?
+ let
+ val xml =
+ PolyML.NameSpace.displayTypeExpression (types, depth, space)
+ |> pretty_ml |> Pretty.from_ML |> Pretty.string_of
+ |> Output.output |> YXML.parse_body;
+ in cons (pos, fn () => Markup.ML_typing, fn () => YXML.string_of_body xml) end
+ end;
fun reported_entity kind loc decl =
- reported_text (position_of loc)
- (Markup.entityN, (Markup.kindN, kind) :: Position.def_properties_of (position_of decl)) "";
+ let val pos = Exn_Properties.position_of loc in
+ is_reported pos ?
+ let
+ val def_pos = Exn_Properties.position_of decl;
+ fun markup () =
+ (Markup.entityN, (Markup.kindN, kind) :: Position.def_properties_of def_pos);
+ in cons (pos, markup, fn () => "") end
+ end;
- fun reported loc (PolyML.PTtype types) =
- cons
- (PolyML.NameSpace.displayTypeExpression (types, depth, space)
- |> pretty_ml |> Pretty.from_ML |> Pretty.string_of
- |> reported_text (position_of loc) Markup.ML_typing)
- | reported loc (PolyML.PTdeclaredAt decl) =
- cons (reported_entity Markup.ML_defN loc decl)
- | reported loc (PolyML.PTopenedAt decl) =
- cons (reported_entity Markup.ML_openN loc decl)
- | reported loc (PolyML.PTstructureAt decl) =
- cons (reported_entity Markup.ML_structureN loc decl)
+ fun reported loc (PolyML.PTtype types) = reported_types loc types
+ | reported loc (PolyML.PTdeclaredAt decl) = reported_entity Markup.ML_defN loc decl
+ | reported loc (PolyML.PTopenedAt decl) = reported_entity Markup.ML_openN loc decl
+ | reported loc (PolyML.PTstructureAt decl) = reported_entity Markup.ML_structureN loc decl
| reported _ (PolyML.PTnextSibling tree) = reported_tree (tree ())
| reported _ (PolyML.PTfirstChild tree) = reported_tree (tree ())
| reported _ _ = I
and reported_tree (loc, props) = fold (reported loc) props;
- in fn tree => Output.report (implode (reported_tree tree [])) end;
+
+ val persistent_reports = reported_tree parse_tree [];
+
+ fun output () =
+ persistent_reports
+ |> map (fn (pos, markup, text) => Position.reported_text pos (markup ()) (text ()))
+ |> implode |> Output.report;
+ in
+ if not (null persistent_reports) andalso redirect andalso Multithreading.enabled ()
+ then
+ Execution.print
+ {name = "ML_Compiler.report", pos = Position.thread_data (), pri = 1} output
+ else output ()
+ end;
(* eval ML source tokens *)
-fun eval {SML, verbose} pos toks =
+fun eval (flags: flags) pos toks =
let
val _ = Secure.secure_mltext ();
- val space = if SML then ML_Env.SML_name_space else ML_Env.name_space;
+ val space = if #SML flags then ML_Env.SML_name_space else ML_Env.name_space;
val opt_context = Context.thread_data ();
@@ -122,7 +112,7 @@
fun message {message = msg, hard, location = loc, context = _} =
let
- val pos = position_of loc;
+ val pos = Exn_Properties.position_of loc;
val txt =
(if hard then "ML error" else "ML warning") ^ Position.here pos ^ ":\n" ^
Pretty.string_of (Pretty.from_ML (pretty_ml msg));
@@ -131,7 +121,7 @@
(* results *)
- val depth = get_print_depth ();
+ val depth = ML_Options.get_print_depth ();
fun apply_result {fixes, types, signatures, structures, functors, values} =
let
@@ -166,14 +156,14 @@
fun result_fun (phase1, phase2) () =
((case phase1 of
NONE => ()
- | SOME parse_tree => report_parse_tree depth space parse_tree);
+ | SOME parse_tree => report_parse_tree (#redirect flags) depth space parse_tree);
(case phase2 of
NONE => raise STATIC_ERRORS ()
| SOME code =>
apply_result
((code
- |> Runtime.debugging exn_message opt_context
- |> Runtime.toplevel_error (err o exn_message)) ())));
+ |> Runtime.debugging opt_context
+ |> Runtime.toplevel_error (err o Runtime.exn_message)) ())));
(* compiler invocation *)
@@ -185,7 +175,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 get_print_depth,
+ PolyML.Compiler.CPPrintDepth ML_Options.get_print_depth,
PolyML.Compiler.CPCompilerResultFun result_fun,
PolyML.Compiler.CPPrintInAlphabeticalOrder false];
val _ =
@@ -199,12 +189,12 @@
(case exn of
STATIC_ERRORS () => ""
| Runtime.TOPLEVEL_ERROR => ""
- | _ => "Exception- " ^ Pretty.string_of (pretty_exn exn) ^ " raised");
+ | _ => "Exception- " ^ Pretty.string_of (Exn_Output.pretty exn) ^ " raised");
val _ = output_warnings ();
val _ = output_writeln ();
in raise_error exn_msg end;
in
- if verbose then (output_warnings (); flush_error (); output_writeln ())
+ if #verbose flags then (output_warnings (); flush_error (); output_writeln ())
else ()
end;
--- a/src/Pure/ML/ml_context.ML Wed Mar 26 11:05:25 2014 -0700
+++ b/src/Pure/ML/ml_context.ML Thu Mar 27 21:38:45 2014 +0100
@@ -17,8 +17,6 @@
val add_antiquotation: binding -> (Args.src -> Proof.context -> decl * Proof.context) ->
theory -> theory
val print_antiquotations: Proof.context -> unit
- val source_trace_raw: Config.raw
- val source_trace: bool Config.T
val eval_antiquotes: ML_Lex.token Antiquote.antiquote list * Position.T ->
Context.generic option -> (ML_Lex.token list * ML_Lex.token list) * Context.generic option
val eval: ML_Compiler.flags -> Position.T -> ML_Lex.token Antiquote.antiquote list -> unit
@@ -137,21 +135,17 @@
in ((begin_env visible @ ml_env, ml_body), SOME (Context.Proof ctxt')) end;
in ((ml_env @ end_env, ml_body), opt_ctxt') end;
-val source_trace_raw = Config.declare "ML_source_trace" (fn _ => Config.Bool false);
-val source_trace = Config.bool source_trace_raw;
-
fun eval flags pos ants =
let
- val non_verbose = {SML = #SML flags, verbose = false};
+ val non_verbose = ML_Compiler.verbose false flags;
(*prepare source text*)
val ((env, body), env_ctxt) = eval_antiquotes (ants, pos) (Context.thread_data ());
val _ =
(case Option.map Context.proof_of env_ctxt of
SOME ctxt =>
- if Config.get ctxt source_trace then
- Context_Position.if_visible ctxt
- tracing (cat_lines [ML_Lex.flatten env, ML_Lex.flatten body])
+ if Config.get ctxt ML_Options.source_trace andalso Context_Position.is_visible ctxt
+ then tracing (cat_lines [ML_Lex.flatten env, ML_Lex.flatten body])
else ()
| NONE => ());
@@ -187,13 +181,14 @@
(fn () => eval_source flags source) ();
fun expression pos bind body ants =
- exec (fn () => eval {SML = false, verbose = false} pos
- (ML_Lex.read Position.none ("Context.set_thread_data (SOME (let " ^ bind ^ " = ") @ ants @
+ exec (fn () =>
+ eval ML_Compiler.flags pos
+ (ML_Lex.read Position.none ("Context.set_thread_data (SOME (let " ^ bind ^ " = ") @ ants @
ML_Lex.read Position.none (" in " ^ body ^ " end (ML_Context.the_generic_context ())));")));
end;
fun use s =
- ML_Context.eval_file {SML = false, verbose = true} (Path.explode s)
+ ML_Context.eval_file (ML_Compiler.verbose true ML_Compiler.flags) (Path.explode s)
handle ERROR msg => (writeln msg; error "ML error");
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML/ml_options.ML Thu Mar 27 21:38:45 2014 +0100
@@ -0,0 +1,49 @@
+(* Title: Pure/ML/ml_options.ML
+ Author: Makarius
+
+ML configuration options.
+*)
+
+signature ML_OPTIONS =
+sig
+ val source_trace_raw: Config.raw
+ val source_trace: bool Config.T
+ val exception_trace_raw: Config.raw
+ val exception_trace: bool Config.T
+ val exception_trace_enabled: Context.generic option -> bool
+ val print_depth_raw: Config.raw
+ val print_depth: int Config.T
+ val get_print_depth: unit -> int
+end;
+
+structure ML_Options: ML_OPTIONS =
+struct
+
+(* source trace *)
+
+val source_trace_raw = Config.declare "ML_source_trace" (fn _ => Config.Bool false);
+val source_trace = Config.bool source_trace_raw;
+
+
+(* exception trace *)
+
+val exception_trace_raw = Config.declare_option "ML_exception_trace";
+val exception_trace = Config.bool exception_trace_raw;
+
+fun exception_trace_enabled NONE =
+ (Options.default_bool (Config.name_of exception_trace_raw) handle ERROR _ => false)
+ | exception_trace_enabled (SOME context) = Config.get_generic context exception_trace;
+
+
+(* print depth *)
+
+val print_depth_raw =
+ Config.declare "ML_print_depth" (fn _ => Config.Int (get_default_print_depth ()));
+val print_depth = Config.int print_depth_raw;
+
+fun get_print_depth () =
+ (case Context.thread_data () of
+ NONE => get_default_print_depth ()
+ | SOME context => Config.get_generic context print_depth);
+
+end;
--- a/src/Pure/ML/ml_thms.ML Wed Mar 26 11:05:25 2014 -0700
+++ b/src/Pure/ML/ml_thms.ML Thu Mar 27 21:38:45 2014 +0100
@@ -130,7 +130,7 @@
else if not (ML_Syntax.is_identifier name) then
error ("Cannot bind theorem(s) " ^ quote name ^ " as ML value")
else
- ML_Compiler.eval {SML = false, verbose = true} Position.none
+ ML_Compiler.eval (ML_Compiler.verbose true ML_Compiler.flags) Position.none
(ML_Lex.tokenize ("val " ^ name ^ " = " ^ get ^ " ();"));
val _ = Theory.setup (Stored_Thms.put []);
in () end;
--- a/src/Pure/PIDE/command.ML Wed Mar 26 11:05:25 2014 -0700
+++ b/src/Pure/PIDE/command.ML Thu Mar 27 21:38:45 2014 +0100
@@ -20,7 +20,7 @@
eval -> print list -> print list option
type print_fn = Toplevel.transition -> Toplevel.state -> unit
type print_function =
- {command_name: string, args: string list} ->
+ {command_name: string, args: string list, exec_id: Document_ID.exec} ->
{delay: Time.time option, pri: int, persistent: bool, strict: bool, print_fn: print_fn} option
val print_function: string -> print_function -> unit
val no_print_function: string -> unit
@@ -172,9 +172,10 @@
datatype eval = Eval of {exec_id: Document_ID.exec, eval_process: eval_state memo};
-fun eval_eq (Eval {exec_id, ...}, Eval {exec_id = exec_id', ...}) = exec_id = exec_id';
+fun eval_exec_id (Eval {exec_id, ...}) = exec_id;
+val eval_eq = op = o pairself eval_exec_id;
-fun eval_running (Eval {exec_id, ...}) = Execution.is_running_exec exec_id;
+val eval_running = Execution.is_running_exec o eval_exec_id;
fun eval_finished (Eval {eval_process, ...}) = memo_finished eval_process;
fun eval_result (Eval {eval_process, ...}) = memo_result eval_process;
@@ -195,7 +196,7 @@
(Thy_Output.check_text (Token.source_position_of cmt) st'; [])
handle exn =>
if Exn.is_interrupt exn then reraise exn
- else ML_Compiler.exn_messages_ids exn)) ();
+ else Runtime.exn_messages_ids exn)) ();
fun report tr m =
Toplevel.setmp_thread_position tr (fn () => Output.report (Markup.markup_only m)) ();
@@ -260,10 +261,13 @@
{name: string, args: string list, delay: Time.time option, pri: int, persistent: bool,
exec_id: Document_ID.exec, print_process: unit memo};
+fun print_exec_id (Print {exec_id, ...}) = exec_id;
+val print_eq = op = o pairself print_exec_id;
+
type print_fn = Toplevel.transition -> Toplevel.state -> unit;
type print_function =
- {command_name: string, args: string list} ->
+ {command_name: string, args: string list, exec_id: Document_ID.exec} ->
{delay: Time.time option, pri: int, persistent: bool, strict: bool, print_fn: print_fn} option;
local
@@ -272,12 +276,10 @@
Synchronized.var "Command.print_functions" ([]: (string * print_function) list);
fun print_error tr opt_context e =
- (Toplevel.setmp_thread_position tr o Toplevel.controlled_execution opt_context) e ()
+ (Toplevel.setmp_thread_position tr o Runtime.controlled_execution opt_context) e ()
handle exn =>
if Exn.is_interrupt exn then reraise exn
- else List.app (Future.error_msg (Toplevel.pos_of tr)) (ML_Compiler.exn_messages_ids exn);
-
-fun print_eq (Print {exec_id, ...}, Print {exec_id = exec_id', ...}) = exec_id = exec_id';
+ else List.app (Future.error_msg (Toplevel.pos_of tr)) (Runtime.exn_messages_ids exn);
fun print_finished (Print {print_process, ...}) = memo_finished print_process;
@@ -315,9 +317,9 @@
fun new_print name args get_pr =
let
- val params = {command_name = command_name, args = args};
+ val params = {command_name = command_name, args = args, exec_id = eval_exec_id eval};
in
- (case Exn.capture (Toplevel.controlled_execution NONE get_pr) params of
+ (case Exn.capture (Runtime.controlled_execution NONE get_pr) params of
Exn.Res NONE => NONE
| Exn.Res (SOME pr) => SOME (make_print name args pr)
| Exn.Exn exn => SOME (bad_print name args exn))
@@ -353,6 +355,14 @@
end;
val _ =
+ print_function "Execution.print"
+ (fn {args, exec_id, ...} =>
+ if null args then
+ SOME {delay = NONE, pri = 1, persistent = false, strict = true,
+ print_fn = fn _ => fn _ => Execution.fork_prints exec_id}
+ else NONE);
+
+val _ =
print_function "print_state"
(fn {command_name, ...} =>
SOME {delay = NONE, pri = 1, persistent = false, strict = true,
@@ -373,8 +383,7 @@
(Eval {exec_id = Document_ID.none, eval_process = memo_value init_eval_state}, []);
fun exec_ids NONE = []
- | exec_ids (SOME (Eval {exec_id, ...}, prints)) =
- exec_id :: map (fn Print {exec_id, ...} => exec_id) prints;
+ | exec_ids (SOME (eval, prints)) = eval_exec_id eval :: map print_exec_id prints;
local
--- a/src/Pure/PIDE/command.scala Wed Mar 26 11:05:25 2014 -0700
+++ b/src/Pure/PIDE/command.scala Thu Mar 27 21:38:45 2014 +0100
@@ -27,8 +27,8 @@
{
type Entry = (Long, XML.Tree)
val empty = new Results(SortedMap.empty)
- def make(es: Iterable[Results.Entry]): Results = (empty /: es.iterator)(_ + _)
- def merge(rs: Iterable[Results]): Results = (empty /: rs.iterator)(_ ++ _)
+ def make(es: List[Results.Entry]): Results = (empty /: es)(_ + _)
+ def merge(rs: List[Results]): Results = (empty /: rs)(_ ++ _)
}
final class Results private(private val rep: SortedMap[Long, XML.Tree])
@@ -81,11 +81,6 @@
def add(index: Markup_Index, markup: Text.Markup): Markups =
new Markups(rep + (index -> (this(index) + markup)))
- def ++ (other: Markups): Markups =
- new Markups(
- (rep.keySet ++ other.rep.keySet)
- .map(index => index -> (this(index) ++ other(index))).toMap)
-
override def hashCode: Int = rep.hashCode
override def equals(that: Any): Boolean =
that match {
@@ -98,6 +93,16 @@
/* state */
+ object State
+ {
+ def merge_results(states: List[State]): Command.Results =
+ Results.merge(states.map(_.results))
+
+ def merge_markup(states: List[State], index: Markup_Index,
+ range: Text.Range, elements: Document.Elements): Markup_Tree =
+ Markup_Tree.merge(states.map(_.markup(index)), range, elements)
+ }
+
sealed case class State(
command: Command,
status: List[Markup] = Nil,
@@ -108,9 +113,6 @@
def markup(index: Markup_Index): Markup_Tree = markups(index)
- def markup_to_XML(filter: XML.Elem => Boolean): XML.Body =
- markup(Markup_Index.markup).to_XML(command.range, command.source, filter)
-
/* content */
@@ -132,7 +134,7 @@
copy(markups = markups1.add(Markup_Index(false, file_name), m))
}
- def + (alt_id: Document_ID.Generic, message: XML.Elem): State =
+ def + (valid_id: Document_ID.Generic => Boolean, message: XML.Elem): State =
message match {
case XML.Elem(Markup(Markup.STATUS, _), msgs) =>
(this /: msgs)((state, msg) =>
@@ -154,7 +156,7 @@
msg match {
case XML.Elem(Markup(name,
atts @ Position.Reported(id, file_name, symbol_range)), args)
- if id == command.id || id == alt_id =>
+ if valid_id(id) =>
command.chunks.get(file_name) match {
case Some(chunk) =>
chunk.incorporate(symbol_range) match {
@@ -187,7 +189,7 @@
if (Protocol.is_inlined(message)) {
for {
(file_name, chunk) <- command.chunks
- range <- Protocol.message_positions(command.id, alt_id, chunk, message)
+ range <- Protocol.message_positions(valid_id, chunk, message)
} st = st.add_markup(false, file_name, Text.Info(range, message2))
}
st
@@ -196,14 +198,7 @@
System.err.println("Ignored message without serial number: " + message)
this
}
- }
-
- def ++ (other: State): State =
- copy(
- status = other.status ::: status,
- results = results ++ other.results,
- markups = markups ++ other.markups
- )
+ }
}
--- a/src/Pure/PIDE/document.scala Wed Mar 26 11:05:25 2014 -0700
+++ b/src/Pure/PIDE/document.scala Thu Mar 27 21:38:45 2014 +0100
@@ -429,13 +429,13 @@
range: Text.Range,
info: A,
elements: Elements,
- result: Command.State => (A, Text.Markup) => Option[A],
+ result: Command.Results => (A, Text.Markup) => Option[A],
status: Boolean = false): List[Text.Info[A]]
def select[A](
range: Text.Range,
elements: Elements,
- result: Command.State => Text.Markup => Option[A],
+ result: Command.Results => Text.Markup => Option[A],
status: Boolean = false): List[Text.Info[A]]
}
@@ -521,15 +521,19 @@
def the_dynamic_state(id: Document_ID.Exec): Command.State = execs.getOrElse(id, fail)
def the_assignment(version: Version): State.Assignment = assignments.getOrElse(version.id, fail)
+ def valid_id(st: Command.State)(id: Document_ID.Generic): Boolean =
+ id == st.command.id ||
+ (execs.get(id) match { case Some(st1) => st1.command.id == st.command.id case None => false })
+
def accumulate(id: Document_ID.Generic, message: XML.Elem): (Command.State, State) =
execs.get(id) match {
case Some(st) =>
- val new_st = st + (id, message)
+ val new_st = st + (valid_id(st), message)
(new_st, copy(execs = execs + (id -> new_st)))
case None =>
commands.get(id) match {
case Some(st) =>
- val new_st = st + (id, message)
+ val new_st = st + (valid_id(st), message)
(new_st, copy(commands = commands + (id -> new_st)))
case None => fail
}
@@ -626,25 +630,37 @@
assignments = assignments1)
}
- def command_state(version: Version, command: Command): Command.State =
+ def command_states(version: Version, command: Command): List[Command.State] =
{
require(is_assigned(version))
try {
the_assignment(version).check_finished.command_execs.getOrElse(command.id, Nil)
.map(the_dynamic_state(_)) match {
- case eval_state :: print_states => (eval_state /: print_states)(_ ++ _)
case Nil => fail
+ case states => states
}
}
catch {
case _: State.Fail =>
- try { the_static_state(command.id) }
- catch { case _: State.Fail => command.init_state }
+ try { List(the_static_state(command.id)) }
+ catch { case _: State.Fail => List(command.init_state) }
}
}
- def markup_to_XML(version: Version, node: Node, filter: XML.Elem => Boolean): XML.Body =
- node.commands.toList.map(cmd => command_state(version, cmd).markup_to_XML(filter)).flatten
+ def command_results(version: Version, command: Command): Command.Results =
+ Command.State.merge_results(command_states(version, command))
+
+ def command_markup(version: Version, command: Command, index: Command.Markup_Index,
+ range: Text.Range, elements: Elements): Markup_Tree =
+ Command.State.merge_markup(command_states(version, command), index, range, elements)
+
+ def markup_to_XML(version: Version, node: Node, elements: Elements): XML.Body =
+ (for {
+ command <- node.commands.iterator
+ markup =
+ command_markup(version, command, Command.Markup_Index.markup, command.range, elements)
+ tree <- markup.to_XML(command.range, command.source, elements)
+ } yield tree).toList
// persistent user-view
def snapshot(name: Node.Name = Node.Name.empty, pending_edits: List[Text.Edit] = Nil)
@@ -687,8 +703,12 @@
def eq_content(other: Snapshot): Boolean =
{
def eq_commands(commands: (Command, Command)): Boolean =
- state.command_state(version, commands._1) eq_content
- other.state.command_state(other.version, commands._2)
+ {
+ val states1 = state.command_states(version, commands._1)
+ val states2 = other.state.command_states(other.version, commands._2)
+ states1.length == states2.length &&
+ (states1 zip states2).forall({ case (st1, st2) => st1 eq_content st2 })
+ }
!is_outdated && !other.is_outdated &&
node.commands.size == other.node.commands.size &&
@@ -704,48 +724,39 @@
range: Text.Range,
info: A,
elements: Elements,
- result: Command.State => (A, Text.Markup) => Option[A],
+ result: Command.Results => (A, Text.Markup) => Option[A],
status: Boolean = false): List[Text.Info[A]] =
{
val former_range = revert(range)
- thy_load_commands match {
- case thy_load_command :: _ =>
- val file_name = node_name.node
- val markup_index = Command.Markup_Index(status, file_name)
- (for {
- chunk <- thy_load_command.chunks.get(file_name).iterator
- st = state.command_state(version, thy_load_command)
- res = result(st)
- Text.Info(r0, a) <- st.markup(markup_index).cumulate[A](
- former_range.restrict(chunk.range), info, elements,
- { case (a, Text.Info(r0, b)) => res(a, Text.Info(convert(r0), b)) }
- ).iterator
- } yield Text.Info(convert(r0), a)).toList
-
- case _ =>
- val markup_index = Command.Markup_Index(status, "")
- (for {
- (command, command_start) <- node.command_range(former_range)
- st = state.command_state(version, command)
- res = result(st)
- Text.Info(r0, a) <- st.markup(markup_index).cumulate[A](
- (former_range - command_start).restrict(command.range), info, elements,
- {
- case (a, Text.Info(r0, b)) => res(a, Text.Info(convert(r0 + command_start), b))
- }).iterator
- } yield Text.Info(convert(r0 + command_start), a)).toList
- }
+ val (file_name, command_range_iterator) =
+ thy_load_commands match {
+ case command :: _ => (node_name.node, Iterator((command, 0)))
+ case _ => ("", node.command_range(former_range))
+ }
+ val markup_index = Command.Markup_Index(status, file_name)
+ (for {
+ (command, command_start) <- command_range_iterator
+ chunk <- command.chunks.get(file_name).iterator
+ states = state.command_states(version, command)
+ res = result(Command.State.merge_results(states))
+ range = (former_range - command_start).restrict(chunk.range)
+ markup = Command.State.merge_markup(states, markup_index, range, elements)
+ Text.Info(r0, a) <- markup.cumulate[A](range, info, elements,
+ {
+ case (a, Text.Info(r0, b)) => res(a, Text.Info(convert(r0 + command_start), b))
+ }).iterator
+ } yield Text.Info(convert(r0 + command_start), a)).toList
}
def select[A](
range: Text.Range,
elements: Elements,
- result: Command.State => Text.Markup => Option[A],
+ result: Command.Results => Text.Markup => Option[A],
status: Boolean = false): List[Text.Info[A]] =
{
- def result1(st: Command.State): (Option[A], Text.Markup) => Option[Option[A]] =
+ def result1(results: Command.Results): (Option[A], Text.Markup) => Option[Option[A]] =
{
- val res = result(st)
+ val res = result(results)
(_: Option[A], x: Text.Markup) =>
res(x) match {
case None => None
--- a/src/Pure/PIDE/execution.ML Wed Mar 26 11:05:25 2014 -0700
+++ b/src/Pure/PIDE/execution.ML Thu Mar 27 21:38:45 2014 +0100
@@ -15,7 +15,10 @@
val peek: Document_ID.exec -> Future.group list
val cancel: Document_ID.exec -> unit
val terminate: Document_ID.exec -> unit
- val fork: {name: string, pos: Position.T, pri: int} -> (unit -> 'a) -> 'a future
+ type params = {name: string, pos: Position.T, pri: int}
+ val fork: params -> (unit -> 'a) -> 'a future
+ val print: params -> (unit -> unit) -> unit
+ val fork_prints: Document_ID.exec -> unit
val purge: Document_ID.exec list -> unit
val reset: unit -> Future.group list
val shutdown: unit -> unit
@@ -26,18 +29,20 @@
(* global state *)
-datatype state = State of
- {execution: Document_ID.execution, (*overall document execution*)
- execs: Future.group list Inttab.table}; (*command execs with registered forks*)
+type print = {name: string, pri: int, body: unit -> unit};
+type exec_state = Future.group list * print list; (*active forks, prints*)
+type state =
+ Document_ID.execution * (*overall document execution*)
+ exec_state Inttab.table; (*running command execs*)
-fun make_state (execution, execs) = State {execution = execution, execs = execs};
-fun map_state f (State {execution, execs}) = make_state (f (execution, execs));
-
-val init_state = make_state (Document_ID.none, Inttab.make [(Document_ID.none, [])]);
+val init_state: state = (Document_ID.none, Inttab.make [(Document_ID.none, ([], []))]);
val state = Synchronized.var "Execution.state" init_state;
-fun get_state () = let val State args = Synchronized.value state in args end;
-fun change_state f = Synchronized.change state (map_state f);
+fun get_state () = Synchronized.value state;
+fun change_state_result f = Synchronized.change_result state f;
+fun change_state f = Synchronized.change state f;
+
+fun unregistered exec_id = "Unregistered execution: " ^ Document_ID.print exec_id;
(* unique running execution *)
@@ -50,29 +55,30 @@
fun discontinue () = change_state (apfst (K Document_ID.none));
-fun is_running execution_id = execution_id = #execution (get_state ());
+fun is_running execution_id = execution_id = #1 (get_state ());
(* execs *)
fun is_running_exec exec_id =
- Inttab.defined (#execs (get_state ())) exec_id;
+ Inttab.defined (#2 (get_state ())) exec_id;
fun running execution_id exec_id groups =
- Synchronized.change_result state
- (fn State {execution = execution_id', execs} =>
- let
- val continue = execution_id = execution_id';
- val execs' =
- if continue then
- Inttab.update_new (exec_id, groups) execs
- handle Inttab.DUP dup =>
- raise Fail ("Execution already registered: " ^ Document_ID.print dup)
- else execs;
- in (continue, make_state (execution_id', execs')) end);
+ change_state_result (fn (execution_id', execs) =>
+ let
+ val continue = execution_id = execution_id';
+ val execs' =
+ if continue then
+ Inttab.update_new (exec_id, (groups, [])) execs
+ handle Inttab.DUP dup =>
+ raise Fail ("Execution already registered: " ^ Document_ID.print dup)
+ else execs;
+ in (continue, (execution_id', execs')) end);
fun peek exec_id =
- Inttab.lookup_list (#execs (get_state ())) exec_id;
+ (case Inttab.lookup (#2 (get_state ())) exec_id of
+ SOME (groups, _) => groups
+ | NONE => []);
fun cancel exec_id = List.app Future.cancel_group (peek exec_id);
fun terminate exec_id = List.app Future.terminate (peek exec_id);
@@ -81,18 +87,24 @@
(* fork *)
fun status task markups =
- let val props = Markup.properties [(Markup.taskN, Task_Queue.str_of_task task)]
- in Output.status (implode (map (Markup.markup_only o props) markups)) end;
+ let
+ val props =
+ if ! Multithreading.trace >= 2
+ then [(Markup.taskN, Task_Queue.str_of_task task)] else [];
+ in Output.status (implode (map (Markup.markup_only o Markup.properties props) markups)) end;
-fun fork {name, pos, pri} e =
+type params = {name: string, pos: Position.T, pri: int};
+
+fun fork ({name, pos, pri}: params) e =
uninterruptible (fn _ => Position.setmp_thread_data pos (fn () =>
let
val exec_id = the_default 0 (Position.parse_id pos);
val group = Future.worker_subgroup ();
val _ = change_state (apsnd (fn execs =>
- if Inttab.defined execs exec_id
- then Inttab.cons_list (exec_id, group) execs
- else raise Fail ("Cannot fork from unregistered execution: " ^ Document_ID.print exec_id)));
+ (case Inttab.lookup execs exec_id of
+ SOME (groups, prints) =>
+ Inttab.update (exec_id, (group :: groups, prints)) execs
+ | NONE => raise Fail (unregistered exec_id))));
val future =
(singleton o Future.forks)
@@ -112,7 +124,7 @@
status task [Markup.finished];
Output.report (Markup.markup_only Markup.bad);
if exec_id = 0 then ()
- else List.app (Future.error_msg pos) (ML_Compiler.exn_messages_ids exn))
+ else List.app (Future.error_msg pos) (Runtime.exn_messages_ids exn))
| Exn.Res _ =>
status task [Markup.finished])
in Exn.release result end);
@@ -121,6 +133,32 @@
in future end)) ();
+(* print *)
+
+fun print ({name, pos, pri}: params) e =
+ change_state (apsnd (fn execs =>
+ let
+ val exec_id = the_default 0 (Position.parse_id pos);
+ val print = {name = name, pri = pri, body = e};
+ in
+ (case Inttab.lookup execs exec_id of
+ SOME (groups, prints) => Inttab.update (exec_id, (groups, print :: prints)) execs
+ | NONE => raise Fail (unregistered exec_id))
+ end));
+
+fun fork_prints exec_id =
+ (case Inttab.lookup (#2 (get_state ())) exec_id of
+ SOME (_, prints) =>
+ if null prints orelse null (tl prints) orelse not (Multithreading.enabled ())
+ then List.app (fn {body, ...} => body ()) (rev prints)
+ else
+ let val pos = Position.thread_data () in
+ List.app (fn {name, pri, body} =>
+ ignore (fork {name = name, pos = pos, pri = pri} body)) (rev prints)
+ end
+ | NONE => raise Fail (unregistered exec_id));
+
+
(* cleanup *)
fun purge exec_ids =
@@ -128,7 +166,7 @@
let
val execs' = fold Inttab.delete_safe exec_ids execs;
val () =
- (execs', ()) |-> Inttab.fold (fn (exec_id, groups) => fn () =>
+ (execs', ()) |-> Inttab.fold (fn (exec_id, (groups, _)) => fn () =>
if Inttab.defined execs' exec_id then ()
else groups |> List.app (fn group =>
if Task_Queue.is_canceled group then ()
@@ -136,8 +174,8 @@
in execs' end);
fun reset () =
- Synchronized.change_result state (fn State {execs, ...} =>
- let val groups = Inttab.fold (append o #2) execs []
+ change_state_result (fn (_, execs) =>
+ let val groups = Inttab.fold (append o #1 o #2) execs []
in (groups, init_state) end);
fun shutdown () =
--- a/src/Pure/PIDE/markup_tree.scala Wed Mar 26 11:05:25 2014 -0700
+++ b/src/Pure/PIDE/markup_tree.scala Thu Mar 27 21:38:45 2014 +0100
@@ -20,6 +20,9 @@
val empty: Markup_Tree = new Markup_Tree(Branches.empty)
+ def merge(trees: List[Markup_Tree], range: Text.Range, elements: Document.Elements): Markup_Tree =
+ (empty /: trees)(_.merge(_, range, elements))
+
def merge_disjoint(trees: List[Markup_Tree]): Markup_Tree =
trees match {
case Nil => empty
@@ -113,12 +116,6 @@
private def this(branches: Markup_Tree.Branches.T, entry: Markup_Tree.Entry) =
this(branches + (entry.range -> entry))
- override def toString =
- branches.toList.map(_._2) match {
- case Nil => "Empty"
- case list => list.mkString("Tree(", ",", ")")
- }
-
private def overlapping(range: Text.Range): Branches.T =
{
val start = Text.Range(range.start)
@@ -130,6 +127,11 @@
}
}
+ def restrict(range: Text.Range): Markup_Tree =
+ new Markup_Tree(overlapping(range))
+
+ def is_empty: Boolean = branches.isEmpty
+
def + (new_markup: Text.Markup): Markup_Tree =
{
val new_range = new_markup.range
@@ -156,44 +158,26 @@
}
}
- def ++ (other: Markup_Tree): Markup_Tree =
- (this /: other.branches)({ case (tree, (range, entry)) =>
- ((tree ++ entry.subtree) /: entry.markup)({ case (t, elem) => t + Text.Info(range, elem) }) })
-
- def to_XML(root_range: Text.Range, text: CharSequence, filter: XML.Elem => Boolean): XML.Body =
+ def merge(other: Markup_Tree, root_range: Text.Range, elements: Document.Elements): Markup_Tree =
{
- def make_text(start: Text.Offset, stop: Text.Offset): XML.Body =
- if (start == stop) Nil
- else List(XML.Text(text.subSequence(start, stop).toString))
-
- def make_elems(rev_markups: List[XML.Elem], body: XML.Body): XML.Body =
- (body /: rev_markups) {
- case (b, elem) =>
- if (!filter(elem)) b
- else if (elem.body.isEmpty) List(XML.Elem(elem.markup, b))
- else List(XML.Wrapped_Elem(elem.markup, elem.body, b))
- }
+ def merge_trees(tree1: Markup_Tree, tree2: Markup_Tree): Markup_Tree =
+ (tree1 /: tree2.branches)(
+ { case (tree, (range, entry)) =>
+ if (!range.overlaps(root_range)) tree
+ else
+ (merge_trees(tree, entry.subtree) /: entry.filter_markup(elements))(
+ { case (t, elem) => t + Text.Info(range, elem) })
+ })
- def make_body(elem_range: Text.Range, elem_markup: List[XML.Elem], entries: Branches.T)
- : XML.Body =
- {
- val body = new mutable.ListBuffer[XML.Tree]
- var last = elem_range.start
- for ((range, entry) <- entries) {
- val subrange = range.restrict(elem_range)
- body ++= make_text(last, subrange.start)
- body ++= make_body(subrange, entry.rev_markup, entry.subtree.overlapping(subrange))
- last = subrange.stop
- }
- body ++= make_text(last, elem_range.stop)
- make_elems(elem_markup, body.toList)
+ if (this eq other) this
+ else {
+ val tree1 = this.restrict(root_range)
+ val tree2 = other.restrict(root_range)
+ if (tree1.is_empty) tree2
+ else merge_trees(tree1, tree2)
}
- make_body(root_range, Nil, overlapping(root_range))
}
- def to_XML(text: CharSequence): XML.Body =
- to_XML(Text.Range(0, text.length), text, (_: XML.Elem) => true)
-
def cumulate[A](root_range: Text.Range, root_info: A, elements: Document.Elements,
result: (A, Text.Markup) => Option[A]): List[Text.Info[A]] =
{
@@ -242,5 +226,42 @@
traverse(root_range.start,
List((Text.Info(root_range, root_info), overlapping(root_range).toList)))
}
+
+ def to_XML(root_range: Text.Range, text: CharSequence, elements: Document.Elements): XML.Body =
+ {
+ def make_text(start: Text.Offset, stop: Text.Offset): XML.Body =
+ if (start == stop) Nil
+ else List(XML.Text(text.subSequence(start, stop).toString))
+
+ def make_elems(rev_markups: List[XML.Elem], body: XML.Body): XML.Body =
+ (body /: rev_markups) {
+ case (b, elem) =>
+ if (!elements(elem.name)) b
+ else if (elem.body.isEmpty) List(XML.Elem(elem.markup, b))
+ else List(XML.Wrapped_Elem(elem.markup, elem.body, b))
+ }
+
+ def make_body(elem_range: Text.Range, elem_markup: List[XML.Elem], entries: Branches.T)
+ : XML.Body =
+ {
+ val body = new mutable.ListBuffer[XML.Tree]
+ var last = elem_range.start
+ for ((range, entry) <- entries) {
+ val subrange = range.restrict(elem_range)
+ body ++= make_text(last, subrange.start)
+ body ++= make_body(subrange, entry.rev_markup, entry.subtree.overlapping(subrange))
+ last = subrange.stop
+ }
+ body ++= make_text(last, elem_range.stop)
+ make_elems(elem_markup, body.toList)
+ }
+ make_body(root_range, Nil, overlapping(root_range))
+ }
+
+ override def toString =
+ branches.toList.map(_._2) match {
+ case Nil => "Empty"
+ case list => list.mkString("Tree(", ",", ")")
+ }
}
--- a/src/Pure/PIDE/protocol.scala Wed Mar 26 11:05:25 2014 -0700
+++ b/src/Pure/PIDE/protocol.scala Thu Mar 27 21:38:45 2014 +0100
@@ -74,8 +74,11 @@
case _ => status
}
- def command_status(markups: List[Markup]): Status =
- (Status.init /: markups)(command_status(_, _))
+ def command_status(status: Status, state: Command.State): Status =
+ (status /: state.status)(command_status(_, _))
+
+ def command_status(status: Status, states: List[Command.State]): Status =
+ (status /: states)(command_status(_, _))
val command_status_elements =
Document.Elements(Markup.ACCEPTED, Markup.FORKED, Markup.JOINED, Markup.RUNNING,
@@ -117,18 +120,19 @@
var finished = 0
var warned = 0
var failed = 0
- node.commands.foreach(command =>
- {
- val st = state.command_state(version, command)
- val status = command_status(st.status)
- if (status.is_running) running += 1
- else if (status.is_finished) {
- if (st.results.entries.exists(p => is_warning(p._2))) warned += 1
- else finished += 1
- }
- else if (status.is_failed) failed += 1
- else unprocessed += 1
- })
+ for {
+ command <- node.commands
+ states = state.command_states(version, command)
+ status = command_status(Status.init, states)
+ } {
+ if (status.is_running) running += 1
+ else if (status.is_finished) {
+ val warning = states.exists(st => st.results.entries.exists(p => is_warning(p._2)))
+ if (warning) warned += 1 else finished += 1
+ }
+ else if (status.is_failed) failed += 1
+ else unprocessed += 1
+ }
Node_Status(unprocessed, running, finished, warned, failed)
}
@@ -149,7 +153,7 @@
var commands = Map.empty[Command, Double]
for {
command <- node.commands.iterator
- st = state.command_state(version, command)
+ st <- state.command_states(version, command)
command_timing =
(0.0 /: st.status)({
case (timing, Markup.Timing(t)) => timing + t.elapsed.seconds
@@ -280,15 +284,14 @@
Document.Elements(Markup.BINDING, Markup.ENTITY, Markup.REPORT, Markup.POSITION)
def message_positions(
- command_id: Document_ID.Command,
- alt_id: Document_ID.Generic,
+ valid_id: Document_ID.Generic => Boolean,
chunk: Command.Chunk,
message: XML.Elem): Set[Text.Range] =
{
def elem_positions(props: Properties.T, set: Set[Text.Range]): Set[Text.Range] =
props match {
case Position.Reported(id, file_name, symbol_range)
- if (id == command_id || id == alt_id) && file_name == chunk.file_name =>
+ if valid_id(id) && file_name == chunk.file_name =>
chunk.incorporate(symbol_range) match {
case Some(range) => set + range
case _ => set
--- a/src/Pure/PIDE/query_operation.ML Wed Mar 26 11:05:25 2014 -0700
+++ b/src/Pure/PIDE/query_operation.ML Thu Mar 27 21:38:45 2014 +0100
@@ -24,7 +24,7 @@
fun status m = result (Markup.markup_only m);
fun output_result s = result (Markup.markup (Markup.writelnN, []) s);
fun toplevel_error exn =
- result (Markup.markup (Markup.errorN, []) (ML_Compiler.exn_message exn));
+ result (Markup.markup (Markup.errorN, []) (Runtime.exn_message exn));
val _ = status Markup.running;
fun run () = f {state = state, args = args, output_result = output_result};
--- a/src/Pure/PIDE/query_operation.scala Wed Mar 26 11:05:25 2014 -0700
+++ b/src/Pure/PIDE/query_operation.scala Thu Mar 27 21:38:45 2014 +0100
@@ -70,20 +70,20 @@
/* snapshot */
- val (snapshot, state, removed) =
+ val (snapshot, command_results, removed) =
current_location match {
case Some(cmd) =>
val snapshot = editor.node_snapshot(cmd.node_name)
- val state = snapshot.state.command_state(snapshot.version, cmd)
+ val command_results = snapshot.state.command_results(snapshot.version, cmd)
val removed = !snapshot.version.nodes(cmd.node_name).commands.contains(cmd)
- (snapshot, state, removed)
+ (snapshot, command_results, removed)
case None =>
- (Document.Snapshot.init, Command.empty.init_state, true)
+ (Document.Snapshot.init, Command.Results.empty, true)
}
val results =
(for {
- (_, elem @ XML.Elem(Markup(Markup.RESULT, props), _)) <- state.results.entries
+ (_, elem @ XML.Elem(Markup(Markup.RESULT, props), _)) <- command_results.entries
if props.contains((Markup.INSTANCE, instance))
} yield elem).toList
@@ -154,7 +154,7 @@
current_update_pending = false
if (current_output != new_output && !removed) {
current_output = new_output
- consume_output(snapshot, state.results, new_output)
+ consume_output(snapshot, command_results, new_output)
}
if (current_status != new_status) {
current_status = new_status
--- a/src/Pure/PIDE/resources.ML Wed Mar 26 11:05:25 2014 -0700
+++ b/src/Pure/PIDE/resources.ML Thu Mar 27 21:38:45 2014 +0100
@@ -211,9 +211,10 @@
val msg = "Bad file: " ^ Path.print path' ^ Position.here pos;
in
if strict then error msg
- else
- Context_Position.if_visible ctxt Output.report
+ else if Context_Position.is_visible ctxt then
+ Output.report
(Markup.markup (Markup.bad |> Markup.properties (Position.properties_of pos)) msg)
+ else ()
end;
in path end;
--- a/src/Pure/PIDE/text.scala Wed Mar 26 11:05:25 2014 -0700
+++ b/src/Pure/PIDE/text.scala Thu Mar 27 21:38:45 2014 +0100
@@ -45,8 +45,8 @@
def length: Int = stop - start
def map(f: Offset => Offset): Range = Range(f(start), f(stop))
- def +(i: Offset): Range = map(_ + i)
- def -(i: Offset): Range = map(_ - i)
+ def +(i: Offset): Range = if (i == 0) this else map(_ + i)
+ def -(i: Offset): Range = if (i == 0) this else map(_ - i)
def is_singularity: Boolean = start == stop
--- a/src/Pure/ROOT Wed Mar 26 11:05:25 2014 -0700
+++ b/src/Pure/ROOT Thu Mar 27 21:38:45 2014 +0100
@@ -139,6 +139,8 @@
"Isar/token.ML"
"Isar/toplevel.ML"
"Isar/typedecl.ML"
+ "ML/exn_output.ML"
+ "ML/exn_output_polyml.ML"
"ML/exn_properties_dummy.ML"
"ML/exn_properties_polyml.ML"
"ML/exn_trace_polyml-5.5.1.ML"
@@ -150,6 +152,7 @@
"ML/ml_env.ML"
"ML/ml_lex.ML"
"ML/ml_parse.ML"
+ "ML/ml_options.ML"
"ML/ml_statistics_dummy.ML"
"ML/ml_statistics_polyml-5.5.0.ML"
"ML/ml_syntax.ML"
--- a/src/Pure/ROOT.ML Wed Mar 26 11:05:25 2014 -0700
+++ b/src/Pure/ROOT.ML Thu Mar 27 21:38:45 2014 +0100
@@ -69,6 +69,7 @@
use "PIDE/xml.ML";
use "PIDE/yxml.ML";
+use "PIDE/document_id.ML";
use "General/change_table.ML";
use "General/graph.ML";
@@ -193,16 +194,18 @@
(* Isar -- Intelligible Semi-Automated Reasoning *)
-(*ML support*)
+(*ML support and global execution*)
use "ML/ml_syntax.ML";
use "ML/ml_env.ML";
+use "ML/ml_options.ML";
+use "ML/exn_output.ML";
+if ML_System.is_polyml then use "ML/exn_output_polyml.ML" else ();
+use "ML/ml_options.ML";
use "Isar/runtime.ML";
+use "PIDE/execution.ML";
use "ML/ml_compiler.ML";
if ML_System.is_polyml then use "ML/ml_compiler_polyml.ML" else ();
-(*global execution*)
-use "PIDE/document_id.ML";
-use "PIDE/execution.ML";
use "skip_proof.ML";
use "goal.ML";
@@ -346,7 +349,7 @@
(* the Pure theory *)
use "pure_syn.ML";
-Toplevel.program (fn () => Thy_Info.use_thy ("Pure", Position.none));
+Runtime.toplevel_program (fn () => Thy_Info.use_thy ("Pure", Position.none));
Context.set_thread_data NONE;
structure Pure = struct val thy = Thy_Info.get_theory "Pure" end;
@@ -355,7 +358,8 @@
(* ML toplevel commands *)
-fun use_thys args = Toplevel.program (fn () => Thy_Info.use_thys (map (rpair Position.none) args));
+fun use_thys args =
+ Runtime.toplevel_program (fn () => Thy_Info.use_thys (map (rpair Position.none) args));
val use_thy = use_thys o single;
val cd = File.cd o Path.explode;
--- a/src/Pure/Syntax/syntax_phases.ML Wed Mar 26 11:05:25 2014 -0700
+++ b/src/Pure/Syntax/syntax_phases.ML Thu Mar 27 21:38:45 2014 +0100
@@ -417,8 +417,9 @@
report_result ctxt pos []
[(reports', Exn.Exn (Exn.EXCEPTIONS (map ERROR ambig_msgs @ errs)))]
else if checked_len = 1 then
- (if not (null ambig_msgs) andalso ambiguity_warning then
- Context_Position.if_visible ctxt warning
+ (if not (null ambig_msgs) andalso ambiguity_warning andalso
+ Context_Position.is_visible ctxt then
+ warning
(cat_lines (ambig_msgs @
["Fortunately, only one parse tree is well-formed and type-correct,\n\
\but you may still want to disambiguate your grammar or your input."]))
@@ -927,7 +928,7 @@
fun check_typs ctxt raw_tys =
let
val (sorting_report, tys) = Proof_Context.prepare_sortsT ctxt raw_tys;
- val _ = Context_Position.if_visible ctxt Output.report sorting_report;
+ val _ = if Context_Position.is_visible ctxt then Output.report sorting_report else ();
in
tys
|> apply_typ_check ctxt
@@ -951,7 +952,9 @@
else I) ps tys' []
|> implode;
- val _ = Context_Position.if_visible ctxt Output.report (sorting_report ^ typing_report);
+ val _ =
+ if Context_Position.is_visible ctxt then Output.report (sorting_report ^ typing_report)
+ else ();
in Term_Sharing.terms (Proof_Context.theory_of ctxt) ts' end;
fun check_props ctxt = map (Type.constraint propT) #> check_terms ctxt;
--- a/src/Pure/System/command_line.ML Wed Mar 26 11:05:25 2014 -0700
+++ b/src/Pure/System/command_line.ML Thu Mar 27 21:38:45 2014 +0100
@@ -19,7 +19,7 @@
restore_attributes body () handle exn =>
let
val _ =
- ML_Compiler.exn_error_message exn
+ Runtime.exn_error_message exn
handle _ => Output.error_message "Exception raised, but failed to print details!";
in if Exn.is_interrupt exn then 130 else 1 end;
in if rc = 0 then () else exit rc end) ();
--- a/src/Pure/System/isabelle_process.ML Wed Mar 26 11:05:25 2014 -0700
+++ b/src/Pure/System/isabelle_process.ML Thu Mar 27 21:38:45 2014 +0100
@@ -48,9 +48,9 @@
(case Symtab.lookup (Synchronized.value commands) name of
NONE => error ("Undefined Isabelle protocol command " ^ quote name)
| SOME cmd =>
- (Toplevel.debugging NONE cmd args handle exn =>
+ (Runtime.debugging NONE cmd args handle exn =>
error ("Isabelle protocol command failure: " ^ quote name ^ "\n" ^
- ML_Compiler.exn_message exn)));
+ Runtime.exn_message exn)));
end;
@@ -170,7 +170,7 @@
[] => (Output.error_message "Isabelle process: no input"; true)
| name :: args => (task_context (fn () => run_command name args); true))
handle Runtime.TERMINATE => false
- | exn => (ML_Compiler.exn_error_message exn handle crash => recover crash; true);
+ | exn => (Runtime.exn_error_message exn handle crash => recover crash; true);
in
if continue then loop channel
else (Future.shutdown (); Execution.reset (); ())
--- a/src/Pure/System/isar.ML Wed Mar 26 11:05:25 2014 -0700
+++ b/src/Pure/System/isar.ML Thu Mar 27 21:38:45 2014 +0100
@@ -97,7 +97,7 @@
| SOME (_, SOME exn_info) =>
(set_exn (SOME exn_info);
Toplevel.setmp_thread_position tr
- ML_Compiler.exn_error_message (Runtime.EXCURSION_FAIL exn_info);
+ Runtime.exn_error_message (Runtime.EXCURSION_FAIL exn_info);
true)
| SOME (st', NONE) =>
let
@@ -144,7 +144,7 @@
NONE => if secure then quit () else ()
| SOME (tr, src') => if op >> tr orelse check_secure () then raw_loop secure src' else ())
handle exn =>
- (ML_Compiler.exn_error_message exn
+ (Runtime.exn_error_message exn
handle crash =>
(Synchronized.change crashes (cons crash);
warning "Recovering from Isar toplevel crash -- see also Isar.crashes");
--- a/src/Pure/Thy/thy_output.ML Wed Mar 26 11:05:25 2014 -0700
+++ b/src/Pure/Thy/thy_output.ML Thu Mar 27 21:38:45 2014 +0100
@@ -639,7 +639,7 @@
fun ml_text name ml = antiquotation name (Scan.lift Args.name_source_position)
(fn {context, ...} => fn source =>
- (ML_Context.eval_in (SOME context) {SML = false, verbose = false} (#pos source) (ml source);
+ (ML_Context.eval_in (SOME context) ML_Compiler.flags (#pos source) (ml source);
Symbol_Pos.source_content source
|> #1
|> (if Config.get context quotes then quote else I)
--- a/src/Pure/config.ML Wed Mar 26 11:05:25 2014 -0700
+++ b/src/Pure/config.ML Thu Mar 27 21:38:45 2014 +0100
@@ -131,8 +131,9 @@
print_value (get_value (Context.Theory (Context.theory_of context'))) <>
print_value (get_value context')
then
- (Context_Position.if_visible ctxt warning
- ("Ignoring local change of global option " ^ quote name); context)
+ (if Context_Position.is_visible ctxt then
+ warning ("Ignoring local change of global option " ^ quote name)
+ else (); context)
else context'
end
| map_value f context = update_value f context;
--- a/src/Pure/context_position.ML Wed Mar 26 11:05:25 2014 -0700
+++ b/src/Pure/context_position.ML Thu Mar 27 21:38:45 2014 +0100
@@ -9,8 +9,6 @@
val is_visible_generic: Context.generic -> bool
val is_visible: Proof.context -> bool
val is_visible_global: theory -> bool
- val if_visible: Proof.context -> ('a -> unit) -> 'a -> unit
- val if_visible_global: theory -> ('a -> unit) -> 'a -> unit
val set_visible: bool -> Proof.context -> Proof.context
val set_visible_global: bool -> theory -> theory
val restore_visible: Proof.context -> Proof.context -> Proof.context
@@ -40,9 +38,6 @@
val is_visible = is_visible_generic o Context.Proof;
val is_visible_global = is_visible_generic o Context.Theory;
-fun if_visible ctxt f x = if is_visible ctxt then f x else ();
-fun if_visible_global thy f x = if is_visible_global thy then f x else ();
-
val set_visible = Context.proof_map o Data.put o SOME;
val set_visible_global = Context.theory_map o Data.put o SOME;
--- a/src/Pure/pure_syn.ML Wed Mar 26 11:05:25 2014 -0700
+++ b/src/Pure/pure_syn.ML Thu Mar 27 21:38:45 2014 +0100
@@ -23,9 +23,10 @@
val [{src_path, lines, digest, pos}] = files (Context.theory_of gthy);
val provide = Resources.provide (src_path, digest);
val source = {delimited = true, text = cat_lines lines, pos = pos};
+ val flags = {SML = false, redirect = true, verbose = true};
in
gthy
- |> ML_Context.exec (fn () => ML_Context.eval_source {SML = false, verbose = true} source)
+ |> ML_Context.exec (fn () => ML_Context.eval_source flags source)
|> Local_Theory.propagate_ml_env
|> Context.mapping provide (Local_Theory.background_theory provide)
end)));
--- a/src/Pure/skip_proof.ML Wed Mar 26 11:05:25 2014 -0700
+++ b/src/Pure/skip_proof.ML Thu Mar 27 21:38:45 2014 +0100
@@ -18,8 +18,9 @@
(* report *)
fun report ctxt =
- Context_Position.if_visible ctxt Output.report
- (Markup.markup Markup.bad "Skipped proof");
+ if Context_Position.is_visible ctxt then
+ Output.report (Markup.markup Markup.bad "Skipped proof")
+ else ();
(* oracle setup *)
--- a/src/Pure/unify.ML Wed Mar 26 11:05:25 2014 -0700
+++ b/src/Pure/unify.ML Thu Mar 27 21:38:45 2014 +0100
@@ -607,8 +607,8 @@
[] => SOME (fold_rev (add_ffpair thy) flexflex (env', []), reseq)
| dp :: frigid' =>
if tdepth > search_bound then
- (Context_Position.if_visible_global thy warning "Unification bound exceeded";
- Seq.pull reseq)
+ (if Context_Position.is_visible_global thy
+ then warning "Unification bound exceeded" else (); Seq.pull reseq)
else
(if tdepth > trace_bound then
print_dpairs thy "Enter MATCH" (env',flexrigid@flexflex)
@@ -617,7 +617,8 @@
(add_unify (tdepth + 1)) (MATCH thy (env',dp, frigid'@flexflex), reseq))))
end
handle CANTUNIFY =>
- (if tdepth > trace_bound then Context_Position.if_visible_global thy tracing "Failure node"
+ (if tdepth > trace_bound andalso Context_Position.is_visible_global thy
+ then tracing "Failure node"
else (); Seq.pull reseq));
val dps = map (fn (t, u) => ([], t, u)) tus;
in add_unify 1 ((env, dps), Seq.empty) end;
--- a/src/Tools/WWW_Find/scgi_server.ML Wed Mar 26 11:05:25 2014 -0700
+++ b/src/Tools/WWW_Find/scgi_server.ML Thu Mar 27 21:38:45 2014 +0100
@@ -53,7 +53,7 @@
ConditionVar.wait (thread_wait, thread_wait_mutex));
add_thread
(Thread.fork (* FIXME avoid low-level Poly/ML thread primitives *)
- (fn () => ML_Compiler.exn_trace threadf,
+ (fn () => Runtime.exn_trace threadf,
[Thread.EnableBroadcastInterrupt true,
Thread.InterruptState
Thread.InterruptAsynchOnce])))
--- a/src/Tools/jEdit/src/isabelle_sidekick.scala Wed Mar 26 11:05:25 2014 -0700
+++ b/src/Tools/jEdit/src/isabelle_sidekick.scala Thu Mar 27 21:38:45 2014 +0100
@@ -160,8 +160,9 @@
val root = data.root
for ((command, command_start) <- snapshot.node.command_range() if !stopped) {
val markup =
- snapshot.state.command_state(snapshot.version, command).
- markup(Command.Markup_Index.markup)
+ snapshot.state.command_markup(
+ snapshot.version, command, Command.Markup_Index.markup,
+ command.range, Document.Elements.full)
Isabelle_Sidekick.swing_markup_tree(markup, root, (info: Text.Info[List[XML.Elem]]) =>
{
val range = info.range + command_start
--- a/src/Tools/jEdit/src/output_dockable.scala Wed Mar 26 11:05:25 2014 -0700
+++ b/src/Tools/jEdit/src/output_dockable.scala Thu Mar 27 21:38:45 2014 +0100
@@ -27,7 +27,8 @@
private var zoom_factor = 100
private var do_update = true
private var current_snapshot = Document.Snapshot.init
- private var current_state = Command.empty.init_state
+ private var current_command = Command.empty
+ private var current_results = Command.Results.empty
private var current_output: List[XML.Tree] = Nil
@@ -49,33 +50,34 @@
{
Swing_Thread.require()
- val (new_snapshot, new_state) =
+ val (new_snapshot, new_command, new_results) =
PIDE.editor.current_node_snapshot(view) match {
case Some(snapshot) =>
if (follow && !snapshot.is_outdated) {
PIDE.editor.current_command(view, snapshot) match {
case Some(cmd) =>
- (snapshot, snapshot.state.command_state(snapshot.version, cmd))
+ (snapshot, cmd, snapshot.state.command_results(snapshot.version, cmd))
case None =>
- (Document.Snapshot.init, Command.empty.init_state)
+ (Document.Snapshot.init, Command.empty, Command.Results.empty)
}
}
- else (current_snapshot, current_state)
- case None => (current_snapshot, current_state)
+ else (current_snapshot, current_command, current_results)
+ case None => (current_snapshot, current_command, current_results)
}
val new_output =
- if (!restriction.isDefined || restriction.get.contains(new_state.command)) {
+ if (!restriction.isDefined || restriction.get.contains(new_command)) {
val rendering = Rendering(new_snapshot, PIDE.options.value)
- rendering.output_messages(new_state)
+ rendering.output_messages(new_results)
}
else current_output
if (new_output != current_output)
- pretty_text_area.update(new_snapshot, new_state.results, Pretty.separate(new_output))
+ pretty_text_area.update(new_snapshot, new_results, Pretty.separate(new_output))
current_snapshot = new_snapshot
- current_state = new_state
+ current_command = new_command
+ current_results = new_results
current_output = new_output
}
@@ -149,8 +151,7 @@
tooltip = "Detach window with static copy of current output"
reactions += {
case ButtonClicked(_) =>
- Info_Dockable(view, current_snapshot,
- current_state.results, Pretty.separate(current_output))
+ Info_Dockable(view, current_snapshot, current_results, Pretty.separate(current_output))
}
}
--- a/src/Tools/jEdit/src/rendering.scala Wed Mar 26 11:05:25 2014 -0700
+++ b/src/Tools/jEdit/src/rendering.scala Thu Mar 27 21:38:45 2014 +0100
@@ -380,13 +380,13 @@
/* active elements */
def active(range: Text.Range): Option[Text.Info[XML.Elem]] =
- snapshot.select(range, Rendering.active_elements, command_state =>
+ snapshot.select(range, Rendering.active_elements, command_results =>
{
case Text.Info(info_range, elem) =>
if (elem.name == Markup.DIALOG) {
elem match {
case Protocol.Dialog(_, serial, _)
- if !command_state.results.defined(serial) =>
+ if !command_results.defined(serial) =>
Some(Text.Info(snapshot.convert(info_range), elem))
case _ => None
}
@@ -397,8 +397,8 @@
def command_results(range: Text.Range): Command.Results =
{
val results =
- snapshot.select[Command.Results](range, Document.Elements.full, command_state =>
- { case _ => Some(command_state.results) }).map(_.info)
+ snapshot.select[Command.Results](range, Document.Elements.full, command_results =>
+ { case _ => Some(command_results) }).map(_.info)
(Command.Results.empty /: results)(_ ++ _)
}
@@ -592,8 +592,8 @@
message_colors.get(pri).map((_, is_separator))
}
- def output_messages(st: Command.State): List[XML.Tree] =
- st.results.entries.map(_._2).filterNot(Protocol.is_result(_)).toList
+ def output_messages(results: Command.Results): List[XML.Tree] =
+ results.entries.map(_._2).filterNot(Protocol.is_result(_)).toList
/* text background */
@@ -606,7 +606,7 @@
Text.Info(r, result) <-
snapshot.cumulate[(Option[Protocol.Status], Option[Color])](
range, (Some(Protocol.Status.init), None), Rendering.background_elements,
- command_state =>
+ command_results =>
{
case (((Some(status), color), Text.Info(_, XML.Elem(markup, _))))
if (Protocol.command_status_elements(markup.name)) =>
@@ -616,7 +616,7 @@
case (_, Text.Info(_, XML.Elem(Markup(Markup.INTENSIFY, _), _))) =>
Some((None, Some(intensify_color)))
case (acc, Text.Info(_, Protocol.Dialog(_, serial, result))) =>
- command_state.results.get(serial) match {
+ command_results.get(serial) match {
case Some(Protocol.Dialog_Result(res)) if res == result =>
Some((None, Some(active_result_color)))
case _ =>
--- a/src/Tools/jEdit/src/simplifier_trace_dockable.scala Wed Mar 26 11:05:25 2014 -0700
+++ b/src/Tools/jEdit/src/simplifier_trace_dockable.scala Thu Mar 27 21:38:45 2014 +0100
@@ -26,7 +26,8 @@
/* component state -- owned by Swing thread */
private var current_snapshot = Document.State.init.snapshot()
- private var current_state = Command.empty.init_state
+ private var current_command = Command.empty
+ private var current_results = Command.Results.empty
private var current_id = 0L
private var do_update = true
private var do_auto_reply = false
@@ -77,7 +78,7 @@
private def show_trace()
{
- val trace = Simplifier_Trace.generate_trace(current_state.results)
+ val trace = Simplifier_Trace.generate_trace(current_results)
new Simplifier_Trace_Window(view, current_snapshot, trace)
}
@@ -92,7 +93,7 @@
{
set_context(
current_snapshot,
- Simplifier_Trace.handle_results(PIDE.session, current_id, current_state.results)
+ Simplifier_Trace.handle_results(PIDE.session, current_id, current_results)
)
}
@@ -103,23 +104,24 @@
private def handle_update(follow: Boolean)
{
- val (new_snapshot, new_state, new_id) =
+ val (new_snapshot, new_command, new_results, new_id) =
PIDE.editor.current_node_snapshot(view) match {
case Some(snapshot) =>
if (follow && !snapshot.is_outdated) {
PIDE.editor.current_command(view, snapshot) match {
case Some(cmd) =>
- (snapshot, snapshot.state.command_state(snapshot.version, cmd), cmd.id)
+ (snapshot, cmd, snapshot.state.command_results(snapshot.version, cmd), cmd.id)
case None =>
- (Document.State.init.snapshot(), Command.empty.init_state, 0L)
+ (Document.State.init.snapshot(), Command.empty, Command.Results.empty, 0L)
}
}
- else (current_snapshot, current_state, current_id)
- case None => (current_snapshot, current_state, current_id)
+ else (current_snapshot, current_command, current_results, current_id)
+ case None => (current_snapshot, current_command, current_results, current_id)
}
current_snapshot = new_snapshot
- current_state = new_state
+ current_command = new_command
+ current_results = new_results
current_id = new_id
update_contents()
}