diff options
| author |  Pierre Courtieu <courtieu@lri.fr> | 2000-09-29 12:17:10 +0000 |
|---|---|---|
| committer | Pierre Courtieu <courtieu@lri.fr> | 2000-09-29 12:17:10 +0000 |
| commit | 63000d541743e839c62be74af1158f241124ba42 (patch) | |
| tree | 5959625fddb7f5a74ee272f7e4095d3dcb486dd8 | |
| parent | ef4c4bdd09a577e40f3e5e31cb78349e60ce48f1 (diff) | |
Added Uncaught exception errors in coq-error-regexp.
| -rw-r--r-- | coq/coq-syntax.el | 2 | ||||
| -rw-r--r-- | coq/coq.el | 4 | ||||
| -rw-r--r-- | coq/coqtags | 2 | ||||
| -rw-r--r-- | coq/x-symbol-coq.el | 12 | ||||
| -rw-r--r-- | lego/legotags | 2 |
5 files changed, 15 insertions, 7 deletions
diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el index 25880fed..5e559ea9 100644 --- a/coq/coq-syntax.el +++ b/coq/coq-syntax.el @@ -257,7 +257,7 @@ "Punctuation Symbols used by Coq") ;; ----- regular expressions -(defvar coq-error-regexp "^\\(Error\\|Discarding\\|Syntax error\\|System Error\\|Anomaly\\)" +(defvar coq-error-regexp "^\\(Error\\|Discarding\\|Syntax error\\|System Error\\|Anomaly\\|Uncaught exception\\)" "A regular expression indicating that the Coq process has identified an error.") @@ -91,7 +91,7 @@ (defvar coq-outline-regexp (concat "(\\*\\|" (proof-ids-to-regexp '( -"Tactic" "Axiom" "Parameter" "Parameters" "Variable" "Variables" "Syntax" "Grammar" "Syntactic" "Load" "Require" "Hint" "Hints" "Correctness" "Section" "Chapter" "Goal" "Lemma" "Theorem" "Fact" "Remark" "Record" "Inductive" "Mutual" "Definition" "Fixpoint" "Save" "Qed" "Defined")))) +"Tactic" "Axiom" "Parameter" "Parameters" "Variable" "Variables" "Syntax" "Grammar" "Syntactic" "Load" "Require" "Hint" "Hints" "Hypothesis" "Correctness" "Section" "Chapter" "Goal" "Lemma" "Theorem" "Fact" "Remark" "Record" "Inductive" "Mutual" "Definition" "Fixpoint" "Save" "Qed" "Defined" "End" "Coercion")))) (defvar coq-outline-heading-end-regexp "\\*\)\n\\|\\.\n") @@ -103,7 +103,7 @@ (defconst coq-undoable-commands-regexp (proof-ids-to-regexp (append coq-tactics coq-keywords-undoable-commands))) -(defconst coq-not-undoable-commands-regexp (proof-ids-to-regexp coq-keywords-not-undoable-commands)) +(defconst coq-not-undoable-commands-regexp (proof-ids-to-regexp (append coq-keywords-decl coq-keywords-not-undoable-commands))) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; Derived modes - they're here 'cos they define keymaps 'n stuff ;; diff --git a/coq/coqtags b/coq/coqtags index a166a5a9..1088c24a 100644 --- a/coq/coqtags +++ b/coq/coqtags @@ -1,4 +1,4 @@ -#!/usr/local/bin/perl +#!/usr/bin/perl # # $Id$ # diff --git a/coq/x-symbol-coq.el b/coq/x-symbol-coq.el index d74ab428..99d7588b 100644 --- a/coq/x-symbol-coq.el +++ b/coq/x-symbol-coq.el @@ -6,9 +6,17 @@ ;; (defvar x-symbol-coq-symbol-table - '((perpendicular () "False" "\\<bottom>") + '((arrowup () "\\+" "\\<uparrow>") + (arrowdown () "\\-" "\\<downarrow>") + (angleleft () "\\<\\" "\\<langle>") + (angleright () "\\>\\" "\\<rangle>") + (circledot () "\\dot\\" "\\<odot>") + (reflexsubset () "\\incl\\" "\\<rset>") + (element () "\\in\\" "\\<in>") + (emptyset () "emptyset" "\\<emptyset>") + (perpendicular () "False" "\\<bottom>") (top () "True" "\\<top>") - (notsign () "~" "\\<not>") + (notsign () "~" "\\<not>") (longarrowright () "->" "\\<longrightarrow>") (logicaland () "/\\" "\\<and>") (logicalor () "\\/" "\\<or>") diff --git a/lego/legotags b/lego/legotags index a5c0f825..d32547ae 100644 --- a/lego/legotags +++ b/lego/legotags @@ -1,4 +1,4 @@ -#!/usr/local/bin/perl +#!/usr/bin/perl # # $Id$ # |