--- 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
--- 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)
}