From e1c67a6cb5ba78af5faf43b87c1869de5f3161b9 Mon Sep 17 00:00:00 2001 From: Hendrik Tews Date: Tue, 15 Jan 2013 14:40:18 +0000 Subject: - support bullets and braces in Prooftree - prooftree protocol change to version 3 --- generic/proof-tree.el | 73 +++++++++++++++++++++++++++++++-------------------- 1 file changed, 45 insertions(+), 28 deletions(-) (limited to 'generic/proof-tree.el') diff --git a/generic/proof-tree.el b/generic/proof-tree.el index b73c2308..969dce05 100644 --- a/generic/proof-tree.el +++ b/generic/proof-tree.el @@ -211,8 +211,13 @@ the state display expands to the end of the prover output." :type '(choice regexp (const nil)) :group 'proof-tree-internals) -(defcustom proof-tree-proof-finished-regexp nil - "Regexp to match the no-more-subgoals message." +(defcustom proof-tree-branch-finished-regexp nil + "Regexp to recognize that the current branch has been finished. +This must match in precisely the following cases: +- The current branch has been finished but there is no current + open subgoal because the prover has not switched to the next + subgoal. +- The last open goal has been proved. " :type 'regexp :group 'proof-tree-internals) @@ -472,7 +477,7 @@ variables." ;; Low-level communication primitives ;; -(defconst proof-tree-protocol-version 2 +(defconst proof-tree-protocol-version 3 "Version of the communication protocol between Proof General and Prooftree. Must be increased if one of the low-level communication primitives is changed.") @@ -547,12 +552,12 @@ DATA as data sections to Prooftree." (1+ (string-bytes proof-name))))) (proof-tree-send-message second-line (list proof-name)))) -(defun proof-tree-send-proof-finished (state proof-name cmd-string +(defun proof-tree-send-branch-finished (state proof-name cmd-string cheated-flag existential-info) - "Send proof-finished to prooftree." + "Send branch-finished to prooftree." (proof-tree-send-message (format - (concat "proof-finished state %d %s proof-name-bytes %d command-bytes %d " + (concat "branch-finished state %d %s proof-name-bytes %d command-bytes %d " "existential-bytes %d") state (if cheated-flag "cheated" "not-cheated") @@ -820,6 +825,7 @@ This function cuts out the text between output, including the matches of these regular expressions. If the start regexp is nil, the empty string is returned. If the end regexp is nil, the match expands to the end of the prover output." + (goto-char start) (if (and proof-tree-existentials-state-start-regexp (proof-re-search-forward proof-tree-existentials-state-start-regexp end t)) @@ -832,7 +838,7 @@ regexp is nil, the match expands to the end of the prover output." (buffer-substring-no-properties start end)) "")) -(defun proof-tree-handle-proof-progress (cmd-string proof-info) +(defun proof-tree-handle-proof-progress (old-proof-marker cmd-string proof-info) "Send CMD-STRING and goals in delayed output to prooftree. This function is called if there is some real progress in a proof. This function sends the current state, the current goal @@ -840,9 +846,13 @@ and the list of additional open subgoals to Prooftree. Prooftree will sort out the rest. The delayed output is in the region -\[proof-shell-delayed-output-start, proof-shell-delayed-output-end]." - ;; (message "PTHPO cmd |%s| info %s flags %s start %s end %s" +\[proof-shell-delayed-output-start, proof-shell-delayed-output-end]. +Urgent messages might be before that, following OLD-PROOF-MARKER, +which contains the position of `proof-marker', before the next +command was sent to the proof assistant." + ;; (message "PTHPO cmd |%s| info %s flags %s proof-marker %s start %s end %s" ;; cmd proof-info flags + ;; old-proof-marker ;; proof-shell-delayed-output-start ;; proof-shell-delayed-output-end) (let* ((start proof-shell-delayed-output-start) @@ -852,10 +862,17 @@ The delayed output is in the region (cheated-flag (and proof-tree-cheating-regexp (proof-string-match proof-tree-cheating-regexp cmd-string))) - (current-goals (proof-tree-extract-goals start end)) - (existential-info - (proof-tree-extract-existential-info start end))) - (if current-goals + current-goals) + ;; Check first for special cases, because Coq's output for finished + ;; branches is almost identical to proper goals. + (goto-char old-proof-marker) + (if (proof-re-search-forward proof-tree-branch-finished-regexp end t) + (proof-tree-send-branch-finished + proof-state proof-name cmd-string cheated-flag + (proof-tree-extract-existential-info start end)) + (goto-char start) + (setq current-goals (proof-tree-extract-goals start end)) + (when current-goals (let ((current-sequent-id (car current-goals)) (current-sequent-text (nth 1 current-goals)) ;; nth 2 current-goals contains the additional ID's @@ -867,21 +884,13 @@ The delayed output is in the region current-sequent-id current-sequent-text (nth 2 current-goals) - existential-info) + (proof-tree-extract-existential-info start end)) ;; put current sequent into hash (if it is not there yet) (unless (gethash current-sequent-id proof-tree-sequent-hash) (puthash current-sequent-id proof-state proof-tree-sequent-hash)) (proof-tree-register-existentials proof-state current-sequent-id - current-sequent-text)) - - ;; no current goal found, maybe the proof has been finished? - (goto-char start) - (if (proof-re-search-forward proof-tree-proof-finished-regexp end t) - (progn - (proof-tree-send-proof-finished - proof-state proof-name cmd-string - cheated-flag existential-info)))))) + current-sequent-text)))))) (defun proof-tree-handle-navigation (proof-info) "Handle a navigation command. @@ -901,7 +910,7 @@ The delayed output of the navigation command is in the region (proof-tree-send-switch-goal proof-state proof-name current-id))))) -(defun proof-tree-handle-proof-command (cmd proof-info) +(defun proof-tree-handle-proof-command (old-proof-marker cmd proof-info) "Display current goal in prooftree unless CMD should be ignored." ;; (message "PTHPC") (let ((proof-state (car proof-info)) @@ -913,7 +922,8 @@ The delayed output of the navigation command is in the region (proof-string-match proof-tree-navigation-command-regexp cmd-string)) (proof-tree-handle-navigation proof-info) - (proof-tree-handle-proof-progress cmd-string proof-info))) + (proof-tree-handle-proof-progress old-proof-marker + cmd-string proof-info))) (setq proof-tree-last-state (car proof-info)))) (defun proof-tree-handle-undo (proof-info) @@ -989,13 +999,19 @@ The delayed output is in the region sequent-text))))))) -(defun proof-tree-handle-delayed-output (cmd flags span) +(defun proof-tree-handle-delayed-output (old-proof-marker cmd flags span) "Process delayed output for prooftree. This function is the main entry point of the Proof General prooftree support. It examines the delayed output in order to take appropriate actions and maintains the internal state. -All arguments are (former) fields of the `proof-action-list' +The delayed output to handle is in the region +\[proof-shell-delayed-output-start, proof-shell-delayed-output-end]. +Urgent messages might be before that, following OLD-PROOF-MARKER, +which contains the position of `proof-marker', before the next +command was sent to the proof assistant. + +All other arguments are (former) fields of the `proof-action-list' entry that is now finally retired. CMD is the command, FLAGS are the flags and SPAN is the span." ;; (message "PTHDO cmd %s flags %s span %s-%s" cmd flags @@ -1035,7 +1051,8 @@ the flags and SPAN is the span." (when current-proof-name ;; we are inside a proof: display something (proof-tree-ensure-running) - (proof-tree-handle-proof-command cmd proof-info))))))) + (proof-tree-handle-proof-command old-proof-marker + cmd proof-info))))))) ;; -- cgit v1.2.3