maintain explicit execution frontier: avoid conflict with former task via static dependency;
start execution immediate after assignment, to keep frontier simple;
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"