--- a/src/Pure/Isar/toplevel.ML Fri Jul 05 09:17:03 2013 +0200
+++ b/src/Pure/Isar/toplevel.ML Fri Jul 05 14:09:06 2013 +0200
@@ -81,8 +81,7 @@
val actual_proof: (Proof_Node.T -> Proof_Node.T) -> transition -> transition
val skip_proof: (int -> int) -> transition -> transition
val skip_proof_to_theory: (int -> bool) -> transition -> transition
- val get_id: transition -> string option
- val put_id: string -> transition -> transition
+ val put_id: int -> transition -> transition
val unknown_theory: transition -> transition
val unknown_proof: transition -> transition
val unknown_context: transition -> transition
@@ -584,13 +583,10 @@
(** toplevel transactions **)
-(* identification *)
+(* runtime position *)
-fun get_id (Transition {pos, ...}) = Position.get_id pos;
-fun put_id id (tr as Transition {pos, ...}) = position (Position.put_id id pos) tr;
-
-
-(* thread position *)
+fun put_id id (tr as Transition {pos, ...}) =
+ position (Position.put_id (Markup.print_int id) pos) tr;
fun setmp_thread_position (Transition {pos, ...}) f x =
Position.setmp_thread_data pos f x;
--- a/src/Pure/PIDE/command.ML Fri Jul 05 09:17:03 2013 +0200
+++ b/src/Pure/PIDE/command.ML Fri Jul 05 14:09:06 2013 +0200
@@ -13,16 +13,19 @@
val memo: (unit -> 'a) -> 'a memo
val memo_value: 'a -> 'a memo
val memo_eval: 'a memo -> 'a
+ val memo_fork: Future.params -> 'a memo -> unit
val memo_result: 'a memo -> 'a
+ val memo_stable: 'a memo -> bool
val read: span -> Toplevel.transition
- val eval: span -> Toplevel.transition ->
- Toplevel.state * {malformed: bool} -> {failed: bool} * (Toplevel.state * {malformed: bool})
- type print = {name: string, pri: int, pr: unit lazy}
- val print: Toplevel.state -> Toplevel.transition -> Toplevel.state -> print list
- type print_function =
- {old_state: Toplevel.state, tr: Toplevel.transition, state: Toplevel.state} ->
- (unit -> unit) option
- val print_function: string -> int -> print_function -> unit
+ type eval_state =
+ {failed: bool, malformed: bool, command: Toplevel.transition, state: Toplevel.state}
+ type eval = eval_state memo
+ val no_eval: eval
+ val eval: span -> Toplevel.transition -> eval_state -> eval_state
+ type print_fn = Toplevel.transition -> Toplevel.state -> unit
+ type print = {name: string, pri: int, exec_id: int, print: unit memo}
+ val print: (unit -> int) -> string -> eval -> print list
+ val print_function: {name: string, pri: int} -> (string -> print_fn option) -> unit
end;
structure Command: COMMAND =
@@ -59,11 +62,21 @@
in SOME (res, Result res) end))
|> Exn.release;
+fun memo_fork params (Memo v) =
+ (case Synchronized.value v of
+ Result _ => ()
+ | _ => ignore ((singleton o Future.forks) params (fn () => memo_eval (Memo v))));
+
fun memo_result (Memo v) =
(case Synchronized.value v of
Result res => Exn.release res
| _ => raise Fail "Unfinished memo result");
+fun memo_stable (Memo v) =
+ (case Synchronized.value v of
+ Expr _ => true
+ | Result res => not (Exn.is_interrupt_exn res));
+
end;
@@ -98,6 +111,14 @@
(* eval *)
+type eval_state =
+ {failed: bool, malformed: bool, command: Toplevel.transition, state: Toplevel.state};
+val no_eval_state: eval_state =
+ {failed = false, malformed = false, command = Toplevel.empty, state = Toplevel.toplevel};
+
+type eval = eval_state memo;
+val no_eval = memo_value no_eval_state;
+
local
fun run int tr st =
@@ -120,9 +141,9 @@
in
-fun eval span tr (st, {malformed}) =
+fun eval span tr ({malformed, state = st, ...}: eval_state) =
if malformed then
- ({failed = true}, (Toplevel.toplevel, {malformed = malformed}))
+ {failed = true, malformed = malformed, command = tr, state = Toplevel.toplevel}
else
let
val malformed' = Toplevel.is_malformed tr;
@@ -142,11 +163,11 @@
let
val _ = if null errs then Exn.interrupt () else ();
val _ = Toplevel.status tr Markup.failed;
- in ({failed = true}, (st, {malformed = malformed'})) end
+ in {failed = true, malformed = malformed', command = tr, state = st} end
| SOME st' =>
let
val _ = proof_status tr st';
- in ({failed = false}, (st', {malformed = malformed'})) end)
+ in {failed = false, malformed = malformed', command = tr, state = st'} end)
end;
end;
@@ -154,16 +175,13 @@
(* print *)
-type print_function =
- {old_state: Toplevel.state, tr: Toplevel.transition, state: Toplevel.state} ->
- (unit -> unit) option;
-
-type print = {name: string, pri: int, pr: unit lazy};
+type print = {name: string, pri: int, exec_id: int, print: unit memo};
+type print_fn = Toplevel.transition -> Toplevel.state -> unit;
local
-val print_functions =
- Synchronized.var "Command.print_functions" ([]: (string * (int * print_function)) list);
+type print_function = string * (int * (string -> print_fn option));
+val print_functions = Synchronized.var "Command.print_functions" ([]: print_function list);
fun output_error tr exn =
List.app (Future.error_msg (Toplevel.pos_of tr)) (ML_Compiler.exn_messages_ids exn);
@@ -174,14 +192,30 @@
in
-fun print st tr st' =
- rev (Synchronized.value print_functions) |> map_filter (fn (name, (pri, f)) =>
- (case Exn.capture (Runtime.controlled_execution f) {old_state = st, tr = tr, state = st'} of
+fun print new_id command_name eval =
+ rev (Synchronized.value print_functions) |> map_filter (fn (name, (pri, get_print_fn)) =>
+ (case Exn.capture (Runtime.controlled_execution get_print_fn) command_name of
Exn.Res NONE => NONE
- | Exn.Res (SOME pr) => SOME {name = name, pri = pri, pr = (Lazy.lazy o print_error tr) pr}
- | Exn.Exn exn => SOME {name = name, pri = pri, pr = Lazy.lazy (fn () => output_error tr exn)}));
+ | Exn.Res (SOME print_fn) =>
+ let
+ val exec_id = new_id ();
+ fun body () =
+ let
+ val {failed, command, state = st', ...} = memo_result eval;
+ val tr = Toplevel.put_id exec_id command;
+ in if failed then () else print_error tr (fn () => print_fn tr st') () end;
+ in SOME {name = name, pri = pri, exec_id = exec_id, print = memo body} end
+ | Exn.Exn exn =>
+ let
+ val exec_id = new_id ();
+ fun body () =
+ let
+ val {command, ...} = memo_result eval;
+ val tr = Toplevel.put_id exec_id command;
+ in output_error tr exn end;
+ in SOME {name = name, pri = pri, exec_id = exec_id, print = memo body} end));
-fun print_function name pri f =
+fun print_function {name, pri} f =
Synchronized.change print_functions (fn funs =>
(if not (AList.defined (op =) funs name) then ()
else warning ("Redefining command print function: " ^ quote name);
@@ -189,14 +223,15 @@
end;
-val _ = print_function "print_state" 0 (fn {tr, state, ...} =>
- let
- val is_init = Toplevel.is_init tr;
- val is_proof = Keyword.is_proof (Toplevel.name_of tr);
- val do_print =
- not is_init andalso
- (Toplevel.print_of tr orelse (is_proof andalso Toplevel.is_proof state));
- in if do_print then SOME (fn () => Toplevel.print_state false state) else NONE end);
+val _ =
+ print_function {name = "print_state", pri = 0} (fn command_name => SOME (fn tr => fn st' =>
+ let
+ val is_init = Keyword.is_theory_begin command_name;
+ val is_proof = Keyword.is_proof command_name;
+ val do_print =
+ not is_init andalso
+ (Toplevel.print_of tr orelse (is_proof andalso Toplevel.is_proof st'));
+ in if do_print then Toplevel.print_state false st' else () end));
end;
--- a/src/Pure/PIDE/command.scala Fri Jul 05 09:17:03 2013 +0200
+++ b/src/Pure/PIDE/command.scala Fri Jul 05 14:09:06 2013 +0200
@@ -75,7 +75,7 @@
private def add_status(st: Markup): State = copy(status = st :: status)
private def add_markup(m: Text.Markup): State = copy(markup = markup + m)
- def + (alt_id: Document.ID, message: XML.Elem): Command.State =
+ def + (alt_id: Document.ID, message: XML.Elem): State =
message match {
case XML.Elem(Markup(Markup.STATUS, _), msgs) =>
(this /: msgs)((state, msg) =>
@@ -125,6 +125,9 @@
case _ => System.err.println("Ignored message without serial number: " + message); this
}
}
+
+ def ++ (other: State): State =
+ copy(results = results ++ other.results) // FIXME merge more content!?
}
@@ -240,4 +243,6 @@
val init_state: Command.State =
Command.State(this, results = init_results, markup = init_markup)
+
+ val empty_state: Command.State = Command.State(this)
}
--- a/src/Pure/PIDE/document.ML Fri Jul 05 09:17:03 2013 +0200
+++ b/src/Pure/PIDE/document.ML Fri Jul 05 14:09:06 2013 +0200
@@ -31,7 +31,7 @@
val start_execution: state -> unit
val timing: bool Unsynchronized.ref
val update: version_id -> version_id -> edit list -> state ->
- (command_id * exec_id option) list * state
+ (command_id * exec_id list) list * state
val state: unit -> state
val change_state: (state -> state) -> unit
end;
@@ -56,23 +56,33 @@
fun err_undef kind id = error ("Undefined " ^ kind ^ ": " ^ print_id id);
+(* command execution *)
+
+type exec = exec_id * (Command.eval * Command.print list); (*eval/print process*)
+val no_exec: exec = (no_id, (Command.no_eval, []));
+
+fun exec_ids_of ((exec_id, (_, prints)): exec) = exec_id :: map #exec_id prints;
+
+fun exec_result ((_, (eval, _)): exec) = Command.memo_result eval;
+
+fun exec_run ((_, (eval, prints)): exec) =
+ (Command.memo_eval eval;
+ prints |> List.app (fn {name, pri, print, ...} =>
+ Command.memo_fork {name = name, group = NONE, deps = [], pri = pri, interrupts = true} print));
+
+
(** document structure **)
type node_header = string * Thy_Header.header * string list;
-type perspective = (command_id -> bool) * command_id option;
+type perspective = Inttab.set * command_id option;
structure Entries = Linear_Set(type key = command_id val ord = int_ord);
-type exec = ((Toplevel.state * {malformed: bool}) * Command.print list) Command.memo;
- (*eval/print process*)
-val no_exec =
- Command.memo_value ((Toplevel.toplevel, {malformed = false}), []: Command.print list);
-
abstype node = Node of
{header: node_header, (*master directory, theory header, errors*)
perspective: perspective, (*visible commands, last visible command*)
- entries: (exec_id * exec) option Entries.T * bool, (*command entries with excecutions, stable*)
- result: exec option} (*result of last execution*)
+ entries: exec option Entries.T * bool, (*command entries with excecutions, stable*)
+ result: Command.eval option} (*result of last execution*)
and version = Version of node String_Graph.T (*development graph wrt. static imports*)
with
@@ -83,7 +93,7 @@
make_node (f (header, perspective, entries, result));
fun make_perspective command_ids : perspective =
- (Inttab.defined (Inttab.make (map (rpair ()) command_ids)), try List.last command_ids);
+ (Inttab.make_set command_ids, try List.last command_ids);
val no_header = ("", Thy_Header.make ("", Position.none) [] [], ["Bad theory header"]);
val no_perspective = make_perspective [];
@@ -112,7 +122,7 @@
fun set_perspective ids =
map_node (fn (header, _, entries, result) => (header, make_perspective ids, entries, result));
-val visible_command = #1 o get_perspective;
+val visible_commands = #1 o get_perspective;
val visible_last = #2 o get_perspective;
val visible_node = is_some o visible_last
@@ -164,8 +174,8 @@
NONE => err_undef "command entry" id
| SOME (exec, _) => exec);
-fun the_default_entry node (SOME id) = (id, the_default (no_id, no_exec) (the_entry node id))
- | the_default_entry _ NONE = (no_id, (no_id, no_exec));
+fun the_default_entry node (SOME id) = (id, the_default no_exec (the_entry node id))
+ | the_default_entry _ NONE = (no_id, no_exec);
fun update_entry id exec =
map_entries (Entries.update (id, exec));
@@ -304,15 +314,18 @@
(* consolidated states *)
-fun stable_command (exec_id, exec) =
- not (Par_Exn.is_interrupted (Future.join_results (Goal.peek_futures exec_id))) andalso
- (case Exn.capture Command.memo_result exec of
- Exn.Exn exn => not (Exn.is_interrupt exn)
- | Exn.Res _ => true);
+fun stable_goals exec_id =
+ not (Par_Exn.is_interrupted (Future.join_results (Goal.peek_futures exec_id)));
+
+fun stable_eval ((exec_id, (eval, _)): exec) =
+ stable_goals exec_id andalso Command.memo_stable eval;
+
+fun stable_print ({exec_id, print, ...}: Command.print) =
+ stable_goals exec_id andalso Command.memo_stable print;
fun finished_theory node =
(case Exn.capture (Command.memo_result o the) (get_result node) of
- Exn.Res ((st, _), _) => can (Toplevel.end_theory Position.none) st
+ Exn.Res {state = st, ...} => can (Toplevel.end_theory Position.none) st
| _ => false);
@@ -325,15 +338,7 @@
fun start_execution state =
let
- fun execute exec =
- Command.memo_eval exec
- |> (fn (_, print) =>
- print |> List.app (fn {name, pri, pr} =>
- Lazy.future {name = name, group = NONE, deps = [], pri = pri, interrupts = true} pr
- |> ignore));
-
val (version_id, group, running) = execution_of state;
-
val _ =
(singleton o Future.forks)
{name = "Document.execution", group = SOME group, deps = [], pri = ~2, interrupts = true}
@@ -350,7 +355,7 @@
(fn () =>
iterate_entries (fn (_, opt_exec) => fn () =>
(case opt_exec of
- SOME (_, exec) => if ! running then SOME (execute exec) else NONE
+ SOME exec => if ! running then SOME (exec_run exec) else NONE
| NONE => NONE)) node ()))));
in () end;
@@ -391,10 +396,10 @@
SOME thy => thy
| NONE =>
Toplevel.end_theory (Position.file_only import)
- (fst (fst
+ (#state
(Command.memo_result
- (the_default no_exec
- (get_result (snd (the (AList.lookup (op =) deps import))))))))));
+ (the_default Command.no_eval
+ (get_result (snd (the (AList.lookup (op =) deps import)))))))));
val _ = Position.reports (map #2 imports ~~ map Theory.get_markup parents);
in Thy_Load.begin_theory master_dir header parents end;
@@ -422,7 +427,7 @@
| SOME (exec_id, exec) =>
(case lookup_entry node0 id of
NONE => false
- | SOME (exec_id0, _) => exec_id = exec_id0 andalso stable_command (exec_id, exec)));
+ | SOME (exec_id0, _) => exec_id = exec_id0 andalso stable_eval (exec_id, exec)));
in SOME (same', (prev, flags')) end
else NONE;
val (same, (common, flags)) =
@@ -438,31 +443,47 @@
if not proper_init andalso is_none init then NONE
else
let
- val (name, span) = the_command state command_id' ||> Lazy.force;
+ val (command_name, span) = the_command state command_id' ||> Lazy.force;
+
fun illegal_init _ = error "Illegal theory header after end of theory";
val (modify_init, init') =
- if Keyword.is_theory_begin name then
+ if Keyword.is_theory_begin command_name then
(Toplevel.modify_init (fn () => the_default illegal_init init span), NONE)
else (I, init);
+
val exec_id' = new_id ();
- val exec_id'_string = print_id exec_id';
- val read =
- Position.setmp_thread_data (Position.id_only exec_id'_string)
- (fn () =>
- Command.read span
- |> modify_init
- |> Toplevel.put_id exec_id'_string);
- val exec' =
+ val eval' =
Command.memo (fn () =>
let
- val ((st, malformed), _) = Command.memo_result (snd (snd command_exec));
- val tr = read ();
- val ({failed}, (st', malformed')) = Command.eval span tr (st, malformed);
- val print = if failed orelse not command_visible then [] else Command.print st tr st';
- in ((st', malformed'), print) end);
- val command_exec' = (command_id', (exec_id', exec'));
+ val eval_state = exec_result (snd command_exec);
+ val tr =
+ Position.setmp_thread_data (Position.id_only (print_id exec_id'))
+ (fn () =>
+ Command.read span
+ |> modify_init
+ |> Toplevel.put_id exec_id') ();
+ in Command.eval span tr eval_state end);
+ val prints' = if command_visible then Command.print new_id command_name eval' else [];
+ val command_exec' = (command_id', (exec_id', (eval', prints')));
in SOME (command_exec' :: execs, command_exec', init') end;
+fun update_prints state node command_id =
+ (case the_entry node command_id of
+ SOME (exec_id, (eval, prints)) =>
+ let
+ val (command_name, _) = the_command state command_id;
+ val new_prints = Command.print new_id command_name eval;
+ val prints' =
+ new_prints |> map (fn new_print =>
+ (case find_first (fn {name, ...} => name = #name new_print) prints of
+ SOME print => if stable_print print then print else new_print
+ | NONE => new_print));
+ in
+ if eq_list (op = o pairself #exec_id) (prints, prints') then NONE
+ else SOME (command_id, (exec_id, (eval, prints')))
+ end
+ | NONE => NONE);
+
in
fun update (old_id: version_id) (new_id: version_id) edits state =
@@ -483,10 +504,10 @@
(fn () =>
let
val imports = map (apsnd Future.join) deps;
- val updated_imports = exists (is_some o #3 o #1 o #2) imports;
+ val changed_imports = exists (#4 o #1 o #2) imports;
val node_required = is_required name;
in
- if updated_imports orelse AList.defined (op =) edits name orelse
+ if changed_imports orelse AList.defined (op =) edits name orelse
not (stable_entries node) orelse not (finished_theory node)
then
let
@@ -496,48 +517,58 @@
check_theory false name node andalso
forall (fn (name, (_, node)) => check_theory true name node) imports;
+ val visible_commands = visible_commands node;
+ val visible_command = Inttab.defined visible_commands;
val last_visible = visible_last node;
+
val (common, (still_visible, initial)) =
- if updated_imports then (NONE, (true, true))
+ if changed_imports then (NONE, (true, true))
else last_common state last_visible node0 node;
val common_command_exec = the_default_entry node common;
- val (new_execs, (command_id', (_, exec')), _) =
+ val (new_execs, (command_id', (_, (eval', _))), _) =
([], common_command_exec, if initial then SOME init else NONE) |>
(still_visible orelse node_required) ?
iterate_entries_after common
(fn ((prev, id), _) => fn res =>
if not node_required andalso prev = last_visible then NONE
- else new_exec state proper_init (visible_command node id) id res) node;
+ else new_exec state proper_init (visible_command id) id res) node;
+
+ val updated_execs =
+ (visible_commands, new_execs) |-> Inttab.fold (fn (id, ()) =>
+ if exists (fn (_, (id', _)) => id = id') new_execs then I
+ else append (the_list (update_prints state node id)));
val no_execs =
iterate_entries_after common
(fn ((_, id0), exec0) => fn res =>
if is_none exec0 then NONE
- else if exists (fn (_, (id, _)) => id0 = id) new_execs then SOME res
+ else if exists (fn (_, (id, _)) => id0 = id) updated_execs
+ then SOME res
else SOME (id0 :: res)) node0 [];
val last_exec = if command_id' = no_id then NONE else SOME command_id';
val result =
if is_some (after_entry node last_exec) then NONE
- else SOME exec';
+ else SOME eval';
val node' = node
|> fold reset_entry no_execs
- |> fold (fn (id, exec) => update_entry id (SOME exec)) new_execs
- |> entries_stable (null new_execs)
+ |> fold (fn (id, exec) => update_entry id (SOME exec)) updated_execs
+ |> entries_stable (null updated_execs)
|> set_result result;
val updated_node =
- if null no_execs andalso null new_execs then NONE
+ if null no_execs andalso null updated_execs then NONE
else SOME (name, node');
- in ((no_execs, new_execs, updated_node), node') end
- else (([], [], NONE), node)
+ val changed_result = not (null no_execs) orelse not (null new_execs);
+ in ((no_execs, updated_execs, updated_node, changed_result), node') end
+ else (([], [], NONE, false), node)
end))
|> Future.joins |> map #1);
val command_execs =
- map (rpair NONE) (maps #1 updated) @
- map (fn (command_id, (exec_id, _)) => (command_id, SOME exec_id)) (maps #2 updated);
+ map (rpair []) (maps #1 updated) @
+ map (fn (command_id, exec) => (command_id, exec_ids_of exec)) (maps #2 updated);
val updated_nodes = map_filter #3 updated;
val state' = state
--- a/src/Pure/PIDE/document.scala Fri Jul 05 09:17:03 2013 +0200
+++ b/src/Pure/PIDE/document.scala Fri Jul 05 14:09:06 2013 +0200
@@ -289,7 +289,7 @@
result: Command.State => PartialFunction[Text.Markup, A]): Stream[Text.Info[A]]
}
- type Assign = List[(Document.Command_ID, Option[Document.Exec_ID])] // exec state assignment
+ type Assign = List[(Document.Command_ID, List[Document.Exec_ID])] // exec state assignment
object State
{
@@ -301,19 +301,19 @@
}
final class Assignment private(
- val command_execs: Map[Command_ID, Exec_ID] = Map.empty,
+ val command_execs: Map[Command_ID, List[Exec_ID]] = Map.empty,
val is_finished: Boolean = false)
{
def check_finished: Assignment = { require(is_finished); this }
def unfinished: Assignment = new Assignment(command_execs, false)
- def assign(add_command_execs: List[(Command_ID, Option[Exec_ID])]): Assignment =
+ def assign(add_command_execs: List[(Command_ID, List[Exec_ID])]): Assignment =
{
require(!is_finished)
val command_execs1 =
(command_execs /: add_command_execs) {
- case (res, (command_id, None)) => res - command_id
- case (res, (command_id, Some(exec_id))) => res + (command_id -> exec_id)
+ case (res, (command_id, Nil)) => res - command_id
+ case (res, assign) => res + assign
}
new Assignment(command_execs1, true)
}
@@ -357,8 +357,8 @@
}
def the_version(id: Version_ID): Version = versions.getOrElse(id, fail)
- def the_command_state(id: Command_ID): Command.State = commands.getOrElse(id, fail)
- def the_exec(id: Exec_ID): Command.State = execs.getOrElse(id, fail)
+ def the_read_state(id: Command_ID): Command.State = commands.getOrElse(id, fail)
+ def the_exec_state(id: Exec_ID): Command.State = execs.getOrElse(id, fail)
def the_assignment(version: Version): State.Assignment =
assignments.getOrElse(version.id, fail)
@@ -383,12 +383,17 @@
val (changed_commands, new_execs) =
((Nil: List[Command], execs) /: command_execs) {
case ((commands1, execs1), (cmd_id, exec)) =>
- val st = the_command_state(cmd_id)
- val commands2 = st.command :: commands1
+ val st1 = the_read_state(cmd_id)
+ val command = st1.command
+ val st0 = command.empty_state
+
+ val commands2 = command :: commands1
val execs2 =
exec match {
- case None => execs1
- case Some(exec_id) => execs1 + (exec_id -> st)
+ case Nil => execs1
+ case eval_id :: print_ids =>
+ execs1 + (eval_id -> execs.getOrElse(eval_id, st1)) ++
+ print_ids.iterator.map(id => id -> execs.getOrElse(id, st0))
}
(commands2, execs2)
}
@@ -445,12 +450,11 @@
command <- node.commands.iterator
} {
val id = command.id
- if (!commands1.isDefinedAt(id) && commands.isDefinedAt(id))
- commands1 += (id -> commands(id))
- if (command_execs.isDefinedAt(id)) {
- val exec_id = command_execs(id)
- if (!execs1.isDefinedAt(exec_id) && execs.isDefinedAt(exec_id))
- execs1 += (exec_id -> execs(exec_id))
+ if (!commands1.isDefinedAt(id))
+ commands.get(id).foreach(st => commands1 += (id -> st))
+ for (exec_id <- command_execs.getOrElse(id, Nil)) {
+ if (!execs1.isDefinedAt(exec_id))
+ execs.get(exec_id).foreach(st => execs1 += (exec_id -> st))
}
}
copy(versions = versions1, commands = commands1, execs = execs1, assignments = assignments1)
@@ -460,12 +464,15 @@
{
require(is_assigned(version))
try {
- the_exec(the_assignment(version).check_finished.command_execs
- .getOrElse(command.id, fail))
+ the_assignment(version).check_finished.command_execs.getOrElse(command.id, Nil)
+ .map(the_exec_state(_)) match {
+ case eval_state :: print_states => (eval_state /: print_states)(_ ++ _)
+ case Nil => fail
+ }
}
catch {
case _: State.Fail =>
- try { the_command_state(command.id) }
+ try { the_read_state(command.id) }
catch { case _: State.Fail => command.init_state }
}
}
--- a/src/Pure/PIDE/protocol.ML Fri Jul 05 09:17:03 2013 +0200
+++ b/src/Pure/PIDE/protocol.ML Fri Jul 05 14:09:06 2013 +0200
@@ -53,7 +53,7 @@
Output.protocol_message Markup.assign_execs
((new_id, assignment) |>
let open XML.Encode
- in pair int (list (pair int (option int))) end
+ in pair int (list (pair int (list int))) end
|> YXML.string_of_body);
val _ = List.app Future.cancel_group (Goal.reset_futures ());
--- a/src/Pure/PIDE/protocol.scala Fri Jul 05 09:17:03 2013 +0200
+++ b/src/Pure/PIDE/protocol.scala Fri Jul 05 14:09:06 2013 +0200
@@ -17,7 +17,7 @@
try {
import XML.Decode._
val body = YXML.parse_body(text)
- Some(pair(long, list(pair(long, option(long))))(body))
+ Some(pair(long, list(pair(long, list(long))))(body))
}
catch {
case ERROR(_) => None
--- a/src/Tools/jEdit/src/pretty_text_area.scala Fri Jul 05 09:17:03 2013 +0200
+++ b/src/Tools/jEdit/src/pretty_text_area.scala Fri Jul 05 14:09:06 2013 +0200
@@ -38,7 +38,7 @@
val state1 =
state0.continue_history(Future.value(version0), edits, Future.value(version1))._2
.define_version(version1, state0.the_assignment(version0))
- .assign(version1.id, List(command.id -> Some(Document.new_id())))._2
+ .assign(version1.id, List(command.id -> List(Document.new_id())))._2
(command.source, state1)
}