misc tuning and simplification;

--- a/src/Pure/PIDE/document.ML	Wed Aug 24 17:16:48 2011 +0200
+++ b/src/Pure/PIDE/document.ML	Wed Aug 24 17:25:45 2011 +0200
@@ -93,7 +93,7 @@
 
 (* basic components *)
 
-fun get_touched (Node {touched, ...}) = touched;
+fun is_touched (Node {touched, ...}) = touched;
 fun set_touched touched =
   map_node (fn (_, header, perspective, entries, result) =>
     (touched, header, perspective, entries, result));
@@ -405,7 +405,7 @@
     val updates =
       nodes_of new_version |> Graph.schedule
         (fn deps => fn (name, node) =>
-          if not (get_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)

--- a/src/Pure/PIDE/document.scala	Wed Aug 24 17:16:48 2011 +0200
+++ b/src/Pure/PIDE/document.scala	Wed Aug 24 17:25:45 2011 +0200
@@ -224,8 +224,8 @@
 
   sealed case class State(
     val versions: Map[Version_ID, Version] = Map(),
-    val commands: Map[Command_ID, Command.State] = Map(),
-    val execs: Map[Exec_ID, (Command.State, Set[Version])] = Map(),
+    val commands: Map[Command_ID, Command.State] = Map(),  // static markup from define_command
+    val execs: Map[Exec_ID, Command.State] = Map(),  // dynamic markup from execution
     val assignments: Map[Version_ID, State.Assignment] = Map(),
     val disposed: Set[ID] = Set(),  // FIXME unused!?
     val history: History = History.init)
@@ -251,15 +251,15 @@
 
     def the_version(id: Version_ID): Version = versions.getOrElse(id, fail)
     def the_command(id: Command_ID): Command.State = commands.getOrElse(id, fail)
-    def the_exec_state(id: Exec_ID): Command.State = execs.getOrElse(id, fail)._1
+    def the_exec(id: Exec_ID): Command.State = execs.getOrElse(id, fail)
     def the_assignment(version: Version): State.Assignment =
       assignments.getOrElse(version.id, fail)
 
     def accumulate(id: ID, message: XML.Elem): (Command.State, State) =
       execs.get(id) match {
-        case Some((st, occs)) =>
+        case Some(st) =>
           val new_st = st.accumulate(message)
-          (new_st, copy(execs = execs + (id -> (new_st, occs))))
+          (new_st, copy(execs = execs + (id -> new_st)))
         case None =>
           commands.get(id) match {
             case Some(st) =>
@@ -272,14 +272,13 @@
     def assign(id: Version_ID, edits: List[(Command_ID, Exec_ID)]): (List[Command], State) =
     {
       val version = the_version(id)
-      val occs = Set(version)  // FIXME unused (!?)
 
       var new_execs = execs
       val assigned_execs =
         for ((cmd_id, exec_id) <- edits) yield {
           val st = the_command(cmd_id)
           if (new_execs.isDefinedAt(exec_id) || disposed(exec_id)) fail
-          new_execs += (exec_id -> (st, occs))
+          new_execs += (exec_id -> st)
           (st.command, exec_id)
         }
       val new_assignment = the_assignment(version).assign(assigned_execs)
@@ -299,7 +298,8 @@
     def tip_stable: Boolean = is_stable(history.tip)
     def recent_stable: Option[Change] = history.undo_list.find(is_stable)
 
-    def extend_history(previous: Future[Version],
+    def continue_history(
+        previous: Future[Version],
         edits: List[Edit_Text],
         version: Future[Version]): (Change, State) =
     {
@@ -329,7 +329,7 @@
         def lookup_command(id: Command_ID): Option[Command] = State.this.lookup_command(id)
 
         def state(command: Command): Command.State =
-          try { the_exec_state(the_assignment(version).get_finished.getOrElse(command, fail)) }
+          try { the_exec(the_assignment(version).get_finished.getOrElse(command, fail)) }
           catch { case _: State.Fail => command.empty_state }
 
         def convert(offset: Text.Offset) = (offset /: edits)((i, edit) => edit.convert(i))

--- a/src/Pure/System/session.scala	Wed Aug 24 17:16:48 2011 +0200
+++ b/src/Pure/System/session.scala	Wed Aug 24 17:25:45 2011 +0200
@@ -213,7 +213,7 @@
         List((name, Document.Node.Perspective(text_perspective)))
       val change =
         global_state.change_yield(
-          _.extend_history(Future.value(previous), text_edits, Future.value(version)))
+          _.continue_history(Future.value(previous), text_edits, Future.value(version)))
 
       val assignment = global_state().the_assignment(previous).get_finished
       global_state.change(_.define_version(version, assignment))
@@ -235,7 +235,7 @@
       val text_edits = header_edit(name, master_dir, header) :: edits.map(edit => (name, edit))
       val result = Future.fork { Thy_Syntax.text_edits(syntax, previous.join, text_edits) }
       val change =
-        global_state.change_yield(_.extend_history(previous, text_edits, result.map(_._2)))
+        global_state.change_yield(_.continue_history(previous, text_edits, result.map(_._2)))
 
       result.map {
         case (doc_edits, _) =>