src/Pure/PIDE/document.scala
changeset 46682 4a74fbd6f28b
parent 46681 c083a3f621c0
child 46683 fb160aa7a9a8
     1.1 --- a/src/Pure/PIDE/document.scala	Sun Feb 26 17:44:09 2012 +0100
     1.2 +++ b/src/Pure/PIDE/document.scala	Sun Feb 26 17:54:35 2012 +0100
     1.3 @@ -273,15 +273,10 @@
     1.4     (List[(Document.Command_ID, Option[Document.Exec_ID])],  // exec state assignment
     1.5      List[(String, Option[Document.Command_ID])])  // last exec
     1.6  
     1.7 -  val no_assign: Assign = (Nil, Nil)
     1.8 -
     1.9    object State
    1.10    {
    1.11      class Fail(state: State) extends Exception
    1.12  
    1.13 -    val init: State =
    1.14 -      State().define_version(Version.init, Assignment.init).assign(Version.init.id, no_assign)._2
    1.15 -
    1.16      object Assignment
    1.17      {
    1.18        val init: Assignment = Assignment()
    1.19 @@ -307,6 +302,9 @@
    1.20          Assignment(command_execs1, last_execs ++ add_last_execs, true)
    1.21        }
    1.22      }
    1.23 +
    1.24 +    val init: State =
    1.25 +      State().define_version(Version.init, Assignment.init).assign(Version.init.id)._2
    1.26    }
    1.27  
    1.28    sealed case class State(
    1.29 @@ -362,7 +360,7 @@
    1.30            }
    1.31        }
    1.32  
    1.33 -    def assign(id: Version_ID, arg: Assign): (List[Command], State) =
    1.34 +    def assign(id: Version_ID, arg: Assign = (Nil, Nil)): (List[Command], State) =
    1.35      {
    1.36        val version = the_version(id)
    1.37        val (command_execs, last_execs) = arg