From e516288796182bb3a7cd6d10ecbee34a902d78b5 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Fri, 4 Sep 2009 16:35:49 +0000
Subject: Add Elisp timings

---
 etc/isar/AHundredTheorems.thy  | 10 +++++++++-
 etc/isar/AThousandTheorems.thy |  8 +++-----
 2 files changed, 12 insertions(+), 6 deletions(-)

diff --git a/etc/isar/AHundredTheorems.thy b/etc/isar/AHundredTheorems.thy
index 08e4c03a..cc2aebe7 100644
--- a/etc/isar/AHundredTheorems.thy
+++ b/etc/isar/AHundredTheorems.thy
@@ -1,8 +1,9 @@
 theory AHundredTheorems imports Main
 begin
 
-ML {* val start = start_timing(); *}
 
+(* ELISP: -- (setq start (current-time)) -- *)
+ML {* val start = start_timing(); *}
 
 lemma foo: "P --> P" by auto
 lemma foo2: "P --> P" by auto
@@ -105,6 +106,13 @@ lemma foo98: "P --> P" by auto
 lemma foo99: "P --> P" by auto
 lemma foo100: "P --> P" by auto
 
+
+(* NB: this doesn't work because of comment aggregation *)
+(* ELISP: -- (message "Time taken: %f seconds" (time-to-seconds (time-since start))) -- *)
 ML {* Output.warning (#message (end_timing start)); *}
 
 end
+
+
+
+
diff --git a/etc/isar/AThousandTheorems.thy b/etc/isar/AThousandTheorems.thy
index dfb31d58..68f3c474 100644
--- a/etc/isar/AThousandTheorems.thy
+++ b/etc/isar/AThousandTheorems.thy
@@ -2,7 +2,7 @@ theory AThousandTheorems imports Main
 begin
 
 ML {* val start = start_timing(); *}
-
+(* ELISP: -- (setq start (current-time)) -- *)
 
 lemma foo: "P --> P" by auto
 lemma foo2: "P --> P" by auto
@@ -104,10 +104,6 @@ lemma foo97: "P --> P" by auto
 lemma foo98: "P --> P" by auto
 lemma foo99: "P --> P" by auto
 lemma foo100: "P --> P" by auto
-
-
-ML {* #message (end_timing start); *}
-
 lemma foo101: "P --> P" by auto
 lemma foo102: "P --> P" by auto
 lemma foo103: "P --> P" by auto
@@ -1010,5 +1006,7 @@ lemma foo998: "P --> P" by auto
 lemma foo999: "P --> P" by auto
 lemma foo1000: "P --> P" by auto
 
+ML {* Output.warning (#message (end_timing start)); *}
+(* ELISP: -- (message "Time taken: %f seconds" (time-to-seconds (time-since start))) -- *)
 
 end
-- 
cgit v1.2.3