blob: ee530cabf7944583e648dc7878d3b58263d51256 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
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))
|
