diff options
| author |  Christophe Raffalli <christophe.raffalli@univ-savoie.fr> | 2001-06-22 08:48:11 +0000 |
|---|---|---|
| committer | Christophe Raffalli <christophe.raffalli@univ-savoie.fr> | 2001-06-22 08:48:11 +0000 |
| commit | a90649cb9d19bb0c20916c411a8146743689d626 (patch) | |
| tree | dc78a9c656488b2375c775adc074b733d9cfcf00 /phox | |
| parent | fcaea3af83c23259b401e1f50c657abeef9d00bc (diff) | |
*** empty log message ***
Diffstat (limited to 'phox')
| -rw-r--r-- | phox/phox.el | 19 |
1 files changed, 17 insertions, 2 deletions
diff --git a/phox/phox.el b/phox/phox.el index 1e584d57..12d4e305 100644 --- a/phox/phox.el +++ b/phox/phox.el @@ -108,7 +108,7 @@ proof-comment-end "*)" proof-state-command "goals." proof-goal-command-regexp - "\\`\\(goal\\|pro\\(p\\(osition\\)?\\|ve_claim\\)\\|lem\\(ma\\)?\\|fact\\|cor\\(ollary\\)?\\|theo\\(rem\\)?\\)" + "\\`\\(goal[ \t\n\r]\\|pro\\(p\\(osition\\)?\\|ve_claim\\)\\|lem\\(ma\\)?\\|fact\\|cor\\(ollary\\)?\\|theo\\(rem\\)?\\)" proof-save-command-regexp "\\`save" proof-goal-with-hole-regexp (concat @@ -147,10 +147,25 @@ proof-shell-prompt-pattern "\\(>phox> \\)\\|\\(%phox% \\)" proof-shell-annotated-prompt-regexp "\\(>phox> \\)\\|\\(%phox% \\)" proof-shell-interrupt-regexp "Interrupt" - proof-shell-start-goals-regexp "^\\(Here are the goal\\)\\|\\([0-9]+ goal\\(s?\\) created\\)" + proof-shell-start-goals-regexp "^\\(Here \\(are\\|is\\) the goal\\)\\|\\([0-9]* goals\\? created\\)" proof-shell-quit-cmd "quit." proof-shell-restart-cmd "restart." proof-shell-proof-completed-regexp "^.*^proved" + ;; proof-shell-first-special-char ?\371 + ;; proof-shell-wakeup-char ?\371 + ;; proof-shell-start-char ?\371 + ;; proof-shell-end-char ?\372 + ;; proof-shell-goal-char ?\373 + ;; proof-shell-field-char ?\374 + ;; proof-shell-eager-annotation-start "\376" + ;; proof-shell-eager-annotation-start-length 1 + ;; proof-shell-eager-annotation-end "\377" +; proof-shell-annotated-prompt-regexp "Lego> \371" +; proof-shell-result-start "\372 Pbp result \373" +; proof-shell-result-end "\372 End Pbp result \373" +; proof-shell-start-goals-regexp "\372 Start of Goals \373" +; proof-shell-end-goals-regexp "\372 End of Goals \373" +; proof-shell-pre-sync-init-cmd "Configure AnnotateOn;" )) |