1.1 --- a/src/Pure/PIDE/command.ML	Fri Jul 12 11:07:02 2013 +0200
     1.2 +++ b/src/Pure/PIDE/command.ML	Fri Jul 12 11:28:03 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: Execution.context -> exec -> unit
     1.8 +  val exec: Document_ID.execution -> exec -> unit
     1.9  end;
    1.10  
    1.11  structure Command: COMMAND =

     2.1 --- a/src/Pure/PIDE/document.ML	Fri Jul 12 11:07:02 2013 +0200
     2.2 +++ b/src/Pure/PIDE/document.ML	Fri Jul 12 11:28:03 2013 +0200
     2.3 @@ -18,8 +18,6 @@
     2.4    val init_state: state
     2.5    val define_command: Document_ID.command -> string -> string -> state -> state
     2.6    val remove_versions: Document_ID.version list -> state -> state
     2.7 -  val discontinue_execution: state -> unit
     2.8 -  val cancel_execution: state -> unit
     2.9    val start_execution: state -> unit
    2.10    val timing: bool Unsynchronized.ref
    2.11    val update: Document_ID.version -> Document_ID.version -> edit list -> state ->
    2.12 @@ -205,10 +203,10 @@
    2.13  
    2.14  (** main state -- document structure and execution process **)
    2.15  
    2.16 -type execution = {version_id: Document_ID.version, context: Execution.context};
    2.17 +type execution = {version_id: Document_ID.version, execution_id: Document_ID.execution};
    2.18  
    2.19 -val no_execution = {version_id = Document_ID.none, context = Execution.no_context};
    2.20 -fun make_execution version_id = {version_id = version_id, context = Execution.fresh_context ()};
    2.21 +val no_execution = {version_id = Document_ID.none, execution_id = Document_ID.none};
    2.22 +fun next_execution version_id = {version_id = version_id, execution_id = Execution.start ()};
    2.23  
    2.24  abstype state = State of
    2.25   {versions: version Inttab.table,  (*version id -> document content*)
    2.26 @@ -235,7 +233,7 @@
    2.27      let
    2.28        val versions' = Inttab.update_new (version_id, version) versions
    2.29          handle Inttab.DUP dup => err_dup "document version" dup;
    2.30 -      val execution' = make_execution version_id;
    2.31 +      val execution' = next_execution version_id;
    2.32      in (versions', commands, execution') end);
    2.33  
    2.34  fun the_version (State {versions, ...}) version_id =
    2.35 @@ -296,17 +294,11 @@
    2.36  
    2.37  (* document execution *)
    2.38  
    2.39 -fun discontinue_execution state =
    2.40 -  Execution.drop_context (#context (execution_of state));
    2.41 -
    2.42 -fun cancel_execution state =
    2.43 -  (Execution.drop_context (#context (execution_of state)); Execution.terminate_all ());
    2.44 -
    2.45  fun start_execution state =
    2.46    let
    2.47 -    val {version_id, context} = execution_of state;
    2.48 +    val {version_id, execution_id} = execution_of state;
    2.49      val _ =
    2.50 -      if Execution.is_running context then
    2.51 +      if Execution.is_running execution_id then
    2.52          nodes_of (the_version state version_id) |> String_Graph.schedule
    2.53            (fn deps => fn (name, node) =>
    2.54              if not (visible_node node) andalso finished_theory node then
    2.55 @@ -319,7 +311,8 @@
    2.56                    iterate_entries (fn (_, opt_exec) => fn () =>
    2.57                      (case opt_exec of
    2.58                        SOME exec =>
    2.59 -                        if Execution.is_running context then SOME (Command.exec context exec)
    2.60 +                        if Execution.is_running execution_id
    2.61 +                        then SOME (Command.exec execution_id exec)
    2.62                          else NONE
    2.63                      | NONE => NONE)) node ()))
    2.64        else [];

     3.1 --- a/src/Pure/PIDE/document_id.ML	Fri Jul 12 11:07:02 2013 +0200
     3.2 +++ b/src/Pure/PIDE/document_id.ML	Fri Jul 12 11:28:03 2013 +0200
     3.3 @@ -12,6 +12,7 @@
     3.4    type version = generic
     3.5    type command = generic
     3.6    type exec = generic
     3.7 +  type execution = generic
     3.8    val none: generic
     3.9    val make: unit -> generic
    3.10    val parse: string -> generic
    3.11 @@ -25,6 +26,7 @@
    3.12  type version = generic;
    3.13  type command = generic;
    3.14  type exec = generic;
    3.15 +type execution = generic;
    3.16  
    3.17  val none = 0;
    3.18  val make = Counter.make ();

     4.1 --- a/src/Pure/PIDE/execution.ML	Fri Jul 12 11:07:02 2013 +0200
     4.2 +++ b/src/Pure/PIDE/execution.ML	Fri Jul 12 11:28:03 2013 +0200
     4.3 @@ -1,17 +1,16 @@
     4.4  (*  Title:      Pure/PIDE/execution.ML
     4.5      Author:     Makarius
     4.6  
     4.7 -Global management of command execution fragments.
     4.8 +Global management of execution.  Unique running execution serves as
     4.9 +barrier for further exploration of exec particles.
    4.10  *)
    4.11  
    4.12  signature EXECUTION =
    4.13  sig
    4.14 -  type context
    4.15 -  val no_context: context
    4.16 -  val drop_context: context -> unit
    4.17 -  val fresh_context: unit -> context
    4.18 -  val is_running: context -> bool
    4.19 -  val running: context -> Document_ID.exec -> bool
    4.20 +  val start: unit -> Document_ID.execution
    4.21 +  val discontinue: unit -> unit
    4.22 +  val is_running: Document_ID.execution -> bool
    4.23 +  val running: Document_ID.execution -> Document_ID.exec -> bool
    4.24    val finished: Document_ID.exec -> bool -> unit
    4.25    val is_stable: Document_ID.exec -> bool
    4.26    val peek_running: Document_ID.exec -> Future.group option
    4.27 @@ -22,43 +21,37 @@
    4.28  structure Execution: EXECUTION =
    4.29  struct
    4.30  
    4.31 -(* global state *)
    4.32 +type status = Future.group option;  (*SOME group: running, NONE: canceled*)
    4.33 +val state = Synchronized.var "Execution.state" (Document_ID.none, Inttab.empty: status Inttab.table);
    4.34  
    4.35 -datatype context = Context of Document_ID.generic;
    4.36 -val no_context = Context Document_ID.none;
    4.37  
    4.38 -type status = Future.group option;  (*SOME group: running, NONE: canceled*)
    4.39 -val state = Synchronized.var "Execution.state" (no_context, Inttab.empty: status Inttab.table);
    4.40 +(* unique running execution *)
    4.41  
    4.42 +fun start () =
    4.43 +  let
    4.44 +    val execution_id = Document_ID.make ();
    4.45 +    val _ = Synchronized.change state (apfst (K execution_id));
    4.46 +  in execution_id end;
    4.47  
    4.48 -(* unique execution context *)
    4.49 +fun discontinue () =
    4.50 +  Synchronized.change state (apfst (K Document_ID.none));
    4.51  
    4.52 -fun drop_context context =
    4.53 -  Synchronized.change state
    4.54 -    (apfst (fn context' => if context = context' then no_context else context'));
    4.55 -
    4.56 -fun fresh_context () =
    4.57 -  let
    4.58 -    val context = Context (Document_ID.make ());
    4.59 -    val _ = Synchronized.change state (apfst (K context));
    4.60 -  in context end;
    4.61 -
    4.62 -fun is_running context = context = fst (Synchronized.value state);
    4.63 +fun is_running execution_id = execution_id = fst (Synchronized.value state);
    4.64  
    4.65  
    4.66  (* registered execs *)
    4.67  
    4.68 -fun running context exec_id =
    4.69 +fun running execution_id exec_id =
    4.70    Synchronized.guarded_access state
    4.71 -    (fn (current_context, execs) =>
    4.72 +    (fn (execution_id', execs) =>
    4.73        let
    4.74 -        val cont = context = current_context;
    4.75 +        val continue = execution_id = execution_id';
    4.76          val execs' =
    4.77 -          if cont then
    4.78 +          if continue then
    4.79              Inttab.update_new (exec_id, SOME (Future.the_worker_group ())) execs
    4.80                handle Inttab.DUP dup => error ("Duplicate execution " ^ Document_ID.print dup)
    4.81            else execs;
    4.82 -      in SOME (cont, (current_context, execs')) end);
    4.83 +      in SOME (continue, (execution_id', execs')) end);
    4.84  
    4.85  fun finished exec_id stable =
    4.86    Synchronized.change state
    4.87 @@ -81,11 +74,11 @@
    4.88  
    4.89  fun purge_canceled () =
    4.90    Synchronized.guarded_access state
    4.91 -    (fn (context, execs) =>
    4.92 +    (fn (execution_id, execs) =>
    4.93        let
    4.94          val canceled = Inttab.fold (fn (exec_id, NONE) => cons exec_id | _ => I) execs [];
    4.95          val execs' = fold Inttab.delete canceled execs;
    4.96 -      in SOME ((), (context, execs')) end);
    4.97 +      in SOME ((), (execution_id, execs')) end);
    4.98  
    4.99  fun terminate_all () =
   4.100    let

     5.1 --- a/src/Pure/PIDE/protocol.ML	Fri Jul 12 11:07:02 2013 +0200
     5.2 +++ b/src/Pure/PIDE/protocol.ML	Fri Jul 12 11:28:03 2013 +0200
     5.3 @@ -17,17 +17,17 @@
     5.4  
     5.5  val _ =
     5.6    Isabelle_Process.protocol_command "Document.discontinue_execution"
     5.7 -    (fn [] => Document.discontinue_execution (Document.state ()));
     5.8 +    (fn [] => Execution.discontinue ());
     5.9  
    5.10  val _ =
    5.11    Isabelle_Process.protocol_command "Document.cancel_execution"
    5.12 -    (fn [] => Document.cancel_execution (Document.state ()));
    5.13 +    (fn [] => (Execution.discontinue (); Execution.terminate_all ()));
    5.14  
    5.15  val _ =
    5.16    Isabelle_Process.protocol_command "Document.update"
    5.17      (fn [old_id_string, new_id_string, edits_yxml] => Document.change_state (fn state =>
    5.18        let
    5.19 -        val _ = Document.discontinue_execution state;
    5.20 +        val _ = Execution.discontinue ();
    5.21  
    5.22          val old_id = Document_ID.parse old_id_string;
    5.23          val new_id = Document_ID.parse new_id_string;