diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2002-06-12 10:32:19 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2002-06-12 10:32:19 +0000 |
| commit | 54bf12bbf49e62d3afb92b67b1ec4f7a4f682666 (patch) | |
| tree | 62f67b439a34e6e16969dc756c1728787f8cbbb5 /isar | |
| parent | 7770e98ef03aba740fdf7d459aac51ce7f0f5993 (diff) | |
New files.
Diffstat (limited to 'isar')
| -rw-r--r-- | isar/test.el | 25 |
1 files changed, 25 insertions, 0 deletions
diff --git a/isar/test.el b/isar/test.el new file mode 100644 index 00000000..ee530cab --- /dev/null +++ b/isar/test.el @@ -0,0 +1,25 @@ +;; +;; 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. + +(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)) |