# HG changeset patch
# User wenzelm
# Date 1263243699 -3600
# Node ID d5bb188b9f9d18720a4ce7c117a30100eee86ee2
# Parent  d0057d9777ce5c9caedea8352aa8acdcb0917e15
more timing;

diff -r d0057d9777ce -r d5bb188b9f9d 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] =