maintain explicit execution frontier: avoid conflict with former task via static dependency;
authorwenzelm
Mon Jul 29 16:52:04 2013 +0200 (2013-07-29)
changeset 52774627fb639a2d9
parent 52773 3e8b9d2f18cb
child 52775 e0169f13bd37
maintain explicit execution frontier: avoid conflict with former task via static dependency;
start execution immediate after assignment, to keep frontier simple;
src/Pure/PIDE/command.ML
src/Pure/PIDE/document.ML
src/Pure/PIDE/protocol.ML
     1.1 --- a/src/Pure/PIDE/command.ML	Mon Jul 29 16:01:05 2013 +0200
     1.2 +++ b/src/Pure/PIDE/command.ML	Mon Jul 29 16:52:04 2013 +0200
     1.3 @@ -51,7 +51,7 @@
     1.4   | Result res => not (Exn.is_interrupt_exn res));
     1.5  
     1.6  fun memo_exec execution_id (Memo v) =
     1.7 -  Synchronized.guarded_access v
     1.8 +  Synchronized.timed_access v (K (SOME Time.zeroTime))
     1.9      (fn expr =>
    1.10        (case expr of
    1.11          Expr (exec_id, e) =>
    1.12 @@ -63,7 +63,9 @@
    1.13                in SOME (Exn.is_interrupt_exn res, Result res) end
    1.14              else SOME (true, expr)) ()
    1.15        | Result _ => SOME (false, expr)))
    1.16 -  |> (fn true => Exn.interrupt () | false => ());
    1.17 +  |> (fn SOME false => ()
    1.18 +       | SOME true => Exn.interrupt ()
    1.19 +       | NONE => error "Conflicting command execution");
    1.20  
    1.21  fun memo_fork params execution_id (Memo v) =
    1.22    (case Synchronized.value v of
     2.1 --- a/src/Pure/PIDE/document.ML	Mon Jul 29 16:01:05 2013 +0200
     2.2 +++ b/src/Pure/PIDE/document.ML	Mon Jul 29 16:52:04 2013 +0200
     2.3 @@ -18,7 +18,7 @@
     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 start_execution: state -> unit
     2.8 +  val start_execution: state -> state
     2.9    val timing: bool Unsynchronized.ref
    2.10    val update: Document_ID.version -> Document_ID.version -> edit list -> state ->
    2.11      Document_ID.exec list * (Document_ID.command * Document_ID.exec list) list * state
    2.12 @@ -196,10 +196,16 @@
    2.13  
    2.14  (** main state -- document structure and execution process **)
    2.15  
    2.16 -type execution = {version_id: Document_ID.version, execution_id: Document_ID.execution};
    2.17 +type execution =
    2.18 + {version_id: Document_ID.version,  (*static version id*)
    2.19 +  execution_id: Document_ID.execution,  (*dynamic execution id*)
    2.20 +  frontier: Future.task Symtab.table};  (*node name -> running execution task*)
    2.21  
    2.22 -val no_execution = {version_id = Document_ID.none, execution_id = Document_ID.none};
    2.23 -fun new_execution version_id = {version_id = version_id, execution_id = Execution.start ()};
    2.24 +val no_execution: execution =
    2.25 +  {version_id = Document_ID.none, execution_id = Document_ID.none, frontier = Symtab.empty};
    2.26 +
    2.27 +fun new_execution version_id frontier : execution =
    2.28 +  {version_id = version_id, execution_id = Execution.start (), frontier = frontier};
    2.29  
    2.30  abstype state = State of
    2.31   {versions: version Inttab.table,  (*version id -> document content*)
    2.32 @@ -216,17 +222,15 @@
    2.33  val init_state =
    2.34    make_state (Inttab.make [(Document_ID.none, empty_version)], Inttab.empty, no_execution);
    2.35  
    2.36 -fun execution_of (State {execution, ...}) = execution;
    2.37 -
    2.38  
    2.39  (* document versions *)
    2.40  
    2.41  fun define_version version_id version =
    2.42 -  map_state (fn (versions, commands, _) =>
    2.43 +  map_state (fn (versions, commands, {frontier, ...}) =>
    2.44      let
    2.45        val versions' = Inttab.update_new (version_id, version) versions
    2.46          handle Inttab.DUP dup => err_dup "document version" dup;
    2.47 -      val execution' = new_execution version_id;
    2.48 +      val execution' = new_execution version_id frontier;
    2.49      in (versions', commands, execution') end);
    2.50  
    2.51  fun the_version (State {versions, ...}) version_id =
    2.52 @@ -287,29 +291,37 @@
    2.53  
    2.54  (* document execution *)
    2.55  
    2.56 -fun start_execution state =
    2.57 +fun start_execution state = state |> map_state (fn (versions, commands, execution) =>
    2.58    let
    2.59 -    val {version_id, execution_id} = execution_of state;
    2.60 +    val {version_id, execution_id, frontier} = execution;
    2.61      val pri = Options.default_int "editor_execution_priority";
    2.62 -    val _ =
    2.63 +
    2.64 +    val new_tasks =
    2.65        if Execution.is_running execution_id then
    2.66          nodes_of (the_version state version_id) |> String_Graph.schedule
    2.67            (fn deps => fn (name, node) =>
    2.68              if visible_node node orelse pending_result node then
    2.69 -              (singleton o Future.forks)
    2.70 -                {name = "theory:" ^ name, group = SOME (Future.new_group NONE),
    2.71 -                  deps = map (Future.task_of o #2) deps, pri = pri, interrupts = false}
    2.72 -                (fn () =>
    2.73 -                  iterate_entries (fn (_, opt_exec) => fn () =>
    2.74 -                    (case opt_exec of
    2.75 -                      SOME exec =>
    2.76 -                        if Execution.is_running execution_id
    2.77 -                        then SOME (Command.exec execution_id exec)
    2.78 -                        else NONE
    2.79 -                    | NONE => NONE)) node ())
    2.80 -            else Future.value ())
    2.81 +              let
    2.82 +                val former_task = Symtab.lookup frontier name;
    2.83 +                val future =
    2.84 +                  (singleton o Future.forks)
    2.85 +                    {name = "theory:" ^ name, group = SOME (Future.new_group NONE),
    2.86 +                      deps = the_list former_task @ map #2 (maps #2 deps),
    2.87 +                      pri = pri, interrupts = false}
    2.88 +                    (fn () =>
    2.89 +                      iterate_entries (fn (_, opt_exec) => fn () =>
    2.90 +                        (case opt_exec of
    2.91 +                          SOME exec =>
    2.92 +                            if Execution.is_running execution_id
    2.93 +                            then SOME (Command.exec execution_id exec)
    2.94 +                            else NONE
    2.95 +                        | NONE => NONE)) node ());
    2.96 +              in [(name, Future.task_of future)] end
    2.97 +            else [])
    2.98        else [];
    2.99 -  in () end;
   2.100 +    val frontier' = (fold o fold) Symtab.update new_tasks frontier;
   2.101 +    val execution' = {version_id = version_id, execution_id = execution_id, frontier = frontier'};
   2.102 +  in (versions, commands, execution') end);
   2.103  
   2.104  
   2.105  
     3.1 --- a/src/Pure/PIDE/protocol.ML	Mon Jul 29 16:01:05 2013 +0200
     3.2 +++ b/src/Pure/PIDE/protocol.ML	Mon Jul 29 16:52:04 2013 +0200
     3.3 @@ -58,10 +58,7 @@
     3.4                let open XML.Encode
     3.5                in pair int (list (pair int (list int))) end
     3.6                |> YXML.string_of_body);
     3.7 -        val _ =
     3.8 -          Event_Timer.request (Time.+ (Time.now (), seconds 0.02))
     3.9 -            (fn () => Document.start_execution state');
    3.10 -      in state' end));
    3.11 +      in Document.start_execution state' end));
    3.12  
    3.13  val _ =
    3.14    Isabelle_Process.protocol_command "Document.remove_versions"