1.1 --- a/src/Pure/PIDE/command.ML Thu Jul 11 23:24:40 2013 +0200
1.2 +++ b/src/Pure/PIDE/command.ML Fri Jul 12 11:07:02 2013 +0200
1.3 @@ -20,7 +20,7 @@
1.4 type exec = eval * print list
1.5 val no_exec: exec
1.6 val exec_ids: exec option -> Document_ID.exec list
1.7 - val exec: Exec.context -> exec -> unit
1.8 + val exec: Execution.context -> exec -> unit
1.9 end;
1.10
1.11 structure Command: COMMAND =
1.12 @@ -51,10 +51,10 @@
1.13 (fn Result res => SOME (res, Result res)
1.14 | expr as Expr (exec_id, e) =>
1.15 uninterruptible (fn restore_attributes => fn () =>
1.16 - if Exec.running context exec_id then
1.17 + if Execution.running context exec_id then
1.18 let
1.19 val res = Exn.capture (restore_attributes e) ();
1.20 - val _ = Exec.finished exec_id (not (Exn.is_interrupt_exn res));
1.21 + val _ = Execution.finished exec_id (not (Exn.is_interrupt_exn res));
1.22 in SOME (res, Result res) end
1.23 else SOME (Exn.interrupt_exn, expr)) ())
1.24 |> (fn NONE => error "Concurrent execution attempt" | SOME res => res))
1.25 @@ -113,7 +113,7 @@
1.26 val eval_result_state = #state o eval_result;
1.27
1.28 fun eval_same (Eval {exec_id, ...}, Eval {exec_id = exec_id', ...}) =
1.29 - exec_id = exec_id' andalso Exec.is_stable exec_id;
1.30 + exec_id = exec_id' andalso Execution.is_stable exec_id;
1.31
1.32 local
1.33
1.34 @@ -198,7 +198,7 @@
1.35 List.app (Future.error_msg (Toplevel.pos_of tr)) (ML_Compiler.exn_messages_ids exn);
1.36
1.37 fun print_persistent (Print {persistent, ...}) = persistent;
1.38 -fun print_stable (Print {exec_id, ...}) = Exec.is_stable exec_id;
1.39 +fun print_stable (Print {exec_id, ...}) = Execution.is_stable exec_id;
1.40 fun print_eq (Print {exec_id, ...}, Print {exec_id = exec_id', ...}) = exec_id = exec_id';
1.41
1.42 in
2.1 --- a/src/Pure/PIDE/document.ML Thu Jul 11 23:24:40 2013 +0200
2.2 +++ b/src/Pure/PIDE/document.ML Fri Jul 12 11:07:02 2013 +0200
2.3 @@ -205,10 +205,10 @@
2.4
2.5 (** main state -- document structure and execution process **)
2.6
2.7 -type execution = {version_id: Document_ID.version, context: Exec.context};
2.8 +type execution = {version_id: Document_ID.version, context: Execution.context};
2.9
2.10 -val no_execution = {version_id = Document_ID.none, context = Exec.no_context};
2.11 -fun make_execution version_id = {version_id = version_id, context = Exec.fresh_context ()};
2.12 +val no_execution = {version_id = Document_ID.none, context = Execution.no_context};
2.13 +fun make_execution version_id = {version_id = version_id, context = Execution.fresh_context ()};
2.14
2.15 abstype state = State of
2.16 {versions: version Inttab.table, (*version id -> document content*)
2.17 @@ -297,16 +297,16 @@
2.18 (* document execution *)
2.19
2.20 fun discontinue_execution state =
2.21 - Exec.drop_context (#context (execution_of state));
2.22 + Execution.drop_context (#context (execution_of state));
2.23
2.24 fun cancel_execution state =
2.25 - (Exec.drop_context (#context (execution_of state)); Exec.terminate_all ());
2.26 + (Execution.drop_context (#context (execution_of state)); Execution.terminate_all ());
2.27
2.28 fun start_execution state =
2.29 let
2.30 val {version_id, context} = execution_of state;
2.31 val _ =
2.32 - if Exec.is_running context then
2.33 + if Execution.is_running context then
2.34 nodes_of (the_version state version_id) |> String_Graph.schedule
2.35 (fn deps => fn (name, node) =>
2.36 if not (visible_node node) andalso finished_theory node then
2.37 @@ -319,7 +319,7 @@
2.38 iterate_entries (fn (_, opt_exec) => fn () =>
2.39 (case opt_exec of
2.40 SOME exec =>
2.41 - if Exec.is_running context then SOME (Command.exec context exec)
2.42 + if Execution.is_running context then SOME (Command.exec context exec)
2.43 else NONE
2.44 | NONE => NONE)) node ()))
2.45 else [];
2.46 @@ -452,7 +452,7 @@
2.47
2.48 fun cancel_old_execs node0 (command_id, exec_ids) =
2.49 subtract (op =) exec_ids (Command.exec_ids (lookup_entry node0 command_id))
2.50 - |> map_filter (Exec.peek_running #> Option.map (tap Future.cancel_group));
2.51 + |> map_filter (Execution.peek_running #> Option.map (tap Future.cancel_group));
2.52
2.53 in
2.54
3.1 --- a/src/Pure/PIDE/exec.ML Thu Jul 11 23:24:40 2013 +0200
3.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
3.3 @@ -1,100 +0,0 @@
3.4 -(* Title: Pure/PIDE/exec.ML
3.5 - Author: Makarius
3.6 -
3.7 -Global management of command execution fragments.
3.8 -*)
3.9 -
3.10 -signature EXEC =
3.11 -sig
3.12 - type context
3.13 - val no_context: context
3.14 - val drop_context: context -> unit
3.15 - val fresh_context: unit -> context
3.16 - val is_running: context -> bool
3.17 - val running: context -> Document_ID.exec -> bool
3.18 - val finished: Document_ID.exec -> bool -> unit
3.19 - val is_stable: Document_ID.exec -> bool
3.20 - val peek_running: Document_ID.exec -> Future.group option
3.21 - val purge_canceled: unit -> unit
3.22 - val terminate_all: unit -> unit
3.23 -end;
3.24 -
3.25 -structure Exec: EXEC =
3.26 -struct
3.27 -
3.28 -(* global state *)
3.29 -
3.30 -datatype context = Context of Document_ID.generic;
3.31 -val no_context = Context Document_ID.none;
3.32 -
3.33 -type status = Future.group option; (*SOME group: running, NONE: canceled*)
3.34 -val state = Synchronized.var "Exec.state" (no_context, Inttab.empty: status Inttab.table);
3.35 -
3.36 -
3.37 -(* unique execution context *)
3.38 -
3.39 -fun drop_context context =
3.40 - Synchronized.change state
3.41 - (apfst (fn context' => if context = context' then no_context else context'));
3.42 -
3.43 -fun fresh_context () =
3.44 - let
3.45 - val context = Context (Document_ID.make ());
3.46 - val _ = Synchronized.change state (apfst (K context));
3.47 - in context end;
3.48 -
3.49 -fun is_running context = context = fst (Synchronized.value state);
3.50 -
3.51 -
3.52 -(* registered execs *)
3.53 -
3.54 -fun running context exec_id =
3.55 - Synchronized.guarded_access state
3.56 - (fn (current_context, execs) =>
3.57 - let
3.58 - val cont = context = current_context;
3.59 - val execs' =
3.60 - if cont then
3.61 - Inttab.update_new (exec_id, SOME (Future.the_worker_group ())) execs
3.62 - handle Inttab.DUP dup => error ("Duplicate execution " ^ Document_ID.print dup)
3.63 - else execs;
3.64 - in SOME (cont, (current_context, execs')) end);
3.65 -
3.66 -fun finished exec_id stable =
3.67 - Synchronized.change state
3.68 - (apsnd (fn execs =>
3.69 - if not (Inttab.defined execs exec_id) then
3.70 - error ("Attempt to finish unknown execution: " ^ Document_ID.print exec_id)
3.71 - else if stable then Inttab.delete exec_id execs
3.72 - else Inttab.update (exec_id, NONE) execs));
3.73 -
3.74 -fun is_stable exec_id =
3.75 - not (Par_Exn.is_interrupted (Future.join_results (Goal.peek_futures exec_id))) andalso
3.76 - (case Inttab.lookup (snd (Synchronized.value state)) exec_id of
3.77 - NONE => true
3.78 - | SOME status => is_some status);
3.79 -
3.80 -fun peek_running exec_id =
3.81 - (case Inttab.lookup (snd (Synchronized.value state)) exec_id of
3.82 - SOME (SOME group) => SOME group
3.83 - | _ => NONE);
3.84 -
3.85 -fun purge_canceled () =
3.86 - Synchronized.guarded_access state
3.87 - (fn (context, execs) =>
3.88 - let
3.89 - val canceled = Inttab.fold (fn (exec_id, NONE) => cons exec_id | _ => I) execs [];
3.90 - val execs' = fold Inttab.delete canceled execs;
3.91 - in SOME ((), (context, execs')) end);
3.92 -
3.93 -fun terminate_all () =
3.94 - let
3.95 - val groups =
3.96 - Inttab.fold (fn (_, SOME group) => cons group | _ => I)
3.97 - (snd (Synchronized.value state)) [];
3.98 - val _ = List.app Future.cancel_group groups;
3.99 - val _ = List.app Future.terminate groups;
3.100 - in () end;
3.101 -
3.102 -end;
3.103 -
4.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
4.2 +++ b/src/Pure/PIDE/execution.ML Fri Jul 12 11:07:02 2013 +0200
4.3 @@ -0,0 +1,100 @@
4.4 +(* Title: Pure/PIDE/execution.ML
4.5 + Author: Makarius
4.6 +
4.7 +Global management of command execution fragments.
4.8 +*)
4.9 +
4.10 +signature EXECUTION =
4.11 +sig
4.12 + type context
4.13 + val no_context: context
4.14 + val drop_context: context -> unit
4.15 + val fresh_context: unit -> context
4.16 + val is_running: context -> bool
4.17 + val running: context -> Document_ID.exec -> bool
4.18 + val finished: Document_ID.exec -> bool -> unit
4.19 + val is_stable: Document_ID.exec -> bool
4.20 + val peek_running: Document_ID.exec -> Future.group option
4.21 + val purge_canceled: unit -> unit
4.22 + val terminate_all: unit -> unit
4.23 +end;
4.24 +
4.25 +structure Execution: EXECUTION =
4.26 +struct
4.27 +
4.28 +(* global state *)
4.29 +
4.30 +datatype context = Context of Document_ID.generic;
4.31 +val no_context = Context Document_ID.none;
4.32 +
4.33 +type status = Future.group option; (*SOME group: running, NONE: canceled*)
4.34 +val state = Synchronized.var "Execution.state" (no_context, Inttab.empty: status Inttab.table);
4.35 +
4.36 +
4.37 +(* unique execution context *)
4.38 +
4.39 +fun drop_context context =
4.40 + Synchronized.change state
4.41 + (apfst (fn context' => if context = context' then no_context else context'));
4.42 +
4.43 +fun fresh_context () =
4.44 + let
4.45 + val context = Context (Document_ID.make ());
4.46 + val _ = Synchronized.change state (apfst (K context));
4.47 + in context end;
4.48 +
4.49 +fun is_running context = context = fst (Synchronized.value state);
4.50 +
4.51 +
4.52 +(* registered execs *)
4.53 +
4.54 +fun running context exec_id =
4.55 + Synchronized.guarded_access state
4.56 + (fn (current_context, execs) =>
4.57 + let
4.58 + val cont = context = current_context;
4.59 + val execs' =
4.60 + if cont then
4.61 + Inttab.update_new (exec_id, SOME (Future.the_worker_group ())) execs
4.62 + handle Inttab.DUP dup => error ("Duplicate execution " ^ Document_ID.print dup)
4.63 + else execs;
4.64 + in SOME (cont, (current_context, execs')) end);
4.65 +
4.66 +fun finished exec_id stable =
4.67 + Synchronized.change state
4.68 + (apsnd (fn execs =>
4.69 + if not (Inttab.defined execs exec_id) then
4.70 + error ("Attempt to finish unknown execution: " ^ Document_ID.print exec_id)
4.71 + else if stable then Inttab.delete exec_id execs
4.72 + else Inttab.update (exec_id, NONE) execs));
4.73 +
4.74 +fun is_stable exec_id =
4.75 + not (Par_Exn.is_interrupted (Future.join_results (Goal.peek_futures exec_id))) andalso
4.76 + (case Inttab.lookup (snd (Synchronized.value state)) exec_id of
4.77 + NONE => true
4.78 + | SOME status => is_some status);
4.79 +
4.80 +fun peek_running exec_id =
4.81 + (case Inttab.lookup (snd (Synchronized.value state)) exec_id of
4.82 + SOME (SOME group) => SOME group
4.83 + | _ => NONE);
4.84 +
4.85 +fun purge_canceled () =
4.86 + Synchronized.guarded_access state
4.87 + (fn (context, execs) =>
4.88 + let
4.89 + val canceled = Inttab.fold (fn (exec_id, NONE) => cons exec_id | _ => I) execs [];
4.90 + val execs' = fold Inttab.delete canceled execs;
4.91 + in SOME ((), (context, execs')) end);
4.92 +
4.93 +fun terminate_all () =
4.94 + let
4.95 + val groups =
4.96 + Inttab.fold (fn (_, SOME group) => cons group | _ => I)
4.97 + (snd (Synchronized.value state)) [];
4.98 + val _ = List.app Future.cancel_group groups;
4.99 + val _ = List.app Future.terminate groups;
4.100 + in () end;
4.101 +
4.102 +end;
4.103 +
5.1 --- a/src/Pure/PIDE/protocol.ML Thu Jul 11 23:24:40 2013 +0200
5.2 +++ b/src/Pure/PIDE/protocol.ML Fri Jul 12 11:07:02 2013 +0200
5.3 @@ -54,7 +54,7 @@
5.4 val (assign_update, state') = Document.update old_id new_id edits state;
5.5
5.6 val _ = List.app Future.cancel_group (Goal.reset_futures ());
5.7 - val _ = Exec.purge_canceled ();
5.8 + val _ = Execution.purge_canceled ();
5.9 val _ = Isabelle_Process.reset_tracing ();
5.10
5.11 val _ =
6.1 --- a/src/Pure/ROOT Thu Jul 11 23:24:40 2013 +0200
6.2 +++ b/src/Pure/ROOT Fri Jul 12 11:07:02 2013 +0200
6.3 @@ -150,10 +150,10 @@
6.4 "ML/ml_syntax.ML"
6.5 "ML/ml_thms.ML"
6.6 "PIDE/active.ML"
6.7 - "PIDE/exec.ML"
6.8 "PIDE/command.ML"
6.9 "PIDE/document.ML"
6.10 "PIDE/document_id.ML"
6.11 + "PIDE/execution.ML"
6.12 "PIDE/markup.ML"
6.13 "PIDE/protocol.ML"
6.14 "PIDE/xml.ML"
7.1 --- a/src/Pure/ROOT.ML Thu Jul 11 23:24:40 2013 +0200
7.2 +++ b/src/Pure/ROOT.ML Fri Jul 12 11:07:02 2013 +0200
7.3 @@ -267,7 +267,7 @@
7.4 use "Isar/outer_syntax.ML";
7.5 use "General/graph_display.ML";
7.6 use "Thy/present.ML";
7.7 -use "PIDE/exec.ML";
7.8 +use "PIDE/execution.ML";
7.9 use "PIDE/command.ML";
7.10 use "Thy/thy_load.ML";
7.11 use "Thy/thy_info.ML";