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