diff options
| -rw-r--r-- | generic/proof-config.el | 10 | ||||
| -rw-r--r-- | generic/proof-shell.el | 13 | ||||
| -rw-r--r-- | hol-light/hol-light.el | 17 |
3 files changed, 23 insertions, 17 deletions
diff --git a/generic/proof-config.el b/generic/proof-config.el index 83528b9f..f0633e72 100644 --- a/generic/proof-config.el +++ b/generic/proof-config.el @@ -1155,7 +1155,11 @@ is shown to the user. Set to nil to disable." This is an important setting. Output between `proof-shell-start-goals-regexp' and `proof-shell-end-goals-regexp' will be pasted into the goals buffer and possibly analysed further for proof-by-pointing markup. -If it is left as nil, the goals buffer will not be used." +If it is left as nil, the goals buffer will not be used. + +The goals display starts at the beginning of the match on this +regexp, unless it has a match group, in which case it starts +at (match-end 1)." :type '(choice (const nil) regexp) :group 'proof-shell) @@ -1165,10 +1169,10 @@ This allows a shorter form of the proof state output to be displayed, in case several messages are combined in a command output. The portion treated as the goals output will be that between the -start of the match on `proof-shell-start-goals-regexp' and the +match on `proof-shell-start-goals-regexp' (which see) and the start of the match on `proof-shell-end-goals-regexp'. -If nil, use the whole of the output after +If nil, use the whole of the output from the match on `proof-shell-start-goals-regexp' up to the next prompt." :type '(choice (const nil) regexp) :group 'proof-shell) diff --git a/generic/proof-shell.el b/generic/proof-shell.el index ab0d2d05..9cdce998 100644 --- a/generic/proof-shell.el +++ b/generic/proof-shell.el @@ -1518,11 +1518,16 @@ i.e., 'goals or 'response." (cond ((and proof-shell-start-goals-regexp (proof-re-search-forward proof-shell-start-goals-regexp end t)) - (let* ((gstart (match-beginning 0)) (rstart start) gend) + (let* ((gmark (match-beginning 0)) ; start of goals message + (gstart (or (match-end 1) ; start of actual display + gmark)) + (rstart start) ; possible response before goals + (gend end)) ;; Find the last goal string in the output (goto-char gstart) (while (re-search-forward proof-shell-start-goals-regexp end t) - (setq gstart (match-beginning 0)) + (setq gmark (match-beginning 0)) + (setq gstart (or (match-end 1) gmark)) (setq gend (if (and proof-shell-end-goals-regexp (re-search-forward proof-shell-end-goals-regexp end t)) @@ -1536,10 +1541,10 @@ i.e., 'goals or 'response." (pg-goals-display proof-shell-last-goals-output)) ;; also allow (for Coq) any preceding output as a response ;; FIXME heuristic: 4 allows for annotation in end-goals-regexp - (when (> (- gstart rstart) 4) + (when (> (- gmark rstart) 4) (proof-shell-display-output-as-response flags - (buffer-substring-no-properties rstart gstart))) + (buffer-substring-no-properties rstart gmark))) ;; primary output kind is goals 'goals)) diff --git a/hol-light/hol-light.el b/hol-light/hol-light.el index 6cb7fddd..9876b0d9 100644 --- a/hol-light/hol-light.el +++ b/hol-light/hol-light.el @@ -34,10 +34,12 @@ (defvar hol-light-tacticals nil) (proof-easy-config 'hol-light "HOL Light" + proof-assistant-home-page "https://www.cl.cam.ac.uk/~jrh13/hol-light/" proof-prog-name "ocaml" proof-terminal-string ";;" proof-script-comment-start "(*" proof-script-comment-end "*)" + ;; These are all approximations, of course. proof-goal-command-regexp "^g[ `]" proof-save-command-regexp "pg_top_thm_and_drop" @@ -46,22 +48,17 @@ proof-non-undoables-regexp "b()" ; and others.. proof-goal-command "g `%s`;;" proof-save-command "val %s = pg_top_thm_and_drop();;" - proof-kill-goal-command "print_string \"Goal killed.\";;" ; nothing to do, repeated goals OK + proof-kill-goal-command "current_goalstack:=[];;" ; for cleanliness proof-showproof-command "p()" proof-undo-n-times-cmd "(pg_repeat b %s; p());;" proof-auto-multiple-files t proof-shell-cd-cmd "#cd \"%s\";;" proof-shell-filename-escapes '(("\\\\" . "\\\\") ("\"" . "\\\"")) proof-shell-interrupt-regexp "Interrupted" - proof-shell-start-goals-regexp - (regexp-quote "val it : goalstack = ") -; (proof-regexp-alt "Proof manager status" -; "OK.." -; "val it =\n") - proof-shell-end-goals-regexp - (proof-regexp-alt "^[ \t]*: GoalstackPure.goalstack" - "^[ \t]*: GoalstackPure.proofs") - proof-assistant-home-page "https://www.cl.cam.ac.uk/~jrh13/hol-light/" + proof-shell-start-goals-regexp + (concat + "^\\(" (regexp-quote "val it : goalstack = ") "\\)" + "\\(?:[0-9]*[0-9] subgoals? ([0-9]+ total)\\|No subgoals\\)") proof-shell-annotated-prompt-regexp "# " proof-shell-error-regexp (proof-regexp-alt "Characters [0-9]+-[0-9]+:" "Exception: Failure") |