diff options
author | Erik Martin-Dorel <erik@martin-dorel.org> | 2018-08-23 01:37:33 +0200 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-08-23 01:37:33 +0200 |
commit | 733cd24a7368ee186884da488da0f59bbedb627e (patch) | |
tree | e2a6832c08a6f058f423879c40c02fd924082af3 /easycrypt | |
parent | 26b3bf9f070e9aee45c6e3d19bca475d4ae8ed37 (diff) | |
parent | 7986697e7999e1d24356d459d64e7be5ee4c8da0 (diff) |
Merge pull request #380 from ProofGeneral/prepare-melpa
Prepare PG for MELPA
Diffstat (limited to 'easycrypt')
-rw-r--r-- | easycrypt/easycrypt-abbrev.el | 9 | ||||
-rw-r--r-- | easycrypt/easycrypt-hooks.el | 11 | ||||
-rw-r--r-- | easycrypt/easycrypt-keywords.el | 11 | ||||
-rw-r--r-- | easycrypt/easycrypt-syntax.el | 17 | ||||
-rw-r--r-- | easycrypt/easycrypt.el | 28 |
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 |