aboutsummaryrefslogtreecommitdiffhomepage
path: root/coq
diff options
context:
space:
mode:
Diffstat (limited to 'coq')
-rw-r--r--coq/coq-abbrev.el19
-rw-r--r--coq/coq-autotest.el17
-rw-r--r--coq/coq-compile-common.el21
-rw-r--r--coq/coq-db.el34
-rw-r--r--coq/coq-indent.el55
-rw-r--r--coq/coq-local-vars.el19
-rw-r--r--coq/coq-par-compile.el22
-rw-r--r--coq/coq-par-test.el19
-rw-r--r--coq/coq-seq-compile.el21
-rw-r--r--coq/coq-smie.el58
-rw-r--r--coq/coq-syntax.el23
-rw-r--r--coq/coq-system.el25
-rw-r--r--coq/coq-unicode-tokens.el17
-rw-r--r--coq/coq.el34
14 files changed, 297 insertions, 87 deletions
diff --git a/coq/coq-abbrev.el b/coq/coq-abbrev.el
index 3a750472..5a555df5 100644
--- a/coq/coq-abbrev.el
+++ b/coq/coq-abbrev.el
@@ -1,10 +1,23 @@
;;; coq-abbrev.el --- coq abbrev table and menus for ProofGeneral mode
-;;
-;; Copyright (C) 1994-2009 LFCS Edinburgh.
+
+;; 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: Healfdene Goguen, Pierre Courtieu
+;; Maintainer: Pierre Courtieu <Pierre.Courtieu@cnam.fr>
+
;; License: GPL (GNU GENERAL PUBLIC LICENSE)
+
+;;; Commentary:
;;
-;; Maintainer: Pierre Courtieu <Pierre.Courtieu@cnam.fr>
+
+;;; Code:
(require 'proof)
(require 'coq-syntax)
diff --git a/coq/coq-autotest.el b/coq/coq-autotest.el
index e3c4b978..9126c2ae 100644
--- a/coq/coq-autotest.el
+++ b/coq/coq-autotest.el
@@ -1,9 +1,20 @@
-;; coq-autotest.el: tests of Coq Proof General (in progress).
+;;; coq-autotest.el --- tests of Coq Proof General (in progress).
+
+;; 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
+
+;;; Commentary:
;;
;; You can run these by issuing "make test.coq" in PG home dir.
;;
-;; $Id$
-;;
+
+;;; Code:
(eval-when-compile
(require 'cl))
diff --git a/coq/coq-compile-common.el b/coq/coq-compile-common.el
index f96b07da..c94cd8b7 100644
--- a/coq/coq-compile-common.el
+++ b/coq/coq-compile-common.el
@@ -1,17 +1,26 @@
-;; coq-compile-common.el --- common part of compilation feature
-;; Copyright (C) 1994-2012 LFCS Edinburgh.
+;;; coq-compile-common.el --- common part of compilation feature
+
+;; 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: Hendrik Tews
-;; License: GPL (GNU GENERAL PUBLIC LICENSE)
;; Maintainer: Hendrik Tews <hendrik@askra.de>
-;;
-;; $Id$
-;;
+
+;; License: GPL (GNU GENERAL PUBLIC LICENSE)
+
;;; Commentary:
;;
;; This file holds constants, options and some general functions for
;; the compilation feature.
;;
+;;; Code:
(require 'proof-shell)
(require 'coq-system)
diff --git a/coq/coq-db.el b/coq/coq-db.el
index 0d9c0a6e..dd9020d8 100644
--- a/coq/coq-db.el
+++ b/coq/coq-db.el
@@ -1,9 +1,18 @@
-;;; coq-db.el --- coq keywords database utility functions
-;;
+;;; coq-db.el --- coq keywords database utility functions -*- coding: utf-8; -*-
+
+;; 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
+
;; Author: Pierre Courtieu <courtieu@lri.fr>
+
;; License: GPL (GNU GENERAL PUBLIC LICENSE)
-;;
-;;
+
;;; Commentary:
;;
;; We store all information on keywords (tactics or command) in big
@@ -284,19 +293,20 @@ See `coq-syntax-db' for DB structure."
(defface coq-solve-tactics-face
(proof-face-specs
(:foreground "red") ; pour les fonds clairs
- (:foreground "red") ; pour les fond foncés
+ (:foreground "red1") ; pour les fonds foncés
()) ; pour le noir et blanc
"Face for names of closing tactics in proof scripts."
:group 'proof-faces)
-;;A new face for cheating tactics
-;; FIXMe: the background color disappear when locked region overrides it.
-;; this is hard to fix without re-colorizing afterward.
+;;A face for cheating tactics
+;; We use :box in addition to :background because box remains visible in
+;; locked-region. :reverse-video is another solution.
(defface coq-cheat-face
- (proof-face-specs
- (:background "red") ; pour les fonds clairs
- (:background "red") ; pour les fond foncés
- ()) ; pour le noir et blanc
+ '(;(((class color) (background light)) . (:inverse-video t :foreground "red" :background "black"))
+ ;(((class color) (background dark)) . (:inverse-video t :foreground "red1"))
+ (((class color) (background light)) . (:box (:line-width -1 :color "red" :style nil) :background "red"))
+ (((class color) (background dark)) . (:box (:line-width -1 :color "red1" :style nil) :background "red1"))
+ (t . ())) ; monocolor or greyscale: no highlight
"Face for names of cheating tactics in proof scripts."
:group 'proof-faces)
diff --git a/coq/coq-indent.el b/coq/coq-indent.el
index 878fb895..405cbb46 100644
--- a/coq/coq-indent.el
+++ b/coq/coq-indent.el
@@ -1,9 +1,17 @@
;;; coq-indent.el --- indentation for Coq
-;;
-;; Copyright (C) 2004-2006 LFCS Edinburgh.
+
+;; 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: Pierre Courtieu
;; Maintainer: Pierre Courtieu <courtieu@lri.fr>
-;;
+
;; Commentary:
;;
;; Indentation for Coq.
@@ -104,13 +112,19 @@ detect if they start something or not."
No context checking.")
+;; Goal selector syntax
+(defconst coq-goal-selector-regexp "[0-9]+\\s-*:\\s-*")
+
;; We can detect precisely bullets (and curlies) by looking at there
;; prefix: the prefix should be a real "." then spaces then only
;; bullets and curlys and spaces). This is used when search backward.
;; This variable is the regexp of possible prefixes
(defconst coq-bullet-prefix-regexp
(concat "\\(?:\\(?:" coq-simple-cmd-ender-prefix-regexp "\\)"
- "\\(?:\\.\\)\\(?:\\s-\\)\\(?:\\s-\\|{\\|}\\|-\\|+\\|\\*\\)*\\)"))
+ "\\(?:\\.\\)\\(?:\\s-\\)"
+ "\\(?:\\s-\\|"
+ "\\(?:" coq-goal-selector-regexp "\\)?"
+ "{\\|}\\|-\\|+\\|\\*\\)*\\)"))
;; matches regular command end (. and ... followed by a space or buffer end)
;; ". " and "... " are command endings, ".. " is not, same as in
@@ -152,7 +166,9 @@ There are 2 substrings:
* number 2 is the left context matched that is not part of the bullet" )
(defconst coq-curlybracket-end-command
- "\\(?:\\(?1:{\\)\\(?3:[^|]\\)\\|\\(?2:[^|]\\|\\=\\)\\(?1:}\\)\\)"
+ (concat "\\(?:\\(?1:"
+ "\\(?:" coq-bullet-prefix-regexp"\\)?"
+ "{\\)\\(?3:[^|]\\)\\|\\(?2:[^|]\\|\\=\\)\\(?1:}\\)\\)")
"Matches ltac curlies when searching backward. Warning: False positive.
There are 3 substrings (2 and 3 may be nil):
@@ -165,7 +181,10 @@ This matches more than real ltac curlies. See
only when searching backward).")
(defconst coq-curlybracket-end-command-backward
- (concat "\\(?:\\(?2:" coq-bullet-prefix-regexp "\\)\\(?:\\(?:\\(?1:{\\)\\(?3:[^|]\\)\\)\\|\\(?1:}\\)\\)\\)")
+ (concat "\\(?:\\(?2:" coq-bullet-prefix-regexp "\\)"
+ "\\(?:\\(?:\\(?1:" "\\(?:" coq-goal-selector-regexp "\\)?{\\)"
+ "\\(?3:[^|]\\)\\)"
+ "\\|\\(?1:}\\)\\)\\)")
"Matches ltac curly brackets when searching backward.
This should match EXACTLY script structuring curlies. No false
@@ -357,8 +376,28 @@ Comments are ignored, of course."
(start (coq-find-not-in-comment-backward "[^[:space:]]")))
;; we must find a "." to be sure, because {O} {P} is allowed in definitions
;; with implicits --> this function is recursive
- (if (looking-at "{\\|}\\|-\\|\\+\\|\\*") (coq-empty-command-p)
- (looking-at "\\.\\|\\`"))))
+ (cond
+ ;; "{" can be prefixed by a goal selector (coq-8.8).
+ ;; TODO: looking-back is supposed to be slow. Find something else?
+ ((or (and (looking-at "{")(looking-back "[0-9]+\\s-*:\\s-*" nil t))
+ (and (looking-at ":\\s-*{")(looking-back "[0-9]+\\s-*" nil t))
+ (and (looking-at "[0-9]+:\\s-*{") nil t))
+ (goto-char (match-beginning 0)); swallow goal selector
+ (coq-empty-command-p))
+ ;; other bulleting syntax
+ ((looking-at "{\\|}\\|-\\|\\+\\|\\*") (coq-empty-command-p))
+ ;; vernacular controls Time, Fail, Redirect, Timeout
+ ((or (and (looking-at "e\\>") (looking-back "\\<Tim") (- (point) 3))
+ (and (looking-at "l\\>") (looking-back "\\<Fai") (- (point) 3))
+ (and (looking-at "\"") (looking-back "\\<Redirect\\s-+\"[^\"]+"))
+ (and (looking-at "[[:digit:]]\\_>") (looking-back "\\<Timeout\\s-+[[:digit:]]*")))
+ (goto-char (match-beginning 0))
+ (coq-empty-command-p))
+ ;; not a bullet, we found something else, it should be either a
+ ;; dot or the beginning of the file, otherwise we are in the
+ ;; middle of a command
+ (t (looking-at "\\.\\|\\`"))
+ )))
; slight modification of proof-script-generic-parse-cmdend (one of the
diff --git a/coq/coq-local-vars.el b/coq/coq-local-vars.el
index 50a1f626..a097043a 100644
--- a/coq/coq-local-vars.el
+++ b/coq/coq-local-vars.el
@@ -1,14 +1,22 @@
;;; coq-local-vars.el --- local variable list tools for coq
-;;
-;; Copyright (C) 2006-2008 LFCS Edinburgh.
+
+;; 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: Pierre Courtieu
;; Maintainer: Pierre Courtieu <Pierre.Courtieu@cnam.fr>
-;;
-;; $Id$
-;;
+
;;; Commentary:
;;
+;;; Code:
+
(require 'local-vars-list) ; in lib directory
(eval-when-compile
@@ -19,7 +27,6 @@
(defvar coq-load-path))
-;;; Code:
(defconst coq-local-vars-doc nil
"Documentation-only variable.
diff --git a/coq/coq-par-compile.el b/coq/coq-par-compile.el
index 1580febd..17fe12d5 100644
--- a/coq/coq-par-compile.el
+++ b/coq/coq-par-compile.el
@@ -1,11 +1,19 @@
-;; coq-par-compile.el --- parallel compilation of required modules
-;; Copyright (C) 1994-2012 LFCS Edinburgh.
+;;; coq-par-compile.el --- parallel compilation of required modules
+
+;; 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: Hendrik Tews
-;; License: GPL (GNU GENERAL PUBLIC LICENSE)
;; Maintainer: Hendrik Tews <hendrik@askra.de>
-;;
-;; $Id$
-;;
+
+;; License: GPL (GNU GENERAL PUBLIC LICENSE)
+
;;; Commentary:
;;
;; This file implements compilation of required modules. The
@@ -24,6 +32,8 @@
;; changing compilers, all compilation jobs must be terminated. This is
;; consistent with the fact that the _CoqProject file is not reparsed.
+;;; Code:
+
(eval-when-compile
(require 'proof-compat))
diff --git a/coq/coq-par-test.el b/coq/coq-par-test.el
index f60baacf..8e83d1d4 100644
--- a/coq/coq-par-test.el
+++ b/coq/coq-par-test.el
@@ -1,9 +1,19 @@
-;; coq-par-test.el --- tests for parallel compilation
-;; Copyright (C) 2016 Hendrik Tews
+;;; coq-par-test.el --- tests for parallel compilation
+
+;; 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: Hendrik Tews
-;; License: GPL (GNU GENERAL PUBLIC LICENSE)
;; Maintainer: Hendrik Tews <hendrik@askra.de>
-;;
+
+;; License: GPL (GNU GENERAL PUBLIC LICENSE)
+
;;; Commentary:
;;
;; This file file contains tests for `coq-par-job-needs-compilation'.
@@ -18,6 +28,7 @@
;;
;; - integrate into PG build and test(?) system
+;;; Code:
(require 'coq-par-compile)
diff --git a/coq/coq-seq-compile.el b/coq/coq-seq-compile.el
index bf492f82..90bd3c3d 100644
--- a/coq/coq-seq-compile.el
+++ b/coq/coq-seq-compile.el
@@ -1,11 +1,19 @@
-;; coq-seq-compile.el --- sequential compilation of required modules
-;; Copyright (C) 1994-2012 LFCS Edinburgh.
+;;; coq-seq-compile.el --- sequential compilation of required modules
+
+;; 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: Hendrik Tews
-;; License: GPL (GNU GENERAL PUBLIC LICENSE)
;; Maintainer: Hendrik Tews <hendrik@askra.de>
-;;
-;; $Id$
-;;
+
+;; License: GPL (GNU GENERAL PUBLIC LICENSE)
+
;;; Commentary:
;;
;; This file implements compilation of required modules. The
@@ -14,6 +22,7 @@
;; proof-action-list and compiles one module after the other.
;;
+;;; Code:
(eval-when-compile
(require 'proof-compat))
diff --git a/coq/coq-smie.el b/coq/coq-smie.el
index 33ef19d1..2b5e59e9 100644
--- a/coq/coq-smie.el
+++ b/coq/coq-smie.el
@@ -1,10 +1,18 @@
;;; coq-smie.el --- SMIE lexer, grammar, and indent rules for Coq
-;; Copyright (C) 2014 Free Software Foundation, Inc
+;; 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: Pierre Courtieu
;; Stefan Monnier
;; Maintainer: Pierre Courtieu <Pierre.Courtieu@cnam.fr>
+
;; License: GPLv3+ (GNU GENERAL PUBLIC LICENSE version 3 or later)
;;; Commentary:
@@ -42,6 +50,19 @@
; ,@body
; (message "%.06f" (float-time (time-since time)))))
+(defcustom coq-smie-user-tokens nil
+ "Alist of (syntax . token) pairs to extend the coq smie parser.
+These are user configurable additional syntax for smie tokens. It
+allows to define alternative syntax for smie token. Typical
+example: if you define a infix operator \"xor\" you may want to
+define it as a new syntax for token \"or\" in order to have the
+indentation rules of or applied to xor. Other exemple: if you
+want to define a new notation \"ifb\" ... \"then\" \"else\" then
+you need to declare \"ifb\" as a new syntax for \"if\" to make
+indentation work well."
+ :type '(alist :key-type string :value-type string)
+ :group 'coq)
+
(defun coq-string-suffix-p (str1 str2 &optional ignore-case)
"Return non-nil if STR1 is a prefix of STR2.
@@ -375,6 +396,9 @@ The point should be at the beginning of the command name."
(defun coq-smie-forward-token ()
(let ((tok (smie-default-forward-token)))
(cond
+ ((assoc tok coq-smie-user-tokens)
+ (let ((res (assoc tok coq-smie-user-tokens)))
+ (cdr res)))
;; @ may be ahead of an id, it is part of the id.
((and (equal tok "@") (looking-at "[[:alpha:]_]"))
(let ((newtok (coq-smie-forward-token))) ;; recursive call
@@ -492,6 +516,9 @@ The point should be at the beginning of the command name."
(defun coq-smie-backward-token ()
(let* ((tok (smie-default-backward-token)))
(cond
+ ((assoc tok coq-smie-user-tokens)
+ (let ((res (assoc tok coq-smie-user-tokens)))
+ (cdr res)))
;; Distinguish between "," from quantification and other uses of
;; "," (tuples, tactic arguments)
((equal tok ",")
@@ -567,12 +594,28 @@ The point should be at the beginning of the command name."
(goto-char (1- (point))) "{|")
((and (zerop (length tok)) (member (char-before) '(?\{ ?\}))
- (save-excursion
- (forward-char -1)
- (let ((nxttok (coq-smie-backward-token))) ;; recursive call
- (coq-is-cmdend-token nxttok))))
+ (save-excursion
+ (forward-char -1)
+ (if (and (looking-at "{")
+ (looking-back "\\([0-9]+\\s-*:\\s-*\\)" nil t))
+ (goto-char (match-beginning 0)))
+ (let ((nxttok (coq-smie-backward-token))) ;; recursive call
+ (coq-is-cmdend-token nxttok))))
(forward-char -1)
- (if (looking-at "{") "{ subproof" "} subproof"))
+ (if (looking-at "}") "} subproof"
+ (if (and (looking-at "{")
+ (looking-back "\\([0-9]+\\s-*:\\s-*\\)" nil t))
+ (goto-char (match-beginning 0)))
+ "{ subproof"
+ ))
+
+ ;; ((and (zerop (length tok)) (member (char-before) '(?\{ ?\}))
+ ;; (save-excursion
+ ;; (forward-char -1)
+ ;; (let ((nxttok (coq-smie-backward-token))) ;; recursive call
+ ;; (coq-is-cmdend-token nxttok))))
+ ;; (forward-char -1)
+ ;; (if (looking-at "{") "{ subproof" "} subproof"))
((and (equal tok ":") (looking-back "\\<\\(constr\\|ltac\\|uconstr\\)" nil))
": ltacconstr")
@@ -599,6 +642,9 @@ The point should be at the beginning of the command name."
((member tok '("*;" "-*;" "|-*;" "*|-*;"))
;; FIXME; can be "; ltac" too
(forward-char (- (length tok) 1)) "; tactic")
+ ;; bullet detected, is it really a bullet? we have to traverse
+ ;; recursively any other bullet or "n:{" "}". this is the work of
+ ;; coq-empty-command-p
((and (string-match coq-bullet-regexp-nospace tok)
(save-excursion (coq-empty-command-p)))
(concat tok " bullet"))
diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el
index 156d39e1..63d44666 100644
--- a/coq/coq-syntax.el
+++ b/coq/coq-syntax.el
@@ -1,10 +1,23 @@
-;; 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
@@ -516,7 +529,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
diff --git a/coq/coq-system.el b/coq/coq-system.el
index 0bcf6a07..f3eabafc 100644
--- a/coq/coq-system.el
+++ b/coq/coq-system.el
@@ -1,9 +1,18 @@
-;; coq-system.el --- common part of compilation feature
-;; Copyright (C) 2015 LFCS Edinburgh.
+;;; coq-system.el --- common part of compilation feature
+
+;; 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: Hendrik Tews, Pierre Courtieu
-;; License: GPL (GNU GENERAL PUBLIC LICENSE)
;; Maintainer: Pierre.Courtieu<Pierre.Courtieu@cnam.fr>
-;;
+
+;; License: GPL (GNU GENERAL PUBLIC LICENSE)
;;; Commentary:
;;
@@ -12,6 +21,8 @@
;; support for older versions of coq.
;;
+;;; Code:
+
(require 'proof)
(eval-when-compile
@@ -32,7 +43,7 @@
(put 'coq-prog-args 'safe-local-variable #'coq--string-list-p)
(defcustom coq-prog-env nil
- "List of environment settings d to pass to Coq process.
+ "List of environment settings to pass to Coq process.
On Windows you might need something like:
(setq coq-prog-env '(\"HOME=C:\\Program Files\\Coq\\\"))"
:group 'coq)
@@ -416,8 +427,8 @@ LOAD-PATH, CURRENT-DIRECTORY, PRE-V85: see `coq-coqc-prog-args'."
(coq-coqtop-prog-args coq-load-path))
(defcustom coq-use-project-file t
- "If t, when opening a coq file read the dominating _CoqProject.
-If t, when a coq file is opened, Proof General will look for a
+ "If t, when opening a Coq file read the dominating _CoqProject.
+If t, when a Coq file is opened, Proof General will look for a
project file (see `coq-project-filename') somewhere in the
current directory or its parent directories. If there is one,
its contents are read and used to determine the arguments that
diff --git a/coq/coq-unicode-tokens.el b/coq/coq-unicode-tokens.el
index faa02458..5f2cd0c6 100644
--- a/coq/coq-unicode-tokens.el
+++ b/coq/coq-unicode-tokens.el
@@ -1,8 +1,17 @@
-;;; -*- coding: utf-8; -*-
-;; coq-unicode-tokens.el --- (No) Tokens for Unicode Tokens package
-;;
-;; Copyright(C) 2008, 2009 David Aspinall / LFCS Edinburgh
+;;; coq-unicode-tokens.el --- (No) Tokens for Unicode Tokens package -*- coding: utf-8; -*-
+
+;; 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
+
;; Author: David Aspinall <David.Aspinall@ed.ac.uk>
+
+;;; Commentary:
;;
;; This file is loaded by `proof-unicode-tokens.el'.
;;
diff --git a/coq/coq.el b/coq/coq.el
index aff05d28..b56f879e 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -1,12 +1,23 @@
-;; coq.el --- Major mode for Coq proof assistant -*- coding: utf-8 -*-
-;; Copyright (C) 1994-2009 LFCS Edinburgh.
+;;; coq.el --- Major mode for Coq proof assistant -*- coding: utf-8 -*-
+
+;; 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: Healfdene Goguen, Pierre Courtieu
-;; License: GPL (GNU GENERAL PUBLIC LICENSE)
;; Maintainer: Pierre Courtieu <Pierre.Courtieu@cnam.fr>
-;;
-;; $Id$
+;; License: GPL (GNU GENERAL PUBLIC LICENSE)
+
+;;; Commentary:
+;;
+;;; Code:
(eval-when-compile
(require 'cl)
@@ -78,7 +89,7 @@
;; :group 'coq)
(defcustom coq-user-init-cmd nil
- "user defined init commands for Coq.
+ "User defined init commands for Coq.
These are appended at the end of `coq-shell-init-cmd'."
:type '(repeat (cons (string :tag "command")))
:group 'coq)
@@ -91,12 +102,12 @@ These are appended at the end of `coq-shell-init-cmd'."
;; Default coq is only Private_ and _subproof
(defcustom coq-search-blacklist-string ; add this? \"_ind\" \"_rect\" \"_rec\"
"\"Private_\" \"_subproof\""
- "String for blacklisting strings from requests to coq environment."
+ "String for blacklisting strings from requests to Coq environment."
:type 'string
:group 'coq)
(defcustom coq-prefer-top-of-conclusion nil
- "prefer start of the conclusion over its end when displaying goals
+ "Prefer start of the conclusion over its end when displaying goals
that do not fit in the goals window."
:type 'boolean
:group 'coq)
@@ -432,7 +443,8 @@ This is a subroutine of `proof-shell-filter'."
(set-marker
proof-shell-urgent-message-scanner
(if end ;; couldn't find message start; move forward to avoid rescanning
- (max initstart
+ (max (or lastend 1) ;; goto after last end urgent msg
+ ;; or near the end of current output if that jumps farther.
(- (point)
(1+ proof-shell-eager-annotation-start-length)))
;; incomplete message; leave marker at start of message
@@ -884,7 +896,7 @@ Support dot.notation.of.modules."
(if notation (concat "\"" notation "\"") ""))))
(defcustom coq-remap-mouse-1 nil
- "Wether coq mode should remap mouse button 1 to coq queries.
+ "Whether Coq mode should remap mouse button 1 to Coq queries.
This overrides the default global binding of (control mouse-1) and
(shift mouse-1) (buffers and faces menus). Hence it is nil by
@@ -1840,7 +1852,7 @@ Near here means PT is either inside or just aside of a comment."
(defpacustom search-blacklist coq-search-blacklist-string
- "Strings to blacklist in requests to coq environment."
+ "Strings to blacklist in requests to Coq environment."
:type 'string
:get 'coq-get-search-blacklist
:setting coq-set-search-blacklist)
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-17 11:13:09 +0000