# HG changeset patch
# User wenzelm
# Date 1335014765 -7200
# Node ID d6a3b69f4404a6ff0864b51ec7db43568e648bf5
# Parent  b9e132e54d25c0dacbc1119ea8eb22e53c23abec# Parent  4605d4341b8b12908c90773b4a1895694a414483
merged

diff -r b9e132e54d25 -r d6a3b69f4404 src/Pure/General/timing.scala
--- a/src/Pure/General/timing.scala	Sat Apr 21 13:54:29 2012 +0200
+++ b/src/Pure/General/timing.scala	Sat Apr 21 15:26:05 2012 +0200
@@ -10,20 +10,21 @@
 
 object Timing
 {
-  def timeit[A](message: String)(e: => A) =
-  {
-    val start = java.lang.System.currentTimeMillis()
-    val result = Exn.capture(e)
-    val stop = java.lang.System.currentTimeMillis()
+  def timeit[A](message: String, enabled: Boolean = true)(e: => A) =
+    if (enabled) {
+      val start = java.lang.System.currentTimeMillis()
+      val result = Exn.capture(e)
+      val stop = java.lang.System.currentTimeMillis()
 
-    val timing = Time.ms(stop - start)
-    if (timing.is_relevant)
-      java.lang.System.err.println(
-        (if (message == null || message.isEmpty) "" else message + ": ") +
-          timing.message + " elapsed time")
+      val timing = Time.ms(stop - start)
+      if (timing.is_relevant)
+        java.lang.System.err.println(
+          (if (message == null || message.isEmpty) "" else message + ": ") +
+            timing.message + " elapsed time")
 
-    Exn.release(result)
-  }
+      Exn.release(result)
+    }
+    else e
 }
 
 class Timing(val elapsed: Time, val cpu: Time, val gc: Time)
diff -r b9e132e54d25 -r d6a3b69f4404 src/Pure/System/session.scala
--- a/src/Pure/System/session.scala	Sat Apr 21 13:54:29 2012 +0200
+++ b/src/Pure/System/session.scala	Sat Apr 21 15:26:05 2012 +0200
@@ -39,6 +39,12 @@
 
 class Session(thy_load: Thy_Load = new Thy_Load)
 {
+  /* global flags */
+
+  @volatile var timing: Boolean = false
+  @volatile var verbose: Boolean = false
+
+
   /* tuning parameters */  // FIXME properties or settings (!?)
 
   val message_delay = Time.seconds(0.01)  // prover messages
@@ -100,7 +106,10 @@
 
         case Text_Edits(previous, text_edits, version_result) =>
           val prev = previous.get_finished
-          val (doc_edits, version) = Thy_Syntax.text_edits(prover_syntax, prev, text_edits)
+          val (doc_edits, version) =
+            Timing.timeit("Thy_Syntax.text_edits", timing) {
+              Thy_Syntax.text_edits(prover_syntax, prev, text_edits)
+            }
           version_result.fulfill(version)
           sender ! Change(doc_edits, prev, version)
 
@@ -111,12 +120,11 @@
   //}}}
 
 
+
   /** main protocol actor **/
 
   /* global state */
 
-  @volatile var verbose: Boolean = false
-
   @volatile private var prover_syntax =
     Outer_Syntax.init() +
       // FIXME avoid hardwired stuff!?