diff options
| author | Christophe Raffalli | 2000-12-22 14:03:10 +0000 |
|---|---|---|
| committer | Christophe Raffalli | 2000-12-22 14:03:10 +0000 |
| commit | b63dd74e45d33d5493906b3c8caf00d0b84d8146 (patch) | |
| tree | 3f00fcdbe261dd874cce7d7309f3b94e3b2c225f /phox/phox.el | |
| parent | 7fd3934a7915b9dcc7930d59c592089e1357309d (diff) | |
*** empty log message ***
Diffstat (limited to 'phox/phox.el')
| -rw-r--r-- | phox/phox.el | 51 |
1 files changed, 37 insertions, 14 deletions
diff --git a/phox/phox.el b/phox/phox.el index 87c1cdef..e0274faf 100644 --- a/phox/phox.el +++ b/phox/phox.el @@ -111,21 +111,44 @@ proof-comment-start "(*" proof-comment-end "*)" proof-state-command "goals." - proof-goal-command-regexp "goal\\|prop\\(osition\\)?\\|em\\(ma\\)?\\|fact\\|cor\\(ollary\\)?\\|theo\\(rem\\)?" - proof-save-command-regexp "save" - proof-goal-with-hole-regexp (concat - "\\(prop\\(osition\\)?\\|lem\\(ma\\)?\\|fact\\|cor\\(ollary\\)?\\|theo\\(rem\\)?\\)" - phox-strict-comments-regexp - phox-ident-regexp) - proof-goal-with-hole-result 13 - proof-save-with-hole-regexp (concat - "save" - phox-strict-comments-regexp - phox-ident-regexp) - proof-save-with-hole-result 8 - proof-ignore-for-undo-count "constraints\\|flag\\|goals\\|print\\(_sort\\)?\\|eshow\\|search\\|priority\\|depend" + proof-goal-command-regexp + (concat + "^" + phox-comments-regexp + "\\(goal\\|prop\\(osition\\)?\\|em\\(ma\\)?\\|fact\\|cor\\(ollary\\)?\\|theo\\(rem\\)?\\)") + proof-save-command-regexp + (concat + "^" + phox-comments-regexp + "save") + proof-goal-with-hole-regexp + (concat + "^" + phox-comments-regexp + "\\(prop\\(osition\\)?\\|lem\\(ma\\)?\\|fact\\|cor\\(ollary\\)?\\|theo\\(rem\\)?\\)" + phox-strict-comments-regexp + phox-ident-regexp) + proof-goal-with-hole-result 16 + proof-save-with-hole-regexp + (concat + "^" + +phox-comments-regexp + "save" + phox-strict-comments-regexp + phox-ident-regexp) + proof-save-with-hole-result 11 + proof-ignore-for-undo-count + (concat + "^" + phox-comments-regexp + "\\(constraints\\|flag\\|goals\\|print\\(_sort\\)?\\|eshow\\|search\\|priority\\|depend\\)") + proof-non-undoables-regexp + (concat + "^" + phox-comments-regexp + "\\(undo\\|abort\\)") proof-shell-error-regexp "^\\([^ \n\t\r]* \\)?\\(\\(e\\|E\\)rror\\)\\|\\(\\(f\\|F\\)ailure\\)" - proof-non-undoables-regexp "undo\\|abort" proof-goal-command "goal %s." proof-save-command "save %s." proof-kill-goal-command "abort." |