fully synchronized guard of running execution;
authorwenzelm
Thu Jul 11 12:28:24 2013 +0200 (2013-07-11)
changeset 5259576883c1e1c53
parent 52589 d28d2d89034d
child 52596 40298d383463
fully synchronized guard of running execution;
tuned;
src/Pure/PIDE/document.ML
     1.1 --- a/src/Pure/PIDE/document.ML	Thu Jul 11 11:40:21 2013 +0200
     1.2 +++ b/src/Pure/PIDE/document.ML	Thu Jul 11 12:28:24 2013 +0200
     1.3 @@ -202,18 +202,26 @@
     1.4  end;
     1.5  
     1.6  
     1.7 -
     1.8 -(** main state -- document structure and execution process **)
     1.9 +(* associated execution *)
    1.10  
    1.11  type execution =
    1.12   {version_id: Document_ID.version,
    1.13    group: Future.group,
    1.14 -  running: bool Unsynchronized.ref};
    1.15 +  continue: bool Synchronized.var};
    1.16  
    1.17  val no_execution =
    1.18   {version_id = Document_ID.none,
    1.19    group = Future.new_group NONE,
    1.20 -  running = Unsynchronized.ref false};
    1.21 +  continue = Synchronized.var "continue" false};
    1.22 +
    1.23 +fun make_execution version_id =
    1.24 + {version_id = version_id,
    1.25 +  group = Future.new_group NONE,
    1.26 +  continue = Synchronized.var "continue" true};
    1.27 +
    1.28 +
    1.29 +
    1.30 +(** main state -- document structure and execution process **)
    1.31  
    1.32  abstype state = State of
    1.33   {versions: version Inttab.table,  (*version id -> document content*)
    1.34 @@ -240,10 +248,7 @@
    1.35      let
    1.36        val versions' = Inttab.update_new (version_id, version) versions
    1.37          handle Inttab.DUP dup => err_dup "document version" dup;
    1.38 -      val execution' =
    1.39 -       {version_id = version_id,
    1.40 -        group = Future.new_group NONE,
    1.41 -        running = Unsynchronized.ref true};
    1.42 +      val execution' = make_execution version_id;
    1.43      in (versions', commands, execution') end);
    1.44  
    1.45  fun the_version (State {versions, ...}) version_id =
    1.46 @@ -305,15 +310,18 @@
    1.47  
    1.48  (** document execution **)
    1.49  
    1.50 -val discontinue_execution = execution_of #> (fn {running, ...} => running := false);
    1.51 +val discontinue_execution =
    1.52 +  execution_of #> (fn {continue, ...} => Synchronized.change continue (K false));
    1.53 +
    1.54  val cancel_execution = execution_of #> (fn {group, ...} => Future.cancel_group group);
    1.55  val terminate_execution = execution_of #> (fn {group, ...} => Future.terminate group);
    1.56  
    1.57  fun start_execution state =
    1.58    let
    1.59 -    val {version_id, group, running} = execution_of state;
    1.60 +    val {version_id, group, continue} = execution_of state;
    1.61 +    fun running () = Synchronized.guarded_access continue (fn x => SOME (x, x));
    1.62      val _ =
    1.63 -      if not (! running) orelse Task_Queue.is_canceled group then []
    1.64 +      if not (running ()) orelse Task_Queue.is_canceled group then []
    1.65        else
    1.66          nodes_of (the_version state version_id) |> String_Graph.schedule
    1.67            (fn deps => fn (name, node) =>
    1.68 @@ -326,7 +334,7 @@
    1.69                  (fn () =>
    1.70                    iterate_entries (fn (_, opt_exec) => fn () =>
    1.71                      (case opt_exec of
    1.72 -                      SOME exec => if ! running then SOME (Command.execute exec) else NONE
    1.73 +                      SOME exec => if running () then SOME (Command.execute exec) else NONE
    1.74                      | NONE => NONE)) node ()));
    1.75    in () end;
    1.76