more timing;
authorwenzelm
Mon, 11 Jan 2010 22:01:39 +0100
changeset 34868 d5bb188b9f9d
parent 34867 d0057d9777ce
child 34869 502f90967483
more timing;
src/Tools/jEdit/src/proofdocument/document.scala
--- a/src/Tools/jEdit/src/proofdocument/document.scala	Mon Jan 11 20:51:58 2010 +0100
+++ b/src/Tools/jEdit/src/proofdocument/document.scala	Mon Jan 11 22:01:39 2010 +0100
@@ -180,11 +180,13 @@
   def await_assignment { assignment.join }
 
   @volatile private var tmp_states = former_states
+  private val time0 = System.currentTimeMillis
 
   def assign_states(new_states: List[(Command, Command)])
   {
     assignment.fulfill(tmp_states ++ new_states)
     tmp_states = Map()
+    System.err.println("assign_states: " + (System.currentTimeMillis - time0) + " ms elapsed time")
   }
 
   def current_state(cmd: Command): Option[State] =