propagate information about last command with exec state assignment through document model;

--- a/src/Pure/General/linear_set.ML	Thu Aug 25 13:24:41 2011 +0200
+++ b/src/Pure/General/linear_set.ML	Thu Aug 25 16:44:06 2011 +0200
@@ -14,7 +14,7 @@
   val empty: 'a T
   val is_empty: 'a T -> bool
   val defined: 'a T -> key -> bool
-  val lookup: 'a T -> key -> 'a option
+  val lookup: 'a T -> key -> ('a * key option) option
   val update: key * 'a -> 'a T -> 'a T
   val fold: key option ->
     ((key option * key) * 'a -> 'b -> 'b) -> 'a T -> 'b -> 'b
@@ -70,7 +70,7 @@
 
 fun defined set key = Table.defined (entries_of set) key;
 
-fun lookup set key = Option.map fst (Table.lookup (entries_of set) key);
+fun lookup set key = Table.lookup (entries_of set) key;
 
 fun update (key, x) = map_set (fn (start, entries) =>
   (start, put_entry (key, (x, next_entry entries key)) entries));

--- a/src/Pure/General/markup.ML	Thu Aug 25 13:24:41 2011 +0200
+++ b/src/Pure/General/markup.ML	Thu Aug 25 16:44:06 2011 +0200
@@ -108,9 +108,7 @@
   val failedN: string val failed: T
   val finishedN: string val finished: T
   val versionN: string
-  val execN: string
   val assignN: string val assign: int -> T
-  val editN: string val edit: int * int -> T
   val serialN: string
   val promptN: string val prompt: T
   val readyN: string val ready: T
@@ -353,12 +351,8 @@
 (* interactive documents *)
 
 val versionN = "version";
-val execN = "exec";
 val (assignN, assign) = markup_int "assign" versionN;
 
-val editN = "edit";
-fun edit (cmd_id, exec_id) : T = (editN, [(idN, print_int cmd_id), (execN, print_int exec_id)]);
-
 
 (* messages *)
 

--- a/src/Pure/General/markup.scala	Thu Aug 25 13:24:41 2011 +0200
+++ b/src/Pure/General/markup.scala	Thu Aug 25 16:44:06 2011 +0200
@@ -232,9 +232,7 @@
   /* interactive documents */
 
   val VERSION = "version"
-  val EXEC = "exec"
   val ASSIGN = "assign"
-  val EDIT = "edit"
 
 
   /* prover process */

--- a/src/Pure/PIDE/document.ML	Thu Aug 25 13:24:41 2011 +0200
+++ b/src/Pure/PIDE/document.ML	Thu Aug 25 16:44:06 2011 +0200
@@ -28,7 +28,8 @@
   val join_commands: state -> unit
   val cancel_execution: state -> Future.task list
   val update_perspective: version_id -> version_id -> string -> command_id list -> state -> state
-  val edit: version_id -> version_id -> edit list -> state -> (command_id * exec_id) list * state
+  val edit: version_id -> version_id -> edit list -> state ->
+    ((command_id * exec_id) list * (string * command_id option) list) * state
   val execute: version_id -> state -> state
   val state: unit -> state
   val change_state: (state -> state) -> unit
@@ -58,7 +59,7 @@
 (** document structure **)
 
 type node_header = (string * string list * (string * bool) list) Exn.result;
-type perspective = (command_id -> bool) * command_id list; (*visible commands, canonical order*)
+type perspective = (command_id -> bool) * command_id option; (*visible commands, last*)
 structure Entries = Linear_Set(type key = command_id val ord = int_ord);
 
 abstype node = Node of
@@ -66,58 +67,63 @@
   header: node_header,
   perspective: perspective,
   entries: exec_id option Entries.T,  (*command entries with excecutions*)
+  last_exec: command_id option,  (*last command with exec state assignment*)
   result: Toplevel.state lazy}
 and version = Version of node Graph.T  (*development graph wrt. static imports*)
 with
 
-fun make_node (touched, header, perspective, entries, result) =
+fun make_node (touched, header, perspective, entries, last_exec, result) =
   Node {touched = touched, header = header, perspective = perspective,
-    entries = entries, result = result};
+    entries = entries, last_exec = last_exec, result = result};
 
-fun map_node f (Node {touched, header, perspective, entries, result}) =
-  make_node (f (touched, header, perspective, entries, result));
+fun map_node f (Node {touched, header, perspective, entries, last_exec, result}) =
+  make_node (f (touched, header, perspective, entries, last_exec, result));
 
