diff options
Diffstat (limited to 'coq/coq-syntax.el')
| -rw-r--r-- | coq/coq-syntax.el | 233 |
1 files changed, 155 insertions, 78 deletions
diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el index 5844be74..bb32fc52 100644 --- a/coq/coq-syntax.el +++ b/coq/coq-syntax.el @@ -1,27 +1,35 @@ -;; coq-syntax.el Font lock expressions for Coq -;; Copyright (C) 1997-2007, 2009 LFCS Edinburgh. +;;; coq-syntax.el --- Font lock expressions for Coq + +;; This file is part of Proof General. + +;; Portions © Copyright 1994-2012 David Aspinall and University of Edinburgh +;; Portions © Copyright 2003, 2012, 2014 Free Software Foundation, Inc. +;; Portions © Copyright 2001-2017 Pierre Courtieu +;; Portions © Copyright 2010, 2016 Erik Martin-Dorel +;; Portions © Copyright 2011-2013, 2016-2017 Hendrik Tews +;; Portions © Copyright 2015-2017 Clément Pit-Claudel + ;; Authors: Thomas Kleymann, Healfdene Goguen, Pierre Courtieu -;; License: GPL (GNU GENERAL PUBLIC LICENSE) ;; Maintainer: Pierre Courtieu <Pierre.Courtieu@cnam.fr> -;; coq-syntax.el,v 11.13 2013/07/10 14:59:08 pier Exp +;; License: GPL (GNU GENERAL PUBLIC LICENSE) + +;;; Commentary: +;; + +;;; Code: (require 'proof-syntax) (require 'proof-utils) ; proof-locate-executable (require 'coq-db) +(require 'span) -(eval-when-compile - (require 'span) - (defvar coq-goal-command-regexp nil) - (defvar coq-save-command-regexp-strict nil)) - - - ;;; keyword databases +;;; keyword databases (defcustom coq-user-tactics-db nil - "User defined tactic information. See `coq-syntax-db' for -syntax. It is not necessary to add your own tactics here (it is not -needed by the synchronizing/backtracking system). You may however do + "User defined tactic information. See `coq-syntax-db' for syntax. +It is not necessary to add your own tactics here (it is not +needed by the synchronizing/backtracking system). You may however do so for the following reasons: 1 your tactics will be colorized by font-lock @@ -36,10 +44,10 @@ so for the following reasons: (defcustom coq-user-commands-db nil - "User defined command information. See `coq-syntax-db' for - syntax. It is not necessary to add your own commands here (it is not - needed by the synchronizing/backtracking system). You may however do - so for the following reasons: + "User defined command information. See `coq-syntax-db' for syntax. +It is not necessary to add your own commands here (it is not +needed by the synchronizing/backtracking system). You may however do +so for the following reasons: 1 your commands will be colorized by font-lock @@ -52,10 +60,10 @@ so for the following reasons: :group 'coq) (defcustom coq-user-tacticals-db nil - "User defined tactical information. See `coq-syntax-db' for - syntax. It is not necessary to add your own commands here (it is not - needed by the synchronizing/backtracking system). You may however do - so for the following reasons: + "User defined tactical information. See `coq-syntax-db' for syntax. +It is not necessary to add your own commands here (it is not +needed by the synchronizing/backtracking system). You may however do +so for the following reasons: 1 your commands will be colorized by font-lock @@ -68,10 +76,10 @@ so for the following reasons: :group 'coq) (defcustom coq-user-solve-tactics-db nil - "User defined closing tactics. See `coq-syntax-db' for - syntax. It is not necessary to add your own commands here (it is not - needed by the synchronizing/backtracking system). You may however do - so for the following reasons: + "User defined closing tactics. See `coq-syntax-db' for syntax. +It is not necessary to add your own commands here (it is not +needed by the synchronizing/backtracking system). You may however do +so for the following reasons: 1 your commands will be colorized by font-lock @@ -85,10 +93,10 @@ so for the following reasons: (defcustom coq-user-cheat-tactics-db nil "User defined closing tactics BY CHEATING (ex: admit). - See `coq-syntax-db' for syntax. It is not necessary to add your - own commands here (it is not needed by the - synchronizing/backtracking system). You may however do so for - the following reasons: +See `coq-syntax-db' for syntax. It is not necessary to add your +own commands here (it is not needed by the +synchronizing/backtracking system). You may however do so for +the following reasons: 1 your commands will be colorized by font-lock @@ -103,10 +111,10 @@ so for the following reasons: (defcustom coq-user-reserved-db nil - "User defined reserved keywords information. See `coq-syntax-db' for - syntax. It is not necessary to add your own commands here (it is not - needed by the synchronizing/backtracking system). You may however do - so for the following reasons: + "User defined reserved keywords information. See `coq-syntax-db' for syntax. +It is not necessary to add your own commands here (it is not +needed by the synchronizing/backtracking system). You may however do +so for the following reasons: 1 your commands will be colorized by font-lock @@ -320,7 +328,7 @@ so for the following reasons: ("suff" "suff" "suff # : #" t "suff") ) coq-user-tactics-db) - "Coq tactics information list. See `coq-syntax-db' for syntax. " + "Coq tactics information list. See `coq-syntax-db' for syntax." ) ;; user shortcuts are prioritized by being put at the end @@ -437,7 +445,7 @@ so for the following reasons: ("Local Coercion" nil "Local Coercion @{id} : @{typ1} >-> @{typ2}." t "Local\\s-+Coercion") ("Coercion" "coerc" "Coercion @{id} : @{typ1} >-> @{typ2}." t "Coercion") ) - "Coq declaration keywords information list. See `coq-syntax-db' for syntax." + "Coq declaration keywords information list. See `coq-syntax-db' for syntax." ) (defvar coq-defn-db @@ -495,8 +503,9 @@ so for the following reasons: ("Scheme Induction" "sci" "Scheme @{name} := Induction for # Sort #." t) ("Scheme Minimality" "scm" "Scheme @{name} := Minimality for # Sort #." t) ("Structure" "str" "Structure # : # := {\n# : #;\n# : # }" t "Structure") + ("Variant" "varv" "Variant # : # := # : #." t "Variant") ) - "Coq definition keywords information list. See `coq-syntax-db' for syntax. " + "Coq definition keywords information list. See `coq-syntax-db' for syntax." ) ;; modules and section are indented like goal starters @@ -521,7 +530,7 @@ so for the following reasons: ("Instance goal" "instg" "Instance #:#.\n#\nDefined." t);; careful ("Lemma" "l" "Lemma # : #.\nProof.\n#\nQed." t "Lemma") ("Program Lemma" "pl" "Program Lemma # : #.\nProof.\n#\nQed." t "Program\\s-+Lemma") - ("Proposition" "l" "Proposition # : #.\nProof.\n#\nQed." t "Proposition") + ("Proposition" "pr" "Proposition # : #.\nProof.\n#\nQed." t "Proposition") ("Module! (interactive)" nil "Module # : #.\n#\nEnd #." nil nil coq-insert-section-or-module) ("Module Type" "mti" "Module Type #.\n#\nEnd #." t "Module\\s-+Type") ; careful ("Module :" "moi" "Module # : #.\n#\nEnd #." t "Module") ; careful @@ -534,7 +543,7 @@ so for the following reasons: ("Obligations" "obls" "Obligations #.\n#\nQed." nil "Obligations") ("Next Obligation" "nobl" "Next Obligation.\n#\nQed." t "Next Obligation") ) - "Coq goal starters keywords information list. See `coq-syntax-db' for syntax. " + "Coq goal starters keywords information list. See `coq-syntax-db' for syntax." ) ;; TODO: dig other queries from the refman. @@ -563,7 +572,7 @@ so for the following reasons: ("Test" nil "Test" nil "Test" nil t) ; let us not highlight all possible options for Test ("Timeout" nil "Timeout" nil "Timeout") ) - "Coq queries command, that deserve a separate menu for sending them to coq without insertion. " + "Coq queries command, that deserve a separate menu for sending them to coq without insertion." ) ;; command that are not declarations, definition or goal starters @@ -706,22 +715,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") @@ -762,11 +775,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") @@ -907,7 +920,7 @@ so for the following reasons: (append coq-decl-db coq-defn-db coq-goal-starters-db coq-queries-commands-db coq-other-commands-db coq-ssreflect-commands-db coq-user-commands-db) - "Coq all commands keywords information list. See `coq-syntax-db' for syntax. " + "Coq all commands keywords information list. See `coq-syntax-db' for syntax." ) @@ -930,7 +943,7 @@ so for the following reasons: ("match with 4" "m4" "match # with\n| # => #\n| # => #\n| # => #\n| # => #\nend") ("match with 5" "m5" "match # with\n| # => #\n| # => #\n| # => #\n| # => #\n| # => #\nend") ) - "Coq terms keywords information list. See `coq-syntax-db' for syntax. " + "Coq terms keywords information list. See `coq-syntax-db' for syntax." ) @@ -974,8 +987,8 @@ so for the following reasons: ;; (la fonction vernac_declare_module dans toplevel/vernacentries) (defun coq-count-match (regexp strg) - "Count the number of (maximum, non overlapping) matching substring - of STRG matching REGEXP. Empty match are counted once." + "Count the number of max. non-overlapping substring of STRG matching REGEXP. +Empty matches are counted once." (let ((nbmatch 0) (str strg)) (while (and (proof-string-match regexp str) (not (string-equal str ""))) (incf nbmatch) @@ -1004,8 +1017,8 @@ Used by `coq-goal-command-p'" ;; unused anymore (for good) (defun coq-goal-command-str-p (str) - "Decide syntactically whether STR is a goal start or not. Use -`coq-goal-command-p' on a span instead if possible." + "Decide syntactically whether STR is a goal start or not. +Use ‘coq-goal-command-p’ on a span instead if possible." (let* ((match (coq-count-match "\\_<match\\_>" str)) (with (- (coq-count-match "\\_<with\\_>" str) (coq-count-match "\\_<with\\s-+signature\\_>" str))) (letwith (+ (coq-count-match "\\_<let\\_>" str) (- with match))) @@ -1030,7 +1043,6 @@ Used by `coq-goal-command-p'" ;; to look at Modules and section (actually indentation will still ;; need it) (defun coq-goal-command-p (span) - "see `coq-goal-command-p'" (or (span-property span 'goalcmd) ;; module and section starts are detected here (let ((str (or (span-property span 'cmd) ""))) @@ -1052,7 +1064,7 @@ It is used: (defun coq-save-command-p (span str) - "Decide whether argument is a Save command or not" + "Decide whether argument is a Save command or not." (or (proof-string-match coq-save-command-regexp-strict str) (and (proof-string-match "\\`Proof\\_>" str) (not (proof-string-match "\\`Proof\\s-*\\(\\.\\|\\_<with\\_>\\|\\_<using\\_>\\)" str))))) @@ -1203,11 +1215,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_\\)*") @@ -1219,12 +1237,12 @@ It is used: (concat paren "\\s-*\\(" coq-ids "\\)\\s-*" end)) (defcustom coq-variable-highlight-enable t - "Activates partial bound variable highlighting" + "Activates partial bound variable highlighting." :type 'boolean :group 'coq) (defcustom coq-symbol-highlight-enable nil - "Activates partial bound variable highlighting" + "Activates symbol highlighting." :type 'boolean :group 'coq) @@ -1336,12 +1354,71 @@ It is used: (proof-zap-commas)))) -;; ", " is for multiple hypothesis displayed in v8.5. If more than -;; 1 space this is a hypothesis displayed in the middle of a line (> v8.5) -;; "^ " is for goals in debug mode. +;; ", " is for multiple hypothesis displayed in v8.5. +;; exactly no space after start of line = hyps names in +;; Search results (and when we get a more compact display of hyps) +;; exactly 2 spaces at start of line = is for normal goal display at +;; start of line +;; exactly 3 spaces at start of line = hyps on the same line (Set +;; Printing Compact Goals". +;; If more than 3 spaces: not a hyp. +;; we used to have: "^ " for goals in debug mode but it does not seem +;; necessary anymore. (defvar coq-hyp-name-in-goal-or-response-regexp - "\\(^\\|^ \\|^ \\|[^^ ] ? \\)\\(\\(?:[^\n :(),=]\\|, \\)+ *\\(?::[ \n]\\|,$\\)\\)" - "regexp matching hypothesis names in goal or response buffer") + "\\(?:\\(?1:^\\)\\|\\(?1:^ \\)\\|\\(?:[^ ] \\)\\(?1: \\)\\)\\(?2:\\(?:[^\n :(),=]\\|, \\)+\\)\\(?: *:=?[ \n]\\|,$\\)" + "Regexp matching hypothesis names in goal or response buffer. +Subexpr 2 contains the real name of the function. +Subexpr 1 contains the prefix context (spaces mainly) that is not +part of another hypothesis.") + +; Matches the end of the last hyp, before the ======... separator. +(defvar coq-hyp-name-or-goalsep-in-goal-or-response-regexp + (concat coq-hyp-name-in-goal-or-response-regexp "\\|\\(?1:^\\s-+========\\)")) + +(defun coq-find-first-hyp () + (with-current-buffer proof-goals-buffer + (save-excursion + (goto-char (point-min)) + (search-forward-regexp coq-hyp-name-in-goal-or-response-regexp nil t) + (match-beginning 2)))) + +(defun coq-detect-hyps-positions (buf &optional limit) + "Detect all hypotheses displayed in buffer BUF and returns positions. +5 positions are created for each hyp: (begcross beghypname endhypname beg end)." + (with-current-buffer buf + (save-excursion + (goto-char (point-min)) + (let ((res '())) + (goto-char (point-min)) + (while (search-forward-regexp coq-hyp-name-in-goal-or-response-regexp limit t) + (let* ((str (replace-regexp-in-string "\\`[ \r\n\t]+\\|[ \r\n\t]+\\'" "" (match-string 2) t t)) + (beghypname (match-beginning 2)) + (beg (match-end 0)) + (begcross (match-beginning 1)) + (endhypname (match-end 2)) + (splitstr (split-string str ",\\|,$\\|:" t)) ; 4th arg of split-string errors in emacs24 + (end (save-excursion ; looking for next hyp and return its leftest part + (search-forward-regexp coq-hyp-name-or-goalsep-in-goal-or-response-regexp nil t) + (goto-char (match-beginning 1)) + ;; if previous is a newline, don't include it i the overklay + (when (looking-back "\\s-") (goto-char (- (point) 1))) + (point)))) + ; if several hyp names, we name the overlays with the first hyp name + (setq res + (cons + (cons (mapcar (lambda (s) (substring-no-properties s)) splitstr) + (list begcross beghypname endhypname beg end)) + res)))) + res)))) + +;; Don't look at the conclusion of the goal +(defun coq-detect-hyps-positions-in-goals () + (with-current-buffer proof-goals-buffer + (goto-char (point-min)) + (coq-detect-hyps-positions + proof-goals-buffer + (if (search-forward-regexp "==========" nil t) (point) nil)))) + ;; We define a slightly different set of keywords for response buffer. |