diff options
Diffstat (limited to 'coq')
| -rw-r--r-- | coq/coq-abbrev.el | 4 | ||||
| -rw-r--r-- | coq/coq-smie.el | 2 | ||||
| -rw-r--r-- | coq/coq-syntax.el | 56 | ||||
| -rw-r--r-- | coq/coq.el | 6 |
4 files changed, 43 insertions, 25 deletions
diff --git a/coq/coq-abbrev.el b/coq/coq-abbrev.el index 30ec60c4..79231ad9 100644 --- a/coq/coq-abbrev.el +++ b/coq/coq-abbrev.el @@ -289,10 +289,14 @@ It was constructed with `proof-defstringset-fn'.") ["Unset Printing Implicit" coq-unset-printing-implicit t] ["Set Printing Coercions" coq-set-printing-coercions t] ["Unset Printing Coercions" coq-unset-printing-coercions t] + ["Set Printing Compact Contexts" coq-set-printing-implicit t] + ["Unset Printing Compact Contexts" coq-unset-printing-implicit t] ["Set Printing Synth" coq-set-printing-synth t] ["Unset Printing Synth" coq-unset-printing-synth t] ["Set Printing Universes" coq-set-printing-universes t] ["Unset Printing Universes" coq-unset-printing-universes t] + ["Set Printing Unfocused" coq-set-printing-unfocused t] + ["Unset Printing Unfocused" coq-unset-printing-unfocused t] ["Set Printing Wildcards" coq-set-printing-wildcards t] ["Unset Printing Wildcards" coq-unset-printing-wildcards t] ["Set Printing Width" coq-ask-adapt-printing-width-and-show t]) diff --git a/coq/coq-smie.el b/coq/coq-smie.el index c488e73f..ce386c1f 100644 --- a/coq/coq-smie.el +++ b/coq/coq-smie.el @@ -373,7 +373,7 @@ The point should be at the beginning of the command name." (defun coq-smie-forward-token () - (let ((tok (coq-forward-token-fast-nogluing-dot-friends))) + (let ((tok (smie-default-forward-token))) (cond ;; @ may be ahead of an id, it is part of the id. ((and (equal tok "@") (looking-at "[[:alpha:]_]")) diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el index fc0e547a..156d39e1 100644 --- a/coq/coq-syntax.el +++ b/coq/coq-syntax.el @@ -701,22 +701,26 @@ so for the following reasons: ("Set Nonrecursive Elimination Schemes" nil "Set Nonrecursive Elimination Schemes" t "Set Nonrecursive\\s-+Elimination\\s-+Schemes") ("Set Parsing Explicit" nil "Set Parsing Explicit" t "Set Parsing\\s-+Explicit") ("Set Primitive Projections" nil "Set Primitive Projections" t "Set Primitive\\s-+Projections") - ("Set Printing All" nil "Set Printing All" t "Set Printing\\s-+All") - ("Set Printing Coercions" nil "Set Printing Coercions" t "Set Printing\\s-+Coercions") - ("Set Printing Depth" nil "Set Printing Depth" t "Set Printing\\s-+Depth") - ("Set Printing Existential Instances" nil "Set Printing Existential Instances" t "Set Printing\\s-+Existential\\s-+Instances") - ("Set Printing Implicit" nil "Set Printing Implicit" t "Set Printing\\s-+Implicit") - ("Set Printing Implicit Defensive" nil "Set Printing Implicit Defensive" t "Set Printing\\s-+Implicit\\s-+Defensive") - ("Set Printing Matching" nil "Set Printing Matching" t "Set Printing\\s-+Matching") - ("Set Printing Notations" nil "Set Printing Notations" t "Set Printing\\s-+Notations") - ("Set Printing Primitive Projection Compatibility" nil "Set Printing Primitive Projection Compatibility" t "Set Printing\\s-+Primitive\\s-+Projection\\s-+Compatibility") - ("Set Printing Primitive Projection Parameters" nil "Set Printing Primitive Projection Parameters" t "Set Printing\\s-+Primitive\\s-+Projection\\s-+Parameters") - ("Set Printing Projections" nil "Set Printing Projections" t "Set Printing\\s-+Projections") - ("Set Printing Records" nil "Set Printing Records" t "Set Printing\\s-+Records") - ("Set Printing Synth" nil "Set Printing Synth" t "Set Printing\\s-+Synth") - ("Set Printing Universes" nil "Set Printing Universes" t "Set Printing\\s-+Universes") - ("Set Printing Width" nil "Set Printing Width" t "Set Printing\\s-+Width") - ("Set Printing Wildcard" nil "Set Printing Wildcard" t "Set Printing\\s-+Wildcard") + ("Set Printing All" nil "Set Printing All" t "Set\\s-+Printing\\s-+All") + ("Set Printing Coercions" nil "Set Printing Coercions" t "Set\\s-+Printing\\s-+Coercions") + ("Set Printing Compact Contexts" nil "Set Printing Compact Contexts" t "Set\\s-+Printing\\s-+Compact\\s-+Contexts") + ("Set Printing Depth" nil "Set Printing Depth" t "Set\\s-+Printing\\s-+Depth") + ("Set Printing Existential Instances" nil "Set Printing Existential Instances" t "Set\\s-+Printing\\s-+Existential\\s-+Instances") + ("Set Printing Goal Tags" nil "Set Printing Goal Tags" t "Set\\s-+Printing\\s-+Goal\\s-+Tags") + ("Set Printing Goal Names" nil "Set Printing Goal Names" t "Set\\s-+Printing\\s-+Goal\\s-+Names") + ("Set Printing Implicit" nil "Set Printing Implicit" t "Set\\s-+Printing\\s-+Implicit") + ("Set Printing Implicit Defensive" nil "Set Printing Implicit Defensive" t "Set\\s-+Printing\\s-+Implicit\\s-+Defensive") + ("Set Printing Matching" nil "Set Printing Matching" t "Set\\s-+Printing\\s-+Matching") + ("Set Printing Notations" nil "Set Printing Notations" t "Set\\s-+Printing\\s-+Notations") + ("Set Printing Primitive Projection Compatibility" nil "Set Printing Primitive Projection Compatibility" t "Set\\s-+Printing\\s-+Primitive\\s-+Projection\\s-+Compatibility") + ("Set Printing Primitive Projection Parameters" nil "Set Printing Primitive Projection Parameters" t "Set\\s-+Printing\\s-+Primitive\\s-+Projection\\s-+Parameters") + ("Set Printing Projections" nil "Set Printing Projections" t "Set\\s-+Printing\\s-+Projections") + ("Set Printing Records" nil "Set Printing Records" t "Set\\s-+Printing\\s-+Records") + ("Set Printing Synth" nil "Set Printing Synth" t "Set\\s-+Printing\\s-+Synth") + ("Set Printing Unfocused" nil "Set Printing Unfocused" t "Set\\s-+Printing\\s-+Unfocused") + ("Set Printing Universes" nil "Set Printing Universes" t "Set\\s-+Printing\\s-+Universes") + ("Set Printing Width" nil "Set Printing Width" t "Set\\s-+Printing\\s-+Width") + ("Set Printing Wildcard" nil "Set Printing Wildcard" t "Set\\s-+Printing\\s-+Wildcard") ("Set Program Mode" nil "Set Program Mode" t "Set Program\\s-+Mode") ("Set Proof Using Clear Unused" nil "Set Proof Using Clear Unused" t "Set Proof\\s-+Using\\s-+Clear\\s-+Unused") ("Set Record Elimination Schemes" nil "Set Record Elimination Schemes" t "Set Record\\s-+Elimination\\s-+Schemes") @@ -757,11 +761,11 @@ so for the following reasons: ("Set Silent" nil "Set Silent" t "Set Silent") ("Set Undo" nil "Set Undo" t "Set Undo") ("Set Search Blacklist" nil "Set Search Blacklist" t "Set Search\\s-+Blacklist") - ("Set Printing Coercion" nil "Set Printing Coercion" t "Set Printing\\s-+Coercion") - ("Set Printing If" nil "Set Printing If" t "Set Printing\\s-+If") - ("Set Printing Let" nil "Set Printing Let" t "Set Printing\\s-+Let") - ("Set Printing Record" nil "Set Printing Record" t "Set Printing\\s-+Record") - ("Set Printing Constructor" nil "Set Printing Constructor" t "Set Printing\\s-+Constructor") + ("Set Printing Coercion" nil "Set Printing Coercion" t "Set\\s-+Printing\\s-+Coercion") + ("Set Printing If" nil "Set Printing If" t "Set\\s-+Printing\\s-+If") + ("Set Printing Let" nil "Set Printing Let" t "Set\\s-+Printing\\s-+Let") + ("Set Printing Record" nil "Set Printing Record" t "Set\\s-+Printing\\s-+Record") + ("Set Printing Constructor" nil "Set Printing Constructor" t "Set\\s-+Printing\\s-+Constructor") ("Solve Obligations" "oblssolve" "Solve Obligations using #." t "Solve\\s-+Obligations") ("Local Strategy" nil "Local Strategy # [#]." t "Local\\s-+Strategy") ("Strategy" nil "Strategy # [#]." t "Strategy") @@ -1198,11 +1202,17 @@ It is used: (defvar coq-symbols-regexp (regexp-opt coq-symbols)) ;; ----- regular expressions -(defvar coq-error-regexp "^\\(Error:\\|Discarding pattern\\|Syntax error:\\|System Error:\\|User Error:\\|User error:\\|Anomaly[:.]\\|Toplevel input[,]\\)" +(defvar coq-error-regexp "^\\(In nested Ltac call\\|Error:\\|Discarding pattern\\|Syntax error:\\|System Error:\\|User Error:\\|User error:\\|Anomaly[:.]\\|Toplevel input[,]\\)" "A regexp indicating that the Coq process has identified an error.") +;; april2017: coq-8.7 removes special chars definitely and puts +;; <infomsg> and <warning> around all messages except errors. +;; We let our legacy regexp for some years and remove them, say, in 2020. (defvar coq-shell-eager-annotation-start - "\376\\|\\[Reinterning\\|Warning:\\|TcDebug \\|<infomsg>") + "\376\\|\\[Reinterning\\|Warning:\\|TcDebug \\|<infomsg>\\|<warning>") + +(defvar coq-shell-eager-annotation-end + "\377\\|done\\]\\|</infomsg>\\|</warning>\\|\\*\\*\\*\\*\\*\\*\\|) >") (defvar coq-id "\\(@\\|_\\|\\w\\)\\(\\w\\|\\s_\\)*") ;; Coq ca start an id with @ or _ (defvar coq-id-shy "\\(?:@\\|_\\|\\w\\)\\(?:\\w\\|\\s_\\)*") @@ -1362,6 +1362,10 @@ goal is redisplayed." (proof-definvisible coq-unset-printing-synth "Unset Printing Synth.") (proof-definvisible coq-set-printing-coercions "Set Printing Coercions.") (proof-definvisible coq-unset-printing-coercions "Unset Printing Coercions.") +(proof-definvisible coq-set-printing-compact-contexts "Set Printing Compact Contexts.") +(proof-definvisible coq-unset-printing-compact-contexts "Unset Printing Compact Contexts.") +(proof-definvisible coq-set-printing-unfocused "Set Printing Unfocused.") +(proof-definvisible coq-unset-printing-unfocused "Unset Printing Unfocused.") (proof-definvisible coq-set-printing-universes "Set Printing Universes.") (proof-definvisible coq-unset-printing-universes "Unset Printing Universes.") (proof-definvisible coq-set-printing-wildcards "Set Printing Wildcard.") @@ -1666,7 +1670,7 @@ Near here means PT is either inside or just aside of a comment." ;; want xml like tags, and I want them removed before warning display. ;; I want the same for errors -> pgip - proof-shell-eager-annotation-end "\377\\|done\\]\\|</infomsg>\\|\\*\\*\\*\\*\\*\\*\\|) >" ; done + proof-shell-eager-annotation-end coq-shell-eager-annotation-end ; done proof-shell-annotated-prompt-regexp coq-shell-prompt-pattern proof-shell-result-start "\372 Pbp result \373" proof-shell-result-end "\372 End Pbp result \373" |