clarified "state" (accumulated data) vs. "exec" (execution that produces data);
generic type Document.id (ML) / Document.ID;

--- a/src/Pure/Isar/isar_document.ML	Thu Aug 12 14:22:23 2010 +0200
+++ b/src/Pure/Isar/isar_document.ML	Thu Aug 12 15:19:11 2010 +0200
@@ -29,14 +29,14 @@
 
 (** documents **)
 
-datatype entry = Entry of {next: Document.command_id option, state: Document.state_id option};
+datatype entry = Entry of {next: Document.command_id option, exec: Document.exec_id option};
 type node = entry Inttab.table; (*unique command entries indexed by command_id, start with no_id*)
 type document = node Graph.T;   (*development graph via static imports*)
 
 
 (* command entries *)
 
-fun make_entry next state = Entry {next = next, state = state};
+fun make_entry next exec = Entry {next = next, exec = exec};
 
 fun the_entry (node: node) (id: Document.command_id) =
   (case Inttab.lookup node id of
@@ -45,12 +45,12 @@
 
 fun put_entry (id: Document.command_id, entry: entry) = Inttab.update (id, entry);
 
-fun put_entry_state (id: Document.command_id) state (node: node) =
+fun put_entry_exec (id: Document.command_id) exec (node: node) =
   let val {next, ...} = the_entry node id
-  in put_entry (id, make_entry next state) node end;
+  in put_entry (id, make_entry next exec) node end;
 
-fun reset_entry_state id = put_entry_state id NONE;
-fun set_entry_state (id, state_id) = put_entry_state id (SOME state_id);
+fun reset_entry_exec id = put_entry_exec id NONE;
+fun set_entry_exec (id, exec_id) = put_entry_exec id (SOME exec_id);
 
 
 (* iterate entries *)
@@ -75,21 +75,21 @@
 (* modify entries *)
 
 fun insert_after (id: Document.command_id) (id2: Document.command_id) (node: node) =
-  let val {next, state} = the_entry node id in
+  let val {next, exec} = the_entry node id in
     node
-    |> put_entry (id, make_entry (SOME id2) state)
+    |> put_entry (id, make_entry (SOME id2) exec)
     |> put_entry (id2, make_entry next NONE)
   end;
 
 fun delete_after (id: Document.command_id) (node: node) =
-  let val {next, state} = the_entry node id in
+  let val {next, exec} = the_entry node id in
     (case next of
       NONE => error ("No next entry to delete: " ^ Document.print_id id)
     | SOME id2 =>
         node |>
           (case #next (the_entry node id2) of
-            NONE => put_entry (id, make_entry NONE state)
-          | SOME id3 => put_entry (id, make_entry (SOME id3) state) #> reset_entry_state id3))
+            NONE => put_entry (id, make_entry NONE exec)
+          | SOME id3 => put_entry (id, make_entry (SOME id3) exec) #> reset_entry_exec id3))
   end;
 
 
@@ -112,24 +112,24 @@
 
 (** global configuration **)
 
-(* states *)
+(* command executions *)
 
 local
 
-val global_states =
+val global_execs =
   Unsynchronized.ref (Inttab.make [(Document.no_id, Lazy.value (SOME Toplevel.toplevel))]);
 
 in
 
-fun define_state (id: Document.state_id) state =
+fun define_exec (id: Document.exec_id) exec =
   NAMED_CRITICAL "Isar" (fn () =>
-    Unsynchronized.change global_states (Inttab.update_new (id, state))
-      handle Inttab.DUP dup => err_dup "state" dup);
+    Unsynchronized.change global_execs (Inttab.update_new (id, exec))
+      handle Inttab.DUP dup => err_dup "exec" dup);
 
-fun the_state (id: Document.state_id) =
-  (case Inttab.lookup (! global_states) id of
-    NONE => err_undef "state" id
-  | SOME state => state);
+fun the_exec (id: Document.exec_id) =
+  (case Inttab.lookup (! global_execs) id of
+    NONE => err_undef "exec" id
+  | SOME exec => exec);
 
 end;
 
@@ -192,8 +192,8 @@
 
 val execution: unit future list Unsynchronized.ref = Unsynchronized.ref [];
 
-fun force_state NONE = ()
-  | force_state (SOME state_id) = ignore (Lazy.force (the_state state_id));
+fun force_exec NONE = ()
+  | force_exec (SOME exec_id) = ignore (Lazy.force (the_exec exec_id));
 
 in
 
@@ -209,7 +209,7 @@
           let
             val _ = await_cancellation ();
             val exec =
-              fold_entries Document.no_id (fn (_, {state, ...}) => fn () => force_state state)
+              fold_entries Document.no_id (fn (_, {exec, ...}) => fn () => force_exec exec)
                 (the_node document name);
           in exec () end));
     in execution := new_execution end);
@@ -221,27 +221,27 @@
 
 local
 
