diff options
Diffstat (limited to 'coq/coq.el')
| -rw-r--r-- | coq/coq.el | 34 |
1 files changed, 23 insertions, 11 deletions
@@ -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) |