Fix most doc issues raised by (checkdoc)

5 files changed, 61 insertions, 15 deletions

diff --git a/easycrypt/easycrypt-abbrev.el b/easycrypt/easycrypt-abbrev.el
index 3850ffb7..fa9cdcfc 100644
--- a/easycrypt/easycrypt-abbrev.el
+++ b/easycrypt/easycrypt-abbrev.el
@@ -1,3 +1,5 @@
+;;; easycrypt-abbrev.el --- Abbrev table and menus for EasyCrypt mode
+
 ;; --------------------------------------------------------------------
 ;; Copyright (c) - 2012--2016 - IMDEA Software Institute
 ;; Copyright (c) - 2012--2016 - Inria
@@ -5,9 +7,14 @@
 ;; Distributed under the terms of the GPL-v3 license
 ;; --------------------------------------------------------------------
 
+;;; Commentary:
+;; 
+
 (require 'proof)
 (require 'easycrypt-syntax)
 
+;;; Code:
+
 (defpgdefault menu-entries
   '(
     ["Use Three Panes" proof-three-window-toggle
@@ -23,3 +30,5 @@
 ))
 
 (provide 'easycrypt-abbrev)
+
+;;; easycrypt-abbrev.el ends here
diff --git a/easycrypt/easycrypt-hooks.el b/easycrypt/easycrypt-hooks.el
index 3cf891e3..67592973 100644
--- a/easycrypt/easycrypt-hooks.el
+++ b/easycrypt/easycrypt-hooks.el
@@ -1,3 +1,5 @@
+;;; easycrypt-hooks.el --- Auxiliary functions for EasyCrypt mode
+
 ;; --------------------------------------------------------------------
 ;; Copyright (c) - 2012--2016 - IMDEA Software Institute
 ;; Copyright (c) - 2012--2016 - Inria
@@ -5,9 +7,14 @@
 ;; Distributed under the terms of the GPL-v3 license
 ;; --------------------------------------------------------------------
 
+;;; Commentary:
+;; 
+
 (require 'span)
 (require 'proof)
 
+;;; Code:
+
 (defvar easycrypt-last-but-one-statenum 0)
 (defvar easycrypt-proof-weak-mode nil)
 
@@ -38,7 +45,7 @@
 
 (defun easycrypt-last-prompt-info (s)
   "Extract the information from prompt."
-  (let ((lastprompt (or s (error "no prompt"))))
+  (let ((lastprompt (or s (error "No prompt"))))
      (when (string-match "\\[\\([0-9]+\\)|\\(\\sw+\\)\\]" lastprompt)
            (list (string-to-number (match-string 1 lastprompt))
                  (if (equal (match-string 2 lastprompt) "weakcheck") t nil)))))
@@ -68,3 +75,5 @@
        (list (format "undo %s." (int-to-string span-staten)))))
 
 (provide 'easycrypt-hooks)
+
+;;; easycrypt-hooks.el ends here
diff --git a/easycrypt/easycrypt-keywords.el b/easycrypt/easycrypt-keywords.el
index e0b9d369..feb64fb1 100644
--- a/easycrypt/easycrypt-keywords.el
+++ b/easycrypt/easycrypt-keywords.el
@@ -1,3 +1,5 @@
+;;; easycrypt-keywords.el --- Definition of keywords for EasyCrypt mode
+
 ;; --------------------------------------------------------------------
 ;; Copyright (c) - 2012--2016 - IMDEA Software Institute
 ;; Copyright (c) - 2012--2016 - Inria
@@ -5,7 +7,12 @@
 ;; Distributed under the terms of the GPL-v3 license
 ;; --------------------------------------------------------------------
 
-; Generated on Tue Feb 21 23:37:34 2017
+;;; Commentary:
+;; 
+;; Generated on Tue Feb 21 23:37:34 2017
+;;
+
+;;; Code:
 
 (defvar easycrypt-bytac-keywords '(
   "exact"
@@ -175,3 +182,5 @@
 ))
 
 (provide 'easycrypt-keywords)
+
+;;; easycrypt-keywords.el ends here
diff --git a/easycrypt/easycrypt-syntax.el b/easycrypt/easycrypt-syntax.el
index a784395b..48e64a57 100644
--- a/easycrypt/easycrypt-syntax.el
+++ b/easycrypt/easycrypt-syntax.el
@@ -1,3 +1,5 @@
+;;; easycrypt-syntax.el --- Syntax definitions for EasyCrypt mode
+
 ;; --------------------------------------------------------------------
 ;; Copyright (c) - 2012--2016 - IMDEA Software Institute
 ;; Copyright (c) - 2012--2016 - Inria
@@ -5,10 +7,15 @@
 ;; Distributed under the terms of the GPL-v3 license
 ;; --------------------------------------------------------------------
 
+;;; Commentary:
+;; 
+
 (require 'proof-syntax)
 (require 'easycrypt-keywords)
 (require 'easycrypt-hooks)
 
+;;; Code:
+
 (defconst easycrypt-id "[A-Za-z_]+")
 
 (defconst easycrypt-terminal-string    ".")
@@ -20,7 +27,7 @@
 (defconst easycrypt-non-undoables-regexp "^pragma\\b")
 
 (defconst easycrypt-keywords-code-open  '("{"))
-(defconst easycrypt-keywords-code-close '("}")) 
+(defconst easycrypt-keywords-code-close '("}"))
 (defconst easycrypt-keywords-code-end   '(";"))
 
 (defvar easycrypt-other-symbols "\\(\\.\\.\\|\\[\\]\\)")
@@ -45,7 +52,7 @@
           "\\s-+\\(?:nosmt\\s-+\\)?\\(\\sw+\\)"))
 
 (defun easycrypt-save-command-p (span str)
-  "Decide whether argument is a [save|qed] command or not"
+  "Decide whether argument is a [save|qed] command or not."
   (let ((txt (or (span-property span 'cmd) "")))
        (proof-string-match-safe easycrypt-proof-save-regexp txt)))
 
@@ -61,7 +68,7 @@
   (modify-syntax-entry ?_   "_")
 
   ;; For comments
-  (modify-syntax-entry ?\* ". 23") 
+  (modify-syntax-entry ?\* ". 23")
 
   ;; For blocks
   (modify-syntax-entry ?\( "()1")
@@ -84,7 +91,7 @@
   ;; FIXME: really needs change in generic function to take account of this,
   ;; since the end character of a command is not the start
   (concat "\\(\\s(\\|\\s)\\|\\sw\\|\\s \\|\\s_\\)*="  ;match assignments
-          "\\|;;\\|;\\|" 
+          "\\|;;\\|;\\|"
           (proof-ids-to-regexp easycrypt-global-keywords))
   "Regexp matching any EasyCrypt command start or the terminator character.")
 
@@ -176,3 +183,5 @@
   (modify-syntax-entry ?\) ")(4"))
 
 (provide 'easycrypt-syntax)
+
+;;; easycrypt-syntax.el ends here
diff --git a/easycrypt/easycrypt.el b/easycrypt/easycrypt.el
index f7f0059f..e9b40358 100644
--- a/easycrypt/easycrypt.el
+++ b/easycrypt/easycrypt.el
@@ -1,3 +1,5 @@
+;;; easycrypt.el --- Major mode for EasyCrypt
+
 ;; --------------------------------------------------------------------
 ;; Copyright (c) - 2012--2016 - IMDEA Software Institute
 ;; Copyright (c) - 2012--2016 - Inria
@@ -5,11 +7,16 @@
 ;; Distributed under the terms of the GPL-v3 license
 ;; --------------------------------------------------------------------
 
+;;; Commentary:
+;; 
+
 (require 'proof)
 (require 'easycrypt-syntax)
 (require 'easycrypt-hooks)
 (require 'easycrypt-abbrev)
 
+;;; Code:
+
 (add-to-list 'hs-special-modes-alist
   '(easycrypt-mode "{" "}" "/[*/]" nil nil))
 
@@ -27,7 +34,7 @@
 
 (defcustom easycrypt-load-path nil
   "Non-standard EasyCrypt library load path.
-This list specifies the include path for EasyCrypt. The elements of
+This list specifies the include path for EasyCrypt.  The elements of
 this list are strings."
   :type  '(repeat (string :tag "simple directory (-I)"))
   :safe  'easycrypt-load-path-safep
@@ -102,7 +109,7 @@ this list are strings."
          proof-three-window-mode-policy        (quote hybrid)
          proof-auto-multiple-files             t)
 
-  ; Setting indents 
+  ; Setting indents
   (set   (make-local-variable 'indent-tabs-mode) nil)
   (setq  proof-indent-enclose-offset   (- proof-indent)
          proof-indent-open-offset     0
@@ -158,20 +165,20 @@ this list are strings."
 (define-derived-mode easycrypt-response-mode proof-response-mode
   "EasyCrypt response" nil
   (easycrypt-init-output-syntax-table)
-  (setq  proof-response-font-lock-keywords 
+  (setq  proof-response-font-lock-keywords
          easycrypt-font-lock-keywords)
   (proof-response-config-done))
 
 (define-derived-mode easycrypt-goals-mode proof-goals-mode
   "EasyCrypt goals" nil
   (easycrypt-init-output-syntax-table)
-  (setq  proof-goals-font-lock-keywords 
+  (setq  proof-goals-font-lock-keywords
          easycrypt-font-lock-keywords)
   (proof-goals-config-done))
 
-(defun easycrypt-get-last-error-location () 
-  "Remove [error] in the error message and extract the position
-  and length of the error "
+(defun easycrypt-get-last-error-location ()
+  "Remove [error] in the error message and extract the position and
+length of the error."
   (proof-with-current-buffer-if-exists proof-response-buffer
 
      (goto-char (point-max))
@@ -188,8 +195,8 @@ this list are strings."
    (while (proof-looking-at "\\s-") (forward-char 1)))
 
 (defun easycrypt-highlight-error ()
-  "Use 'easycrypt-get-last-error-location' to know the position
-  of the error and then highlight in the script buffer"
+  "Use ‘easycrypt-get-last-error-location’ to know the position of the
+error and then highlight in the script buffer."
   (proof-with-current-buffer-if-exists proof-script-buffer
     (let ((mtch (easycrypt-get-last-error-location)))
         (when mtch
@@ -260,4 +267,7 @@ this list are strings."
   '(lambda () (when proof-three-window-enable (proof-layout-windows))))
 
 ;; --------------------------------------------------------------------
+
 (provide 'easycrypt)
+
+;;; easycrypt.el ends here