From 573d34069a9ddbc23e7d99bbcefac27c183abb12 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Fri, 9 Aug 2002 08:08:31 +0000
Subject: New files.

---
 etc/isar/new-parsing-test.el | 38 ++++++++++++++++++++++++++++++++++++++
 1 file changed, 38 insertions(+)
 create mode 100644 etc/isar/new-parsing-test.el

diff --git a/etc/isar/new-parsing-test.el b/etc/isar/new-parsing-test.el
new file mode 100644
index 00000000..147ad476
--- /dev/null
+++ b/etc/isar/new-parsing-test.el
@@ -0,0 +1,38 @@
+;; 
+;; Temporary test for new code in proof-done-advancing, following
+;; Markus's suggestions in proof-config  
+;; [see doc of proof-really-save-command-p]
+;; 
+;; Not integrated yet for fear of destruction of finely tuned 
+;; PG/Isar instance.
+;; 
+;;  -da  June 02.
+;; 
+;; FIXME: the handling of nesting depth counter doesn't yet work
+;; smoothly in the generic code, especially across undos/forget.
+;; Need to fix when nesting depth is changed, how it is changed,
+;; and choice of kill_proof vs undos for Isar.
+;;
+;; Testing: evaluate this buffer, reload script file 
+;; (to re-execute isar-mode).
+
+(setq proof-nested-goals-p t)
+(setq proof-goal-command-regexp 
+      (concat isar-goal-command-regexp "\\|" isar-local-goal-command-regexp))
+
+(defun isar-goal-command-p (str)
+  "Decide whether argument is a goal or not"
+  (proof-string-match proof-goal-command-regexp str))
+
+;; Reset this to default value
+(setq proof-really-save-command-p (lambda (span cmd) t))
+
+;; Use the new parser, but have to hack the keywords setting
+;; to fix prob with "{"  
+;; [do we??  that was probably buffer-syntactic context/symtab problem]
+(setq proof-script-use-old-parser nil)
+(setq isar-any-command-regexp
+      (isar-ids-to-regexp isar-keywords-major))
+;      (cons "{[^\\*]"  ;; FIXME:
+;	    (isar-ids-to-regexp 
+;	     (remove "{" isar-keywords-major))))
-- 
cgit v1.2.3