src/Pure/PIDE/document.scala

--- a/src/Pure/PIDE/document.scala	Sun Feb 26 17:44:09 2012 +0100
+++ b/src/Pure/PIDE/document.scala	Sun Feb 26 17:54:35 2012 +0100
@@ -273,15 +273,10 @@
    (List[(Document.Command_ID, Option[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 =
-      State().define_version(Version.init, Assignment.init).assign(Version.init.id, no_assign)._2
-
     object Assignment
     {
       val init: Assignment = Assignment()
@@ -307,6 +302,9 @@
         Assignment(command_execs1, last_execs ++ add_last_execs, true)
       }
     }
+
+    val init: State =
+      State().define_version(Version.init, Assignment.init).assign(Version.init.id)._2
   }
 
   sealed case class State(
@@ -362,7 +360,7 @@
           }
       }
 
-    def assign(id: Version_ID, arg: Assign): (List[Command], State) =
+    def assign(id: Version_ID, arg: Assign = (Nil, Nil)): (List[Command], State) =
     {
       val version = the_version(id)
       val (command_execs, last_execs) = arg