From d4316a2d63c9c2b12cdce73e62cd435d7ff01002 Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Wed, 6 Oct 1999 11:18:56 +0000 Subject: More improvements/fixes for closing unfinished proofs. Added proof-unnamed-theorem-name. --- lego/lego-syntax.el | 2 +- lego/lego.el | 10 ++++++---- 2 files changed, 7 insertions(+), 5 deletions(-) (limited to 'lego') 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))) -- cgit v1.2.3