# HG changeset patch # User wenzelm # Date 1373026146 -7200 # Node ID b6a224676c04e957d112d53305824b92248cdf57 # Parent 1e09c034d6c39a8514c2c6f69ce4e7b13d79dd2f# Parent dbac84eab3bc53eb496e78f7ef74cbb18644a387 merged diff -r 1e09c034d6c3 -r b6a224676c04 src/Pure/Isar/toplevel.ML --- 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; diff -r 1e09c034d6c3 -r b6a224676c04 src/Pure/PIDE/command.ML --- 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; diff -r 1e09c034d6c3 -r b6a224676c04 src/Pure/PIDE/command.scala --- 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) } diff -r 1e09c034d6c3 -r b6a224676c04 src/Pure/PIDE/document.ML --- 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 diff -r 1e09c034d6c3 -r b6a224676c04 src/Pure/PIDE/document.scala --- 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 } } } diff -r 1e09c034d6c3 -r b6a224676c04 src/Pure/PIDE/protocol.ML --- 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 ()); diff -r 1e09c034d6c3 -r b6a224676c04 src/Pure/PIDE/protocol.scala --- 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 diff -r 1e09c034d6c3 -r b6a224676c04 src/Tools/jEdit/src/pretty_text_area.scala --- 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) }