diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 1999-10-06 11:18:56 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 1999-10-06 11:18:56 +0000 |
| commit | d4316a2d63c9c2b12cdce73e62cd435d7ff01002 (patch) | |
| tree | c5eff6a0c98f2d73725cba83d4f0ceea1b9fa6ec /lego | |
| parent | a7928b121ae5c356eac5e2f48f32faca404a7ce3 (diff) | |
More improvements/fixes for closing unfinished proofs.
Added proof-unnamed-theorem-name.
Diffstat (limited to 'lego')
| -rw-r--r-- | lego/lego-syntax.el | 2 | ||||
| -rw-r--r-- | lego/lego.el | 10 |
2 files changed, 7 insertions, 5 deletions
diff --git a/lego/lego-syntax.el b/lego/lego-syntax.el index 9feb283a..454eeb42 100644 --- a/lego/lego-syntax.el +++ b/lego/lego-syntax.el @@ -82,7 +82,7 @@ ;; Instead of "[^:]+", it may be better to use "lego-id". Furthermore, ;; it might be safer to append "\\s-*:". (defconst lego-goal-with-hole-regexp - (concat "\\(" (proof-ids-to-regexp lego-keywords-goal) "\\)\\s-+\\([^:]+\\)") + (concat "\\(" (proof-ids-to-regexp lego-keywords-goal) "\\)\\s-+\\([^(){},:]+\\)") "Regular expression which matches an entry in `lego-keywords-goal' and the name of the goal.") diff --git a/lego/lego.el b/lego/lego.el index bf906c9f..603b19d5 100644 --- a/lego/lego.el +++ b/lego/lego.el @@ -109,7 +109,7 @@ Activates extended printing routines required for Proof General.") (defvar lego-shell-prompt-pattern "^\\(Lego>[ \201]*\\)+" "*The prompt pattern for the inferior shell running lego.") -(defvar lego-shell-cd "Cd \"%s\";" +(defvar lego-shell-cd "Cd \"%s\"" "*Command of the inferior process to change the directory.") (defvar lego-shell-abort-goal-regexp "KillRef: ok, not in proof state" @@ -216,8 +216,9 @@ Given is the first SPAN which needs to be undone." ((eq (span-property span 'type) 'comment)) ((eq (span-property span 'type) 'goalsave) - (setq ans (concat lego-forget-id-command - (span-property span 'name) proof-terminal-string))) + (unless (eq (span-property span 'name) proof-unnamed-theorem-name) + (setq ans (concat lego-forget-id-command + (span-property span 'name) proof-terminal-string)))) ;; alternative definitions ((proof-string-match lego-definiendum-alternative-regexp str) @@ -243,7 +244,8 @@ Given is the first SPAN which needs to be undone." ((proof-string-match "\\`\\s-*Module\\s-+\\(\\S-+\\)\\W" str) (setq ans (concat "ForgetMark " (match-string 1 str) proof-terminal-string)))) - + ;; Carry on searching forward for something to forget + ;; (The first thing to be forget will forget everything following) (setq span (next-span span 'type))) (or ans proof-no-command))) |