diff options
author | David Aspinall <da@inf.ed.ac.uk> | 2002-08-09 08:08:31 +0000 |
---|---|---|
committer | David Aspinall <da@inf.ed.ac.uk> | 2002-08-09 08:08:31 +0000 |
commit | 573d34069a9ddbc23e7d99bbcefac27c183abb12 (patch) | |
tree | d3cd5840bbce04b800c3628ab0bd85d276dad758 /etc | |
parent | 250232137f6ec5f00440422d9e27d59ada981093 (diff) |
New files.
Diffstat (limited to 'etc')
-rw-r--r-- | etc/isar/new-parsing-test.el | 38 |
1 files changed, 38 insertions, 0 deletions
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)))) |