# HG changeset patch # User wenzelm # Date 1333748078 -7200 # Node ID fe4b245af74c9fb620f1e218e8914b02ab7a61b5 # Parent a0f257197741840418f0de5b54195de9ad69692d discontinued obsolete last_execs (cf. cd3ab7625519); diff -r a0f257197741 -r fe4b245af74c src/Pure/PIDE/document.ML --- a/src/Pure/PIDE/document.ML Fri Apr 06 14:40:00 2012 +0200 +++ b/src/Pure/PIDE/document.ML Fri Apr 06 23:34:38 2012 +0200 @@ -29,7 +29,7 @@ val cancel_execution: state -> Future.task list val execute: version_id -> state -> state val update: version_id -> version_id -> edit list -> state -> - ((command_id * exec_id option) list * (string * command_id option) list) * state + (command_id * exec_id option) list * state val remove_versions: version_id list -> state -> state val state: unit -> state val change_state: (state -> state) -> unit @@ -70,17 +70,16 @@ header: node_header, perspective: perspective, entries: (exec_id * exec) option Entries.T, (*command entries with excecutions*) - last_exec: command_id option, (*last command with exec state assignment*) result: exec} and version = Version of node Graph.T (*development graph wrt. static imports*) with -fun make_node (touched, header, perspective, entries, last_exec, result) = +fun make_node (touched, header, perspective, entries, result) = Node {touched = touched, header = header, perspective = perspective, - entries = entries, last_exec = last_exec, result = result}; + entries = entries, result = result}; -fun map_node f (Node {touched, header, perspective, entries, last_exec, result}) = - make_node (f (touched, header, perspective, entries, last_exec, result)); +fun map_node f (Node {touched, header, perspective, entries, result}) = + make_node (f (touched, header, perspective, entries, result)); fun make_perspective command_ids : perspective = (Inttab.defined (Inttab.make (map (rpair ()) command_ids)), try List.last command_ids); @@ -88,35 +87,35 @@ val no_header = Exn.Exn (ERROR "Bad theory header"); val no_perspective = make_perspective []; -val empty_node = make_node (false, no_header, no_perspective, Entries.empty, NONE, no_exec); -val clear_node = map_node (fn (_, header, _, _, _, _) => - (false, header, no_perspective, Entries.empty, NONE, no_exec)); +val empty_node = make_node (false, no_header, no_perspective, Entries.empty, no_exec); +val clear_node = map_node (fn (_, header, _, _, _) => + (false, header, no_perspective, Entries.empty, no_exec)); (* basic components *) fun is_touched (Node {touched, ...}) = touched; fun set_touched touched = - map_node (fn (_, header, perspective, entries, last_exec, result) => - (touched, header, perspective, entries, last_exec, result)); + map_node (fn (_, header, perspective, entries, result) => + (touched, header, perspective, entries, result)); fun get_header (Node {header, ...}) = header; fun set_header header = - map_node (fn (touched, _, perspective, entries, last_exec, result) => - (touched, header, perspective, entries, last_exec, result)); + map_node (fn (touched, _, perspective, entries, result) => + (touched, header, perspective, entries, result)); fun get_perspective (Node {perspective, ...}) = perspective; fun set_perspective ids = - map_node (fn (touched, header, _, entries, last_exec, result) => - (touched, header, make_perspective ids, entries, last_exec, result)); + map_node (fn (touched, header, _, entries, result) => + (touched, header, make_perspective ids, entries, result)); val visible_command = #1 o get_perspective; val visible_last = #2 o get_perspective; val visible_node = is_some o visible_last fun map_entries f = - map_node (fn (touched, header, perspective, entries, last_exec, result) => - (touched, header, perspective, f entries, last_exec, result)); + map_node (fn (touched, header, perspective, entries, result) => + (touched, header, perspective, f entries, result)); fun get_entries (Node {entries, ...}) = entries; fun iterate_entries f = Entries.iterate NONE f o get_entries; @@ -125,15 +124,10 @@ NONE => I | SOME id => Entries.iterate (SOME id) f entries); -fun get_last_exec (Node {last_exec, ...}) = last_exec; -fun set_last_exec last_exec = - map_node (fn (touched, header, perspective, entries, _, result) => - (touched, header, perspective, entries, last_exec, result)); - fun get_result (Node {result, ...}) = result; fun set_result result = - map_node (fn (touched, header, perspective, entries, last_exec, _) => - (touched, header, perspective, entries, last_exec, result)); + map_node (fn (touched, header, perspective, entries, _) => + (touched, header, perspective, entries, result)); fun get_node nodes name = Graph.get_node nodes name handle Graph.UNDEF _ => empty_node; fun default_node name = Graph.default_node (name, empty_node); @@ -499,7 +493,6 @@ val node' = node |> fold reset_entry no_execs |> fold (fn (id, exec) => update_entry id (SOME exec)) execs - |> set_last_exec last_exec |> set_result result |> set_touched false; in ((no_execs, execs, [(name, node')]), node') end) @@ -511,11 +504,10 @@ map (rpair NONE) (maps #1 updated) @ map (fn (command_id, (exec_id, _)) => (command_id, SOME exec_id)) (maps #2 updated); val updated_nodes = maps #3 updated; - val last_execs = map (fn (name, node) => (name, get_last_exec node)) updated_nodes; val state' = state |> define_version new_id (fold put_node updated_nodes new_version); - in ((command_execs, last_execs), state') end; + in (command_execs, state') end; end; diff -r a0f257197741 -r fe4b245af74c src/Pure/PIDE/document.scala --- a/src/Pure/PIDE/document.scala Fri Apr 06 14:40:00 2012 +0200 +++ b/src/Pure/PIDE/document.scala Fri Apr 06 23:34:38 2012 +0200 @@ -296,9 +296,7 @@ result: PartialFunction[Text.Markup, A]): Stream[Text.Info[A]] } - type Assign = - (List[(Document.Command_ID, Option[Document.Exec_ID])], // exec state assignment - List[(String, Option[Document.Command_ID])]) // last exec + type Assign = List[(Document.Command_ID, Option[Document.Exec_ID])] // exec state assignment object State { @@ -311,14 +309,12 @@ final class Assignment private( val command_execs: Map[Command_ID, Exec_ID] = Map.empty, - val last_execs: Map[String, Option[Command_ID]] = Map.empty, val is_finished: Boolean = false) { def check_finished: Assignment = { require(is_finished); this } - def unfinished: Assignment = new Assignment(command_execs, last_execs, false) + def unfinished: Assignment = new Assignment(command_execs, false) - def assign(add_command_execs: List[(Command_ID, Option[Exec_ID])], - add_last_execs: List[(String, Option[Command_ID])]): Assignment = + def assign(add_command_execs: List[(Command_ID, Option[Exec_ID])]): Assignment = { require(!is_finished) val command_execs1 = @@ -326,7 +322,7 @@ case (res, (command_id, None)) => res - command_id case (res, (command_id, Some(exec_id))) => res + (command_id -> exec_id) } - new Assignment(command_execs1, last_execs ++ add_last_execs, true) + new Assignment(command_execs1, true) } } @@ -387,10 +383,9 @@ } } - def assign(id: Version_ID, arg: Assign = (Nil, Nil)): (List[Command], State) = + def assign(id: Version_ID, command_execs: Assign = Nil): (List[Command], State) = { val version = the_version(id) - val (command_execs, last_execs) = arg val (changed_commands, new_execs) = ((Nil: List[Command], execs) /: command_execs) { @@ -404,7 +399,7 @@ } (commands2, execs2) } - val new_assignment = the_assignment(version).assign(command_execs, last_execs) + val new_assignment = the_assignment(version).assign(command_execs) val new_state = copy(assignments = assignments + (id -> new_assignment), execs = new_execs) (changed_commands, new_state) @@ -424,21 +419,6 @@ def tip_stable: Boolean = is_stable(history.tip) def tip_version: Version = history.tip.version.get_finished - def last_exec_offset(name: Node.Name): Text.Offset = - { - val version = tip_version - the_assignment(version).last_execs.get(name.node) match { - case Some(Some(id)) => - val node = version.nodes(name) - val cmd = the_command(id).command - node.command_start(cmd) match { - case None => 0 - case Some(start) => start + cmd.length - } - case _ => 0 - } - } - def continue_history( previous: Future[Version], edits: List[Edit_Text], diff -r a0f257197741 -r fe4b245af74c src/Pure/PIDE/protocol.ML --- a/src/Pure/PIDE/protocol.ML Fri Apr 06 14:40:00 2012 +0200 +++ b/src/Pure/PIDE/protocol.ML Fri Apr 06 23:34:38 2012 +0200 @@ -55,7 +55,7 @@ Output.protocol_message Isabelle_Markup.assign_execs ((new_id, assignment) |> let open XML.Encode - in pair int (pair (list (pair int (option int))) (list (pair string (option int)))) end + in pair int (list (pair int (option int))) end |> YXML.string_of_body); val state2 = Document.execute new_id state1; in state2 end)); diff -r a0f257197741 -r fe4b245af74c src/Pure/PIDE/protocol.scala --- a/src/Pure/PIDE/protocol.scala Fri Apr 06 14:40:00 2012 +0200 +++ b/src/Pure/PIDE/protocol.scala Fri Apr 06 23:34:38 2012 +0200 @@ -17,7 +17,7 @@ try { import XML.Decode._ val body = YXML.parse_body(text) - Some(pair(long, pair(list(pair(long, option(long))), list(pair(string, option(long)))))(body)) + Some(pair(long, list(pair(long, option(long))))(body)) } catch { case ERROR(_) => None