src/Pure/PIDE/document.ML
changeset 52604 ff2f0818aebc
parent 52602 00170ef1dc39
child 52605 a2a805549c74
     1.1 --- a/src/Pure/PIDE/document.ML	Thu Jul 11 22:53:56 2013 +0200
     1.2 +++ b/src/Pure/PIDE/document.ML	Thu Jul 11 23:24:40 2013 +0200
     1.3 @@ -202,27 +202,14 @@
     1.4  end;
     1.5  
     1.6  
     1.7 -(* associated execution *)
     1.8 -
     1.9 -type execution =
    1.10 - {version_id: Document_ID.version,
    1.11 -  group: Future.group,
    1.12 -  continue: bool Synchronized.var};
    1.13 -
    1.14 -val no_execution =
    1.15 - {version_id = Document_ID.none,
    1.16 -  group = Future.new_group NONE,
    1.17 -  continue = Synchronized.var "continue" false};
    1.18 -
    1.19 -fun make_execution version_id =
    1.20 - {version_id = version_id,
    1.21 -  group = Future.new_group NONE,
    1.22 -  continue = Synchronized.var "continue" true};
    1.23 -
    1.24 -
    1.25  
    1.26  (** main state -- document structure and execution process **)
    1.27  
    1.28 +type execution = {version_id: Document_ID.version, context: Exec.context};
    1.29 +
    1.30 +val no_execution = {version_id = Document_ID.none, context = Exec.no_context};
    1.31 +fun make_execution version_id = {version_id = version_id, context = Exec.fresh_context ()};
    1.32 +
    1.33  abstype state = State of
    1.34   {versions: version Inttab.table,  (*version id -> document content*)
    1.35    commands: (string * Token.T list lazy) Inttab.table,  (*command id -> named command span*)
    1.36 @@ -307,34 +294,35 @@
    1.37    in (versions', commands', execution) end);
    1.38  
    1.39  
    1.40 -
    1.41 -(** document execution **)
    1.42 +(* document execution *)
    1.43  
    1.44 -val discontinue_execution =
    1.45 -  execution_of #> (fn {continue, ...} => Synchronized.change continue (K false));
    1.46 +fun discontinue_execution state =
    1.47 +  Exec.drop_context (#context (execution_of state));
    1.48  
    1.49 -val cancel_execution = execution_of #> (fn {group, ...} => Future.cancel_group group);
    1.50 +fun cancel_execution state =
    1.51 +  (Exec.drop_context (#context (execution_of state)); Exec.terminate_all ());
    1.52  
    1.53  fun start_execution state =
    1.54    let
    1.55 -    val {version_id, group, continue} = execution_of state;
    1.56 -    fun running () = Synchronized.guarded_access continue (fn x => SOME (x, x));
    1.57 +    val {version_id, context} = execution_of state;
    1.58      val _ =
    1.59 -      if not (running ()) orelse Task_Queue.is_canceled group then []
    1.60 -      else
    1.61 +      if Exec.is_running context then
    1.62          nodes_of (the_version state version_id) |> String_Graph.schedule
    1.63            (fn deps => fn (name, node) =>
    1.64              if not (visible_node node) andalso finished_theory node then
    1.65                Future.value ()
    1.66              else
    1.67                (singleton o Future.forks)
    1.68 -                {name = "theory:" ^ name, group = SOME (Future.new_group (SOME group)),
    1.69 +                {name = "theory:" ^ name, group = SOME (Future.new_group NONE),
    1.70                    deps = map (Future.task_of o #2) deps, pri = ~2, interrupts = false}
    1.71                  (fn () =>
    1.72                    iterate_entries (fn (_, opt_exec) => fn () =>
    1.73                      (case opt_exec of
    1.74 -                      SOME exec => if running () then SOME (Command.exec exec) else NONE
    1.75 -                    | NONE => NONE)) node ()));
    1.76 +                      SOME exec =>
    1.77 +                        if Exec.is_running context then SOME (Command.exec context exec)
    1.78 +                        else NONE
    1.79 +                    | NONE => NONE)) node ()))
    1.80 +      else [];
    1.81    in () end;
    1.82  
    1.83