--- a/src/Pure/PIDE/command.ML Thu Jul 11 23:24:40 2013 +0200
+++ b/src/Pure/PIDE/command.ML Fri Jul 12 11:07:02 2013 +0200
@@ -20,7 +20,7 @@
type exec = eval * print list
val no_exec: exec
val exec_ids: exec option -> Document_ID.exec list
- val exec: Exec.context -> exec -> unit
+ val exec: Execution.context -> exec -> unit
end;
structure Command: COMMAND =
@@ -51,10 +51,10 @@
(fn Result res => SOME (res, Result res)
| expr as Expr (exec_id, e) =>
uninterruptible (fn restore_attributes => fn () =>
- if Exec.running context exec_id then
+ if Execution.running context exec_id then
let
val res = Exn.capture (restore_attributes e) ();
- val _ = Exec.finished exec_id (not (Exn.is_interrupt_exn res));
+ val _ = Execution.finished exec_id (not (Exn.is_interrupt_exn res));
in SOME (res, Result res) end
else SOME (Exn.interrupt_exn, expr)) ())
|> (fn NONE => error "Concurrent execution attempt" | SOME res => res))
@@ -113,7 +113,7 @@
val eval_result_state = #state o eval_result;
fun eval_same (Eval {exec_id, ...}, Eval {exec_id = exec_id', ...}) =
- exec_id = exec_id' andalso Exec.is_stable exec_id;
+ exec_id = exec_id' andalso Execution.is_stable exec_id;
local
@@ -198,7 +198,7 @@
List.app (Future.error_msg (Toplevel.pos_of tr)) (ML_Compiler.exn_messages_ids exn);
fun print_persistent (Print {persistent, ...}) = persistent;
-fun print_stable (Print {exec_id, ...}) = Exec.is_stable exec_id;
+fun print_stable (Print {exec_id, ...}) = Execution.is_stable exec_id;
fun print_eq (Print {exec_id, ...}, Print {exec_id = exec_id', ...}) = exec_id = exec_id';
in
--- a/src/Pure/PIDE/document.ML Thu Jul 11 23:24:40 2013 +0200
+++ b/src/Pure/PIDE/document.ML Fri Jul 12 11:07:02 2013 +0200
@@ -205,10 +205,10 @@
(** main state -- document structure and execution process **)
-type execution = {version_id: Document_ID.version, context: Exec.context};
+type execution = {version_id: Document_ID.version, context: Execution.context};
-val no_execution = {version_id = Document_ID.none, context = Exec.no_context};
-fun make_execution version_id = {version_id = version_id, context = Exec.fresh_context ()};
+val no_execution = {version_id = Document_ID.none, context = Execution.no_context};
+fun make_execution version_id = {version_id = version_id, context = Execution.fresh_context ()};
abstype state = State of
{versions: version Inttab.table, (*version id -> document content*)
@@ -297,16 +297,16 @@
(* document execution *)
fun discontinue_execution state =
- Exec.drop_context (#context (execution_of state));
+ Execution.drop_context (#context (execution_of state));
fun cancel_execution state =
- (Exec.drop_context (#context (execution_of state)); Exec.terminate_all ());
+ (Execution.drop_context (#context (execution_of state)); Execution.terminate_all ());
fun start_execution state =
let
val {version_id, context} = execution_of state;
val _ =
- if Exec.is_running context then
+ if Execution.is_running context then
nodes_of (the_version state version_id) |> String_Graph.schedule
(fn deps => fn (name, node) =>
if not (visible_node node) andalso finished_theory node then
@@ -319,7 +319,7 @@
iterate_entries (fn (_, opt_exec) => fn () =>
(case opt_exec of
SOME exec =>
- if Exec.is_running context then SOME (Command.exec context exec)
+ if Execution.is_running context then SOME (Command.exec context exec)
else NONE
| NONE => NONE)) node ()))
else [];
@@ -452,7 +452,7 @@
fun cancel_old_execs node0 (command_id, exec_ids) =
subtract (op =) exec_ids (Command.exec_ids (lookup_entry node0 command_id))
- |> map_filter (Exec.peek_running #> Option.map (tap Future.cancel_group));
+ |> map_filter (Execution.peek_running #> Option.map (tap Future.cancel_group));
in
--- a/src/Pure/PIDE/exec.ML Thu Jul 11 23:24:40 2013 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,100 +0,0 @@
-(* Title: Pure/PIDE/exec.ML
- Author: Makarius
-
-Global management of command execution fragments.
-*)
-
-signature EXEC =
-sig
- type context
- val no_context: context
- val drop_context: context -> unit
- val fresh_context: unit -> context
- val is_running: context -> bool
- val running: context -> Document_ID.exec -> bool
- val finished: Document_ID.exec -> bool -> unit
- val is_stable: Document_ID.exec -> bool
- val peek_running: Document_ID.exec -> Future.group option
- val purge_canceled: unit -> unit
- val terminate_all: unit -> unit
-end;
-
-structure Exec: EXEC =
-struct
-
-(* global state *)
-
-datatype context = Context of Document_ID.generic;
-val no_context = Context Document_ID.none;
-
-type status = Future.group option; (*SOME group: running, NONE: canceled*)
-val state = Synchronized.var "Exec.state" (no_context, Inttab.empty: status Inttab.table);
-
-
-(* unique execution context *)
-
-fun drop_context context =
- Synchronized.change state
- (apfst (fn context' => if context = context' then no_context else context'));
-
-fun fresh_context () =
- let
- val context = Context (Document_ID.make ());
- val _ = Synchronized.change state (apfst (K context));
- in context end;
-
-fun is_running context = context = fst (Synchronized.value state);
-
-
-(* registered execs *)
-
-fun running context exec_id =
- Synchronized.guarded_access state
- (fn (current_context, execs) =>
- let
- val cont = context = current_context;
- val execs' =
- if cont then
- Inttab.update_new (exec_id, SOME (Future.the_worker_group ())) execs
- handle Inttab.DUP dup => error ("Duplicate execution " ^ Document_ID.print dup)
- else execs;
- in SOME (cont, (current_context, execs')) end);
-
-fun finished exec_id stable =
- Synchronized.change state
- (apsnd (fn execs =>
- if not (Inttab.defined execs exec_id) then
- error ("Attempt to finish unknown execution: " ^ Document_ID.print exec_id)
- else if stable then Inttab.delete exec_id execs
- else Inttab.update (exec_id, NONE) execs));
-
-fun is_stable exec_id =
- not (Par_Exn.is_interrupted (Future.join_results (Goal.peek_futures exec_id))) andalso
- (case Inttab.lookup (snd (Synchronized.value state)) exec_id of
- NONE => true
- | SOME status => is_some status);
-
-fun peek_running exec_id =
- (case Inttab.lookup (snd (Synchronized.value state)) exec_id of
- SOME (SOME group) => SOME group
- | _ => NONE);
-
-fun purge_canceled () =
- Synchronized.guarded_access state
- (fn (context, execs) =>
- let
- val canceled = Inttab.fold (fn (exec_id, NONE) => cons exec_id | _ => I) execs [];
- val execs' = fold Inttab.delete canceled execs;
- in SOME ((), (context, execs')) end);
-
-fun terminate_all () =
- let
- val groups =
- Inttab.fold (fn (_, SOME group) => cons group | _ => I)
- (snd (Synchronized.value state)) [];
- val _ = List.app Future.cancel_group groups;
- val _ = List.app Future.terminate groups;
- in () end;
-
-end;
-
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/PIDE/execution.ML Fri Jul 12 11:07:02 2013 +0200
@@ -0,0 +1,100 @@
+(* Title: Pure/PIDE/execution.ML
+ Author: Makarius
+
+Global management of command execution fragments.
+*)
+
+signature EXECUTION =
+sig
+ type context
+ val no_context: context
+ val drop_context: context -> unit
+ val fresh_context: unit -> context
+ val is_running: context -> bool
+ val running: context -> Document_ID.exec -> bool
+ val finished: Document_ID.exec -> bool -> unit
+ val is_stable: Document_ID.exec -> bool
+ val peek_running: Document_ID.exec -> Future.group option
+ val purge_canceled: unit -> unit
+ val terminate_all: unit -> unit
+end;
+
+structure Execution: EXECUTION =
+struct
+
+(* global state *)
+
+datatype context = Context of Document_ID.generic;
+val no_context = Context Document_ID.none;
+
+type status = Future.group option; (*SOME group: running, NONE: canceled*)
+val state = Synchronized.var "Execution.state" (no_context, Inttab.empty: status Inttab.table);
+
+
+(* unique execution context *)
+
+fun drop_context context =
+ Synchronized.change state
+ (apfst (fn context' => if context = context' then no_context else context'));
+
+fun fresh_context () =
+ let
+ val context = Context (Document_ID.make ());
+ val _ = Synchronized.change state (apfst (K context));
+ in context end;
+
+fun is_running context = context = fst (Synchronized.value state);
+
+
+(* registered execs *)
+
+fun running context exec_id =
+ Synchronized.guarded_access state
+ (fn (current_context, execs) =>
+ let
+ val cont = context = current_context;
+ val execs' =
+ if cont then
+ Inttab.update_new (exec_id, SOME (Future.the_worker_group ())) execs
+ handle Inttab.DUP dup => error ("Duplicate execution " ^ Document_ID.print dup)
+ else execs;
+ in SOME (cont, (current_context, execs')) end);
+
+fun finished exec_id stable =
+ Synchronized.change state
+ (apsnd (fn execs =>
+ if not (Inttab.defined execs exec_id) then
+ error ("Attempt to finish unknown execution: " ^ Document_ID.print exec_id)
+ else if stable then Inttab.delete exec_id execs
+ else Inttab.update (exec_id, NONE) execs));
+
+fun is_stable exec_id =
+ not (Par_Exn.is_interrupted (Future.join_results (Goal.peek_futures exec_id))) andalso
+ (case Inttab.lookup (snd (Synchronized.value state)) exec_id of
+ NONE => true
+ | SOME status => is_some status);
+
+fun peek_running exec_id =
+ (case Inttab.lookup (snd (Synchronized.value state)) exec_id of
+ SOME (SOME group) => SOME group
+ | _ => NONE);
+
+fun purge_canceled () =
+ Synchronized.guarded_access state
+ (fn (context, execs) =>
+ let
+ val canceled = Inttab.fold (fn (exec_id, NONE) => cons exec_id | _ => I) execs [];
+ val execs' = fold Inttab.delete canceled execs;
+ in SOME ((), (context, execs')) end);
+
+fun terminate_all () =
+ let
+ val groups =
+ Inttab.fold (fn (_, SOME group) => cons group | _ => I)
+ (snd (Synchronized.value state)) [];
+ val _ = List.app Future.cancel_group groups;
+ val _ = List.app Future.terminate groups;
+ in () end;
+
+end;
+
--- a/src/Pure/PIDE/protocol.ML Thu Jul 11 23:24:40 2013 +0200
+++ b/src/Pure/PIDE/protocol.ML Fri Jul 12 11:07:02 2013 +0200
@@ -54,7 +54,7 @@
val (assign_update, state') = Document.update old_id new_id edits state;
val _ = List.app Future.cancel_group (Goal.reset_futures ());
- val _ = Exec.purge_canceled ();
+ val _ = Execution.purge_canceled ();
val _ = Isabelle_Process.reset_tracing ();
val _ =
--- a/src/Pure/ROOT Thu Jul 11 23:24:40 2013 +0200
+++ b/src/Pure/ROOT Fri Jul 12 11:07:02 2013 +0200
@@ -150,10 +150,10 @@
"ML/ml_syntax.ML"
"ML/ml_thms.ML"
"PIDE/active.ML"
- "PIDE/exec.ML"
"PIDE/command.ML"
"PIDE/document.ML"
"PIDE/document_id.ML"
+ "PIDE/execution.ML"
"PIDE/markup.ML"
"PIDE/protocol.ML"
"PIDE/xml.ML"
--- a/src/Pure/ROOT.ML Thu Jul 11 23:24:40 2013 +0200
+++ b/src/Pure/ROOT.ML Fri Jul 12 11:07:02 2013 +0200
@@ -267,7 +267,7 @@
use "Isar/outer_syntax.ML";
use "General/graph_display.ML";
use "Thy/present.ML";
-use "PIDE/exec.ML";
+use "PIDE/execution.ML";
use "PIDE/command.ML";
use "Thy/thy_load.ML";
use "Thy/thy_info.ML";