1.1 --- a/src/Pure/PIDE/document.ML	Fri Apr 06 14:40:00 2012 +0200
     1.2 +++ b/src/Pure/PIDE/document.ML	Fri Apr 06 23:34:38 2012 +0200
     1.3 @@ -29,7 +29,7 @@
     1.4    val cancel_execution: state -> Future.task list
     1.5    val execute: version_id -> state -> state
     1.6    val update: version_id -> version_id -> edit list -> state ->
     1.7 -    ((command_id * exec_id option) list * (string * command_id option) list) * state
     1.8 +    (command_id * exec_id option) list * state
     1.9    val remove_versions: version_id list -> state -> state
    1.10    val state: unit -> state
    1.11    val change_state: (state -> state) -> unit
    1.12 @@ -70,17 +70,16 @@
    1.13    header: node_header,
    1.14    perspective: perspective,
    1.15    entries: (exec_id * exec) option Entries.T,  (*command entries with excecutions*)
    1.16 -  last_exec: command_id option,  (*last command with exec state assignment*)
    1.17    result: exec}
    1.18  and version = Version of node Graph.T  (*development graph wrt. static imports*)
    1.19  with
    1.20  
    1.21 -fun make_node (touched, header, perspective, entries, last_exec, result) =
    1.22 +fun make_node (touched, header, perspective, entries, result) =
    1.23    Node {touched = touched, header = header, perspective = perspective,
    1.24 -    entries = entries, last_exec = last_exec, result = result};
    1.25 +    entries = entries, result = result};
    1.26  
    1.27 -fun map_node f (Node {touched, header, perspective, entries, last_exec, result}) =
    1.28 -  make_node (f (touched, header, perspective, entries, last_exec, result));
    1.29 +fun map_node f (Node {touched, header, perspective, entries, result}) =
    1.30 +  make_node (f (touched, header, perspective, entries, result));
    1.31  
    1.32  fun make_perspective command_ids : perspective =
    1.33    (Inttab.defined (Inttab.make (map (rpair ()) command_ids)), try List.last command_ids);
    1.34 @@ -88,35 +87,35 @@
    1.35  val no_header = Exn.Exn (ERROR "Bad theory header");
    1.36  val no_perspective = make_perspective [];
    1.37  
    1.38 -val empty_node = make_node (false, no_header, no_perspective, Entries.empty, NONE, no_exec);
    1.39 -val clear_node = map_node (fn (_, header, _, _, _, _) =>
    1.40 -  (false, header, no_perspective, Entries.empty, NONE, no_exec));
    1.41 +val empty_node = make_node (false, no_header, no_perspective, Entries.empty, no_exec);
    1.42 +val clear_node = map_node (fn (_, header, _, _, _) =>
    1.43 +  (false, header, no_perspective, Entries.empty, no_exec));
    1.44  
    1.45  
    1.46  (* basic components *)
    1.47  
    1.48  fun is_touched (Node {touched, ...}) = touched;
    1.49  fun set_touched touched =
    1.50 -  map_node (fn (_, header, perspective, entries, last_exec, result) =>
    1.51 -    (touched, header, perspective, entries, last_exec, result));
    1.52 +  map_node (fn (_, header, perspective, entries, result) =>
    1.53 +    (touched, header, perspective, entries, result));
    1.54  
    1.55  fun get_header (Node {header, ...}) = header;
    1.56  fun set_header header =
    1.57 -  map_node (fn (touched, _, perspective, entries, last_exec, result) =>
    1.58 -    (touched, header, perspective, entries, last_exec, result));
    1.59 +  map_node (fn (touched, _, perspective, entries, result) =>
    1.60 +    (touched, header, perspective, entries, result));
    1.61  
    1.62  fun get_perspective (Node {perspective, ...}) = perspective;
    1.63  fun set_perspective ids =
    1.64 -  map_node (fn (touched, header, _, entries, last_exec, result) =>
    1.65 -    (touched, header, make_perspective ids, entries, last_exec, result));
    1.66 +  map_node (fn (touched, header, _, entries, result) =>
    1.67 +    (touched, header, make_perspective ids, entries, result));
    1.68  
    1.69  val visible_command = #1 o get_perspective;
    1.70  val visible_last = #2 o get_perspective;
    1.71  val visible_node = is_some o visible_last
    1.72  
    1.73  fun map_entries f =
    1.74 -  map_node (fn (touched, header, perspective, entries, last_exec, result) =>
    1.75 -    (touched, header, perspective, f entries, last_exec, result));
    1.76 +  map_node (fn (touched, header, perspective, entries, result) =>
    1.77 +    (touched, header, perspective, f entries, result));
    1.78  fun get_entries (Node {entries, ...}) = entries;
    1.79  
    1.80  fun iterate_entries f = Entries.iterate NONE f o get_entries;
    1.81 @@ -125,15 +124,10 @@
    1.82      NONE => I
    1.83    | SOME id => Entries.iterate (SOME id) f entries);
    1.84  
    1.85 -fun get_last_exec (Node {last_exec, ...}) = last_exec;
    1.86 -fun set_last_exec last_exec =
    1.87 -  map_node (fn (touched, header, perspective, entries, _, result) =>
    1.88 -    (touched, header, perspective, entries, last_exec, result));
    1.89 -
    1.90  fun get_result (Node {result, ...}) = result;
    1.91  fun set_result result =
    1.92 -  map_node (fn (touched, header, perspective, entries, last_exec, _) =>
    1.93 -    (touched, header, perspective, entries, last_exec, result));
    1.94 +  map_node (fn (touched, header, perspective, entries, _) =>
    1.95 +    (touched, header, perspective, entries, result));
    1.96  
    1.97  fun get_node nodes name = Graph.get_node nodes name handle Graph.UNDEF _ => empty_node;
    1.98  fun default_node name = Graph.default_node (name, empty_node);
    1.99 @@ -499,7 +493,6 @@
   1.100                      val node' = node
   1.101                        |> fold reset_entry no_execs
   1.102                        |> fold (fn (id, exec) => update_entry id (SOME exec)) execs
   1.103 -                      |> set_last_exec last_exec
   1.104                        |> set_result result
   1.105                        |> set_touched false;
   1.106                    in ((no_execs, execs, [(name, node')]), node') end)
   1.107 @@ -511,11 +504,10 @@
   1.108        map (rpair NONE) (maps #1 updated) @
   1.109        map (fn (command_id, (exec_id, _)) => (command_id, SOME exec_id)) (maps #2 updated);
   1.110      val updated_nodes = maps #3 updated;
   1.111 -    val last_execs = map (fn (name, node) => (name, get_last_exec node)) updated_nodes;
   1.112  
   1.113      val state' = state
   1.114        |> define_version new_id (fold put_node updated_nodes new_version);
   1.115 -  in ((command_execs, last_execs), state') end;
   1.116 +  in (command_execs, state') end;
   1.117  
   1.118  end;
   1.119  

     2.1 --- a/src/Pure/PIDE/document.scala	Fri Apr 06 14:40:00 2012 +0200
     2.2 +++ b/src/Pure/PIDE/document.scala	Fri Apr 06 23:34:38 2012 +0200
     2.3 @@ -296,9 +296,7 @@
     2.4        result: PartialFunction[Text.Markup, A]): Stream[Text.Info[A]]
     2.5    }
     2.6  
     2.7 -  type Assign =
     2.8 -   (List[(Document.Command_ID, Option[Document.Exec_ID])],  // exec state assignment
     2.9 -    List[(String, Option[Document.Command_ID])])  // last exec
    2.10 +  type Assign = List[(Document.Command_ID, Option[Document.Exec_ID])]  // exec state assignment
    2.11  
    2.12    object State
    2.13    {
    2.14 @@ -311,14 +309,12 @@
    2.15  
    2.16      final class Assignment private(
    2.17        val command_execs: Map[Command_ID, Exec_ID] = Map.empty,
    2.18 -      val last_execs: Map[String, Option[Command_ID]] = Map.empty,
    2.19        val is_finished: Boolean = false)
    2.20      {
    2.21        def check_finished: Assignment = { require(is_finished); this }
    2.22 -      def unfinished: Assignment = new Assignment(command_execs, last_execs, false)
    2.23 +      def unfinished: Assignment = new Assignment(command_execs, false)
    2.24  
    2.25 -      def assign(add_command_execs: List[(Command_ID, Option[Exec_ID])],
    2.26 -        add_last_execs: List[(String, Option[Command_ID])]): Assignment =
    2.27 +      def assign(add_command_execs: List[(Command_ID, Option[Exec_ID])]): Assignment =
    2.28        {
    2.29          require(!is_finished)
    2.30          val command_execs1 =
    2.31 @@ -326,7 +322,7 @@
    2.32              case (res, (command_id, None)) => res - command_id
    2.33              case (res, (command_id, Some(exec_id))) => res + (command_id -> exec_id)
    2.34            }
    2.35 -        new Assignment(command_execs1, last_execs ++ add_last_execs, true)
    2.36 +        new Assignment(command_execs1, true)
    2.37        }
    2.38      }
    2.39  
    2.40 @@ -387,10 +383,9 @@
    2.41            }
    2.42        }
    2.43  
    2.44 -    def assign(id: Version_ID, arg: Assign = (Nil, Nil)): (List[Command], State) =
    2.45 +    def assign(id: Version_ID, command_execs: Assign = Nil): (List[Command], State) =
    2.46      {
    2.47        val version = the_version(id)
    2.48 -      val (command_execs, last_execs) = arg
    2.49  
    2.50        val (changed_commands, new_execs) =
    2.51          ((Nil: List[Command], execs) /: command_execs) {
    2.52 @@ -404,7 +399,7 @@
    2.53                }
    2.54              (commands2, execs2)
    2.55          }
    2.56 -      val new_assignment = the_assignment(version).assign(command_execs, last_execs)
    2.57 +      val new_assignment = the_assignment(version).assign(command_execs)
    2.58        val new_state = copy(assignments = assignments + (id -> new_assignment), execs = new_execs)
    2.59  
    2.60        (changed_commands, new_state)
    2.61 @@ -424,21 +419,6 @@
    2.62      def tip_stable: Boolean = is_stable(history.tip)
    2.63      def tip_version: Version = history.tip.version.get_finished
    2.64  
    2.65 -    def last_exec_offset(name: Node.Name): Text.Offset =
    2.66 -    {
    2.67 -      val version = tip_version
    2.68 -      the_assignment(version).last_execs.get(name.node) match {
    2.69 -        case Some(Some(id)) =>
    2.70 -          val node = version.nodes(name)
    2.71 -          val cmd = the_command(id).command
    2.72 -          node.command_start(cmd) match {
    2.73 -            case None => 0
    2.74 -            case Some(start) => start + cmd.length
    2.75 -          }
    2.76 -        case _ => 0
    2.77 -      }
    2.78 -    }
    2.79 -
    2.80      def continue_history(
    2.81          previous: Future[Version],
    2.82          edits: List[Edit_Text],

     3.1 --- a/src/Pure/PIDE/protocol.ML	Fri Apr 06 14:40:00 2012 +0200
     3.2 +++ b/src/Pure/PIDE/protocol.ML	Fri Apr 06 23:34:38 2012 +0200
     3.3 @@ -55,7 +55,7 @@
     3.4            Output.protocol_message Isabelle_Markup.assign_execs
     3.5              ((new_id, assignment) |>
     3.6                let open XML.Encode
     3.7 -              in pair int (pair (list (pair int (option int))) (list (pair string (option int)))) end
     3.8 +              in pair int (list (pair int (option int))) end
     3.9                |> YXML.string_of_body);
    3.10          val state2 = Document.execute new_id state1;
    3.11        in state2 end));

     4.1 --- a/src/Pure/PIDE/protocol.scala	Fri Apr 06 14:40:00 2012 +0200
     4.2 +++ b/src/Pure/PIDE/protocol.scala	Fri Apr 06 23:34:38 2012 +0200
     4.3 @@ -17,7 +17,7 @@
     4.4        try {
     4.5          import XML.Decode._
     4.6          val body = YXML.parse_body(text)
     4.7 -        Some(pair(long, pair(list(pair(long, option(long))), list(pair(string, option(long)))))(body))
     4.8 +        Some(pair(long, list(pair(long, option(long))))(body))
     4.9        }
    4.10        catch {
    4.11          case ERROR(_) => None