1.1 --- a/src/Tools/jEdit/src/proofdocument/document.scala	Mon Jan 11 20:51:58 2010 +0100
     1.2 +++ b/src/Tools/jEdit/src/proofdocument/document.scala	Mon Jan 11 22:01:39 2010 +0100
     1.3 @@ -180,11 +180,13 @@
     1.4    def await_assignment { assignment.join }
     1.5  
     1.6    @volatile private var tmp_states = former_states
     1.7 +  private val time0 = System.currentTimeMillis
     1.8  
     1.9    def assign_states(new_states: List[(Command, Command)])
    1.10    {
    1.11      assignment.fulfill(tmp_states ++ new_states)
    1.12      tmp_states = Map()
    1.13 +    System.err.println("assign_states: " + (System.currentTimeMillis - time0) + " ms elapsed time")
    1.14    }
    1.15  
    1.16    def current_state(cmd: Command): Option[State] =