-fun make_perspective ids : perspective =
-  (Inttab.defined (Inttab.make (map (rpair ()) ids)), ids);
+fun make_perspective command_ids : perspective =
+  (Inttab.defined (Inttab.make (map (rpair ()) command_ids)), try List.last command_ids);
 
+val no_header = Exn.Exn (ERROR "Bad theory header");
 val no_perspective = make_perspective [];
 val no_print = Lazy.value ();
 val no_result = Lazy.value Toplevel.toplevel;
 
-val empty_node =
-  make_node (false, Exn.Exn (ERROR "Bad theory header"), no_perspective, Entries.empty, no_result);
-
-val clear_node =
-  map_node (fn (_, header, _, _, _) => (false, header, no_perspective, Entries.empty, no_result));
+val empty_node = make_node (false, no_header, no_perspective, Entries.empty, NONE, no_result);
+val clear_node = map_node (fn (_, header, _, _, _, _) =>
+  (false, header, no_perspective, Entries.empty, NONE, no_result));
 
 
 (* basic components *)
 
 fun is_touched (Node {touched, ...}) = touched;
 fun set_touched touched =
-  map_node (fn (_, header, perspective, entries, result) =>
-    (touched, header, perspective, entries, result));
+  map_node (fn (_, header, perspective, entries, last_exec, result) =>
+    (touched, header, perspective, entries, last_exec, result));
 
 fun get_header (Node {header, ...}) = header;
 fun set_header header =
-  map_node (fn (touched, _, perspective, entries, result) =>
-    (touched, header, perspective, entries, result));
+  map_node (fn (touched, _, perspective, entries, last_exec, result) =>
+    (touched, header, perspective, entries, last_exec, result));
 
 fun get_perspective (Node {perspective, ...}) = perspective;
 fun set_perspective ids =
-  map_node (fn (touched, header, _, entries, result) =>
-    (touched, header, make_perspective ids, entries, result));
+  map_node (fn (touched, header, _, entries, last_exec, result) =>
+    (touched, header, make_perspective ids, entries, last_exec, result));
 
 fun map_entries f =
-  map_node (fn (touched, header, perspective, entries, result) =>
-    (touched, header, perspective, f entries, result));
+  map_node (fn (touched, header, perspective, entries, last_exec, result) =>
+    (touched, header, perspective, f entries, last_exec, result));
 fun fold_entries start f (Node {entries, ...}) = Entries.fold start f entries;
 fun first_entry start P (Node {entries, ...}) = Entries.get_first start P 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_theory pos (Node {result, ...}) = Toplevel.end_theory pos (Lazy.force result);
 fun set_result result =
-  map_node (fn (touched, header, perspective, entries, _) =>
-    (touched, header, perspective, entries, result));
+  map_node (fn (touched, header, perspective, entries, last_exec, _) =>
+    (touched, header, perspective, entries, last_exec, 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);
@@ -137,9 +143,14 @@
 fun the_entry (Node {entries, ...}) id =
   (case Entries.lookup entries id of
     NONE => err_undef "command entry" id
-  | SOME entry => entry);
+  | SOME (exec, _) => exec);
 
-fun update_entry (id, exec_id) =
+fun is_last_entry (Node {entries, ...}) id =
+  (case Entries.lookup entries id of
+    SOME (_, SOME _) => false
+  | _ => true);
+
+fun update_entry id exec_id =
   map_entries (Entries.update (id, SOME exec_id));
 
 fun reset_after id entries =
@@ -382,17 +393,19 @@
               (#2 (Future.join (the (AList.lookup (op =) deps import))))));
   in Thy_Load.begin_theory dir thy_name imports files parents end;
 
-fun new_exec state init command_id (assigns, execs, exec) =
+fun new_exec state init command_id' (execs, exec) =
   let
-    val command = the_command state command_id;
+    val command' = the_command state command_id';
     val exec_id' = new_id ();
-    val exec' = exec |> Lazy.map (fn (st, _) =>
-      let val tr =
-        Future.join command
-        |> Toplevel.modify_init init
-        |> Toplevel.put_id (print_id exec_id');
-      in run_command tr st end);
-  in ((command_id, exec_id') :: assigns, (exec_id', (command_id, exec')) :: execs, exec') end;
+    val exec' =
+      snd exec |> Lazy.map (fn (st, _) =>
+        let val tr =
+          Future.join command'
+          |> Toplevel.modify_init init
+          |> Toplevel.put_id (print_id exec_id');
+        in run_command tr st end)
+      |> pair command_id';
+  in ((exec_id', exec') :: execs, exec') end;
 
 in
 
@@ -402,13 +415,13 @@
     val _ = Time.now ();  (* FIXME odd workaround for polyml-5.4.0/x86_64 *)
     val new_version = fold edit_nodes edits old_version;
 
-    val updates =
+    val updated =
       nodes_of new_version |> Graph.schedule
         (fn deps => fn (name, node) =>
-          if not (is_touched node) then Future.value (([], [], []), node)
+          if not (is_touched node) then Future.value (([], []), node)
           else
             (case first_entry NONE (is_changed (node_of old_version name)) node of
-              NONE => Future.value (([], [], []), set_touched false node)
+              NONE => Future.value (([], []), set_touched false node)
             | SOME ((prev, id), _) =>
                 let
                   fun init () = init_theory deps name node;
@@ -422,22 +435,32 @@
                           (case prev of
                             NONE => no_id
                           | SOME prev_id => the_default no_id (the_entry node prev_id));
-                        val (assigns, execs, last_exec) =
+                        val (execs, last_exec as (last_id, _)) =
                           fold_entries (SOME id) (new_exec state init o #2 o #1)
-                            node ([], [], #2 (the_exec state prev_exec));
-                        val node' = node
-                          |> fold update_entry assigns
-                          |> set_result (Lazy.map #1 last_exec)
+                            node ([], the_exec state prev_exec);
+                        val node' =
+                          fold (fn (exec_id, (command_id, _)) => update_entry command_id exec_id)
+                            execs node;
+                        val result =
+                          if is_last_entry node' last_id
+                          then Lazy.map #1 (#2 last_exec)
+                          else no_result;
+                        val node'' = node'
+                          |> set_last_exec (if last_id = no_id then NONE else SOME last_id)
+                          |> set_result result
                           |> set_touched false;
-                      in ((assigns, execs, [(name, node')]), node') end)
+                      in ((execs, [(name, node'')]), node'') end)
                 end))
-      |> Future.joins |> map #1;
+      |> Future.joins |> map #1 |> rev;  (* FIXME why rev? *)
+
+    val updated_nodes = maps #2 updated;
+    val assignment = map (fn (exec_id, (command_id, _)) => (command_id, exec_id)) (maps #1 updated);
+    val last_execs = map (fn (name, node) => (name, get_last_exec node)) updated_nodes;
 
     val state' = state
-      |> fold (fold define_exec o #2) updates
-      |> define_version new_id (fold (fold put_node o #3) updates new_version);
-
-  in (maps #1 (rev updates), state') end;
+      |> fold (fold define_exec o #1) updated
+      |> define_version new_id (fold put_node updated_nodes new_version);
+  in ((assignment, last_execs), state') end;
 
 end;
 

--- a/src/Pure/PIDE/document.scala	Thu Aug 25 13:24:41 2011 +0200
+++ b/src/Pure/PIDE/document.scala	Thu Aug 25 16:44:06 2011 +0200
@@ -204,20 +204,28 @@
       : Stream[Text.Info[Option[A]]]
   }
 
+  type Assign =
+   (List[(Document.Command_ID, Document.Exec_ID)],  // exec state assignment
+    List[(String, Option[Document.Command_ID])])  // last exec
+
+  val no_assign: Assign = (Nil, Nil)
+
   object State
   {
     class Fail(state: State) extends Exception
 
-    val init = State().define_version(Version.init, Map()).assign(Version.init.id, Nil)._2
+    val init = State().define_version(Version.init, Map()).assign(Version.init.id, no_assign)._2
 
     case class Assignment(
       val assignment: Map[Command, Exec_ID],
       val is_finished: Boolean = false)
     {
       def get_finished: Map[Command, Exec_ID] = { require(is_finished); assignment }
-      def assign(command_execs: List[(Command, Exec_ID)]): Assignment =
+      def assign(command_execs: List[(Command, Exec_ID)],
+        last_commands: List[(String, Option[Command])]): Assignment =
       {
         require(!is_finished)
+        // FIXME maintain last_commands
         Assignment(assignment ++ command_execs, true)
       }
     }
@@ -270,9 +278,10 @@
           }
       }
 
-    def assign(id: Version_ID, edits: List[(Command_ID, Exec_ID)]): (List[Command], State) =
+    def assign(id: Version_ID, arg: Assign): (List[Command], State) =
     {
       val version = the_version(id)
+      val (edits, last_ids) = arg
 
       var new_execs = execs
       val assigned_execs =
@@ -282,8 +291,14 @@
           new_execs += (exec_id -> st)
           (st.command, exec_id)
         }
-      val new_assignment = the_assignment(version).assign(assigned_execs)
+
+      val last_commands =
+        last_ids map {
+          case (name, Some(cmd_id)) => (name, Some(the_command(cmd_id).command))
+          case (name, None) => (name, None) }
+      val new_assignment = the_assignment(version).assign(assigned_execs, last_commands)
       val new_state = copy(assignments = assignments + (id -> new_assignment), execs = new_execs)
+
       (assigned_execs.map(_._1), new_state)
     }
 

--- a/src/Pure/PIDE/isar_document.ML	Thu Aug 25 13:24:41 2011 +0200
+++ b/src/Pure/PIDE/isar_document.ML	Thu Aug 25 16:44:06 2011 +0200
@@ -48,12 +48,15 @@
             end;
 
         val running = Document.cancel_execution state;
-        val (updates, state') = Document.edit old_id new_id edits state;
+        val (assignment, state') = Document.edit old_id new_id edits state;
         val _ = Future.join_tasks running;
         val _ = Document.join_commands state';
         val _ =
           Output.status (Markup.markup (Markup.assign new_id)
-            (implode (map (Markup.markup_only o Markup.edit) updates)));
+            (assignment |>
+              let open XML.Encode
+              in pair (list (pair int int)) (list (pair string (option int))) end
+              |> YXML.string_of_body));
         val state'' = Document.execute new_id state';
       in state'' end));
 

--- a/src/Pure/PIDE/isar_document.scala	Thu Aug 25 13:24:41 2011 +0200
+++ b/src/Pure/PIDE/isar_document.scala	Thu Aug 25 16:44:06 2011 +0200
@@ -11,24 +11,20 @@
 {
   /* document editing */
 
-  object Assign {
-    def unapply(msg: XML.Tree)
-        : Option[(Document.Version_ID, List[(Document.Command_ID, Document.Exec_ID)])] =
+  object Assign
+  {
+    def unapply(msg: XML.Tree): Option[(Document.Version_ID, Document.Assign)] =
       msg match {
-        case XML.Elem(Markup(Markup.ASSIGN, List((Markup.VERSION, Document.ID(id)))), edits) =>
-          val id_edits = edits.map(Edit.unapply)
-          if (id_edits.forall(_.isDefined)) Some((id, id_edits.map(_.get)))
-          else None
-        case _ => None
-      }
-  }
-
-  object Edit {
-    def unapply(msg: XML.Tree): Option[(Document.Command_ID, Document.Exec_ID)] =
-      msg match {
-        case XML.Elem(
-          Markup(Markup.EDIT,
-            List((Markup.ID, Document.ID(i)), (Markup.EXEC, Document.ID(j)))), Nil) => Some((i, j))
+        case XML.Elem(Markup(Markup.ASSIGN, List((Markup.VERSION, Document.ID(id)))), body) =>
+          try {
+            import XML.Decode._
+            val a = pair(list(pair(long, long)), list(pair(string, option(long))))(body)
+            Some(id, a)
+          }
+          catch {
+            case _: XML.XML_Atom => None
+            case _: XML.XML_Body => None
+          }
         case _ => None
       }
   }

--- a/src/Pure/System/session.scala	Thu Aug 25 13:24:41 2011 +0200
+++ b/src/Pure/System/session.scala	Thu Aug 25 16:44:06 2011 +0200
@@ -217,7 +217,7 @@
 
       val assignment = global_state().the_assignment(previous).get_finished
       global_state.change(_.define_version(version, assignment))
-      global_state.change_yield(_.assign(version.id, Nil))
+      global_state.change_yield(_.assign(version.id, Document.no_assign))
 
       prover.get.update_perspective(previous.id, version.id, name, perspective)
     }
@@ -248,10 +248,10 @@
 
     /* exec state assignment */
 
-    def handle_assign(id: Document.Version_ID, edits: List[(Document.Command_ID, Document.Exec_ID)])
+    def handle_assign(id: Document.Version_ID, assign: Document.Assign)
     //{{{
     {
-      val cmds = global_state.change_yield(_.assign(id, edits))
+      val cmds = global_state.change_yield(_.assign(id, assign))
       for (cmd <- cmds) command_change_buffer ! cmd
       assignments.event(Session.Assignment)
     }
@@ -336,8 +336,8 @@
           else if (result.is_stdout) { }
           else if (result.is_status) {
             result.body match {
-              case List(Isar_Document.Assign(id, edits)) =>
-                try { handle_assign(id, edits) }
+              case List(Isar_Document.Assign(id, assign)) =>
+                try { handle_assign(id, assign) }
                 catch { case _: Document.State.Fail => bad_result(result) }
               case List(Keyword.Command_Decl(name, kind)) => syntax += (name, kind)
               case List(Keyword.Keyword_Decl(name)) => syntax += name