-fun is_changed node' (id, {next = _, state}) =
+fun is_changed node' (id, {next = _, exec}) =
   (case try (the_entry node') id of
     NONE => true
-  | SOME {next = _, state = state'} => state' <> state);
+  | SOME {next = _, exec = exec'} => exec' <> exec);
 
-fun new_state name (id: Document.command_id) (state_id, updates) =
+fun new_exec name (id: Document.command_id) (exec_id, updates) =
   let
-    val state = the_state state_id;
-    val state_id' = create_id ();
-    val tr = Toplevel.put_id (Document.print_id state_id') (the_command id);
-    val state' =
+    val exec = the_exec exec_id;
+    val exec_id' = create_id ();
+    val tr = Toplevel.put_id (Document.print_id exec_id') (the_command id);
+    val exec' =
       Lazy.lazy (fn () =>
-        (case Lazy.force state of
+        (case Lazy.force exec of
           NONE => NONE
         | SOME st => Toplevel.run_command name tr st));
-    val _ = define_state state_id' state';
-  in (state_id', (id, state_id') :: updates) end;
+    val _ = define_exec exec_id' exec';
+  in (exec_id', (id, exec_id') :: updates) end;
 
 fun updates_status updates =
-  implode (map (fn (id, state_id) =>
-    Markup.markup (Markup.edit (Document.print_id id) (Document.print_id state_id)) "") updates)
+  implode (map (fn (id, exec_id) =>
+    Markup.markup (Markup.edit (Document.print_id id) (Document.print_id exec_id)) "") updates)
   |> Markup.markup Markup.assign
   |> Output.status;
 
@@ -259,9 +259,9 @@
             NONE => ([], node)
           | SOME (prev, id, _) =>
               let
-                val prev_state_id = the (#state (the_entry node (the prev)));
-                val (_, updates) = fold_entries id (new_state name o #1) node (prev_state_id, []);
-                val node' = fold set_entry_state updates node;
+                val prev_exec_id = the (#exec (the_entry node (the prev)));
+                val (_, updates) = fold_entries id (new_exec name o #1) node (prev_exec_id, []);
+                val node' = fold set_entry_exec updates node;
               in (rev updates, node') end);
 
         (* FIXME proper node deps *)

--- a/src/Pure/Isar/isar_document.scala	Thu Aug 12 14:22:23 2010 +0200
+++ b/src/Pure/Isar/isar_document.scala	Thu Aug 12 15:19:11 2010 +0200
@@ -20,7 +20,7 @@
   }
 
   object Edit {
-    def unapply(msg: XML.Tree): Option[(Document.Command_ID, Document.State_ID)] =
+    def unapply(msg: XML.Tree): Option[(Document.Command_ID, Document.Exec_ID)] =
       msg match {
         case XML.Elem(Markup(Markup.EDIT, List((Markup.ID, cmd_id), (Markup.STATE, state_id))), Nil) =>
           (Markup.parse_long(cmd_id), Markup.parse_long(state_id)) match {

--- a/src/Pure/PIDE/command.scala	Thu Aug 12 14:22:23 2010 +0200
+++ b/src/Pure/PIDE/command.scala	Thu Aug 12 15:19:11 2010 +0200
@@ -27,7 +27,7 @@
   }
   case class TypeInfo(ty: String)
   case class RefInfo(file: Option[String], line: Option[Int],
-    command_id: Option[Document.Command_ID], offset: Option[Int])  // FIXME Command_ID vs. State_ID !?
+    command_id: Option[Document.Command_ID], offset: Option[Int])  // FIXME Command_ID vs. Exec_ID !?
 
 
 
@@ -201,9 +201,9 @@
     accumulator ! Consume(message, forward)
   }
 
-  def assign_state(state_id: Document.State_ID): Command =
+  def assign_exec(exec_id: Document.Exec_ID): Command =
   {
-    val cmd = new Command(state_id, span, Some(this))
+    val cmd = new Command(exec_id, span, Some(this))
     accumulator !? Assign
     cmd.state = current_state
     cmd

--- a/src/Pure/PIDE/document.ML	Thu Aug 12 14:22:23 2010 +0200
+++ b/src/Pure/PIDE/document.ML	Thu Aug 12 15:19:11 2010 +0200
@@ -7,12 +7,13 @@
 
 signature DOCUMENT =
 sig
-  type state_id = int
-  type command_id = int
-  type version_id = int
-  val no_id: int
-  val parse_id: string -> int
-  val print_id: int -> string
+  type id = int
+  type exec_id = id
+  type command_id = id
+  type version_id = id
+  val no_id: id
+  val parse_id: string -> id
+  val print_id: id -> string
   type edit = string * ((command_id * command_id option) list) option
 end;
 
@@ -21,9 +22,10 @@
 
 (* unique identifiers *)
 
-type state_id = int;
-type command_id = int;
-type version_id = int;
+type id = int;
+type exec_id = id;
+type command_id = id;
+type version_id = id;
 
 val no_id = 0;
 

--- a/src/Pure/PIDE/document.scala	Thu Aug 12 14:22:23 2010 +0200
+++ b/src/Pure/PIDE/document.scala	Thu Aug 12 15:19:11 2010 +0200
@@ -16,14 +16,15 @@
 {
   /* formal identifiers */
 
-  type Version_ID = Long
-  type Command_ID = Long
-  type State_ID = Long
+  type ID = Long
+  type Exec_ID = ID
+  type Command_ID = ID
+  type Version_ID = ID
 
-  val NO_ID = 0L
+  val NO_ID: ID = 0
 
-  def parse_id(s: String): Long = java.lang.Long.parseLong(s)
-  def print_id(id: Long): String = id.toString
+  def parse_id(s: String): ID = java.lang.Long.parseLong(s)
+  def print_id(id: ID): String = id.toString
 
 
 
@@ -80,7 +81,7 @@
   val init: Document =
   {
     val doc = new Document(NO_ID, Map().withDefaultValue(Node.empty), Map())
-    doc.assign_states(Nil)
+    doc.assign_execs(Nil)
     doc
   }
 
@@ -239,7 +240,7 @@
     {
       val doc_edits = new mutable.ListBuffer[Edit[Command]]
       var nodes = old_doc.nodes
-      var former_states = old_doc.assignment.join
+      var former_assignment = old_doc.assignment.join
 
       for ((name, text_edits) <- edits) {
         val commands0 = nodes(name).commands
@@ -255,9 +256,9 @@
 
         doc_edits += (name -> Some(cmd_edits))
         nodes += (name -> new Node(commands2))
-        former_states --= removed_commands
+        former_assignment --= removed_commands
       }
-      (doc_edits.toList, new Document(new_id, nodes, former_states))
+      (doc_edits.toList, new Document(new_id, nodes, former_assignment))
     }
   }
 }
@@ -266,19 +267,19 @@
 class Document(
     val id: Document.Version_ID,
     val nodes: Map[String, Document.Node],
-    former_states: Map[Command, Command])  // FIXME !?
+    former_assignment: Map[Command, Command])  // FIXME !?
 {
   /* command state assignment */
 
   val assignment = Future.promise[Map[Command, Command]]
   def await_assignment { assignment.join }
 
-  @volatile private var tmp_states = former_states
+  @volatile private var tmp_assignment = former_assignment
 
-  def assign_states(new_states: List[(Command, Command)])
+  def assign_execs(execs: List[(Command, Command)])
   {
-    assignment.fulfill(tmp_states ++ new_states)
-    tmp_states = Map()
+    assignment.fulfill(tmp_assignment ++ execs)
+    tmp_assignment = Map()
   }
 
   def current_state(cmd: Command): Command.State =

--- a/src/Pure/System/session.scala	Thu Aug 12 14:22:23 2010 +0200
+++ b/src/Pure/System/session.scala	Thu Aug 12 15:19:11 2010 +0200
@@ -25,11 +25,9 @@
 
   /* managed entities */
 
-  type Entity_ID = Long
-
   trait Entity
   {
-    val id: Entity_ID
+    val id: Document.ID
     def consume(message: XML.Tree, forward: Command => Unit): Unit
   }
 }
@@ -60,8 +58,8 @@
 
   /* unique ids */
 
-  private var id_count: Long = 0
-  def create_id(): Session.Entity_ID = synchronized {
+  private var id_count: Document.ID = 0
+  def create_id(): Document.ID = synchronized {
     require(id_count > java.lang.Long.MIN_VALUE)
     id_count -= 1
     id_count
@@ -74,9 +72,9 @@
   @volatile private var syntax = new Outer_Syntax(system.symbols)
   def current_syntax: Outer_Syntax = syntax
 
-  @volatile private var entities = Map[Session.Entity_ID, Session.Entity]()
-  def lookup_entity(id: Session.Entity_ID): Option[Session.Entity] = entities.get(id)
-  def lookup_command(id: Session.Entity_ID): Option[Command] =
+  @volatile private var entities = Map[Document.ID, Session.Entity]()
+  def lookup_entity(id: Document.ID): Option[Session.Entity] = entities.get(id)
+  def lookup_command(id: Document.ID): Option[Command] =
     lookup_entity(id) match {
       case Some(cmd: Command) => Some(cmd)
       case _ => None
@@ -144,7 +142,7 @@
     {
       raw_results.event(result)
 
-      val target_id: Option[Session.Entity_ID] = Position.get_id(result.properties)
+      val target_id: Option[Document.ID] = Position.get_id(result.properties)
       val target: Option[Session.Entity] =
         target_id match {
           case None => None
@@ -155,20 +153,20 @@
         // global status message
         result.body match {
 
-          // document state assignment
+          // execution assignment
           case List(Isar_Document.Assign(edits)) if target_id.isDefined =>
             documents.get(target_id.get) match {
               case Some(doc) =>
-                val states =
+                val execs =
                   for {
-                    Isar_Document.Edit(cmd_id, state_id) <- edits
+                    Isar_Document.Edit(cmd_id, exec_id) <- edits
                     cmd <- lookup_command(cmd_id)
                   } yield {
-                    val st = cmd.assign_state(state_id)
+                    val st = cmd.assign_exec(exec_id)  // FIXME session state
                     register(st)
                     (cmd, st)
                   }
-                doc.assign_states(states)
+                doc.assign_execs(execs)  // FIXME session state
               case None => bad_result(result)
             }