discontinued obsolete last_execs (cf. cd3ab7625519);

--- 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;
 

--- 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],

--- 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));

--- 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