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
2.1 --- a/src/Pure/System/session.scala Sun Feb 26 17:44:09 2012 +0100
2.2 +++ b/src/Pure/System/session.scala Sun Feb 26 17:54:35 2012 +0100
2.3 @@ -267,7 +267,7 @@
2.4
2.5 val assignment = global_state().the_assignment(previous).check_finished
2.6 global_state.change(_.define_version(version, assignment))
2.7 - global_state.change_yield(_.assign(version.id, Document.no_assign))
2.8 + global_state.change_yield(_.assign(version.id))
2.9
2.10 prover.get.update_perspective(previous.id, version.id, name, perspective)
2.11 }