From dad6a33237ce6af54e9b817526eacfa28815aeb3 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Wed, 10 Jan 2007 13:18:16 +0000
Subject: Comment about undo; use

---
 isar/isar-syntax.el | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/isar/isar-syntax.el b/isar/isar-syntax.el
index 51fc72b4..b70564c7 100644
--- a/isar/isar-syntax.el
+++ b/isar/isar-syntax.el
@@ -452,6 +452,12 @@ matches contents of quotes for quoted identifiers.")
 ;; ----- variations on undo
 
 (defconst isar-undo "ProofGeneral.undo;")  ;; no output undo
+;(defconst isar-undo "undo;")  ;; da: ordinary undo: seems more desirable to use this except
+			       ;; for many composed undos undo;undo;undo; we get output
+			       ;; every time which is a bit inefficient (although not that bad
+			       ;; because the print of the theory is short by default).  
+			       ;; TODO for Isabelle2007: add
+			       ;; times argument to undo and supress intermediate output.
 
 (defun isar-remove (name)
   (concat "init_toplevel; kill_thy " name ";"))
-- 
cgit v1.2.3