tuned signature;
authorwenzelm
Sun, 26 Feb 2012 17:54:35 +0100
changeset 475544a74fbd6f28b
parent 47553 c083a3f621c0
child 47555 fb160aa7a9a8
tuned signature;
src/Pure/PIDE/document.scala
src/Pure/System/session.scala
     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      }