# HG changeset patch # User wenzelm # Date 1373620022 -7200 # Node ID a2a805549c7408900aa29f4263e338f6894280e2 # Parent ff2f0818aebcbfa7eb7f20a15953aa44491b3542 clarified module name; diff -r ff2f0818aebc -r a2a805549c74 src/Pure/PIDE/command.ML --- 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 diff -r ff2f0818aebc -r a2a805549c74 src/Pure/PIDE/document.ML --- 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 diff -r ff2f0818aebc -r a2a805549c74 src/Pure/PIDE/exec.ML --- 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; - diff -r ff2f0818aebc -r a2a805549c74 src/Pure/PIDE/execution.ML --- /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; + diff -r ff2f0818aebc -r a2a805549c74 src/Pure/PIDE/protocol.ML --- 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 _ = diff -r ff2f0818aebc -r a2a805549c74 src/Pure/ROOT --- 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" diff -r ff2f0818aebc -r a2a805549c74 src/Pure/ROOT.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";