# HG changeset patch
# User wenzelm
# Date 1330275275 -3600
# Node ID 4a74fbd6f28bedf10e18954160b033c5a76611d1
# Parent  c083a3f621c0a6c10b6c04ff4237d6c864a9a69c
tuned signature;

diff -r c083a3f621c0 -r 4a74fbd6f28b 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
diff -r c083a3f621c0 -r 4a74fbd6f28b src/Pure/System/session.scala
--- a/src/Pure/System/session.scala	Sun Feb 26 17:44:09 2012 +0100
+++ b/src/Pure/System/session.scala	Sun Feb 26 17:54:35 2012 +0100
@@ -267,7 +267,7 @@
 
       val assignment = global_state().the_assignment(previous).check_finished
       global_state.change(_.define_version(version, assignment))
-      global_state.change_yield(_.assign(version.id, Document.no_assign))
+      global_state.change_yield(_.assign(version.id))
 
       prover.get.update_perspective(previous.id, version.id, name, perspective)
     }