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 --- coq/coq.el | 19 ++++++++++++------- 1 file changed, 12 insertions(+), 7 deletions(-) (limited to 'coq') diff --git a/coq/coq.el b/coq/coq.el index 89a380ce..b0906f65 100644 --- a/coq/coq.el +++ b/coq/coq.el @@ -190,7 +190,8 @@ See also `coq-hide-additional-subgoals'." :group 'coq-proof-tree) (defcustom coq-navigation-command-regexp - "^\\(Focus\\)\\|\\(Unfocus\\)" + (concat "^\\(\\(Focus\\)\\|\\(Unfocus\\)\\|" + "\\(\\+\\)\\|\\(-\\)\\|\\(\\*\\)\\|\\({\\)\\|\\(}\\)\\)") "Regexp for `proof-tree-navigation-command-regexp'." :type 'regexp :group 'coq-proof-tree) @@ -203,8 +204,8 @@ See also `coq-hide-additional-subgoals'." (defcustom coq-proof-tree-current-goal-regexp (concat "^[0-9]+ \\(?:focused \\)?subgoal\\(?:s\\)?" - "\\(?: (unfocused: [0-9]+)\\)?\\(?:\\s-*, subgoal 1\\)? " - "(ID \\([0-9]+\\))\n\\s-*\n\\(\\(?:.+\n\\)*\\)\\(?:\n\\|$\\)") + "\\(?: (unfocused: [-0-9]+)\\)?\\(?:\\s-*, subgoal 1\\)? " + "(ID \\([0-9]+\\))\n\\s-*\n\\(\\(?: .*\n\\)+\\)\\(?:\n\\|$\\)") "Regexp for `proof-tree-current-goal-regexp'." :type 'regexp :group 'coq-proof-tree) @@ -244,9 +245,13 @@ See also `coq-hide-additional-subgoals'." :type 'regexp :group 'coq-proof-tree) -(defcustom coq-proof-tree-proof-finished-regexp - "^\\(?:Proof completed\\)\\|\\(?:No more subgoals\\)\\." - "Regexp for `proof-tree-proof-finished-regexp'." +(defcustom coq-proof-tree-branch-finished-regexp + (concat "^\\(\\(?:Proof completed\\.\\)\\|\\(?:No more subgoals\\.\\)\\|" + "\\(No more subgoals but non-instantiated " + "existential variables:\\)\\|" + "\\(This subproof is complete, but there are " + "still unfocused goals.\\)\\)") + "Regexp for `proof-tree-branch-finished-regexp'." :type 'regexp :group 'coq-proof-tree) @@ -1195,7 +1200,7 @@ flag Printing All set." coq-proof-tree-existentials-state-end-regexp proof-tree-additional-subgoal-ID-regexp coq-proof-tree-additional-subgoal-ID-regexp - proof-tree-proof-finished-regexp coq-proof-tree-proof-finished-regexp + proof-tree-branch-finished-regexp coq-proof-tree-branch-finished-regexp proof-tree-extract-instantiated-existentials 'coq-extract-instantiated-existentials proof-tree-show-sequent-command 'coq-show-sequent-command -- cgit v1.2.3