diff options
author | Erik Martin-Dorel <erik@martin-dorel.org> | 2018-08-23 00:01:12 +0200 |
---|---|---|
committer | Erik Martin-Dorel <erik@martin-dorel.org> | 2018-08-23 01:23:31 +0200 |
commit | 86d22428959a0f5aecef270e0f4dd7d4b5712fc3 (patch) | |
tree | 676fe59b7644498172f96b6da605745a6bf71a13 /coq/coq-unicode-tokens.el | |
parent | 3ba86af3271111cb056676c631b7caa6897e06f1 (diff) |
Fix most doc issues raised by (checkdoc)
Diffstat (limited to 'coq/coq-unicode-tokens.el')
-rw-r--r-- | coq/coq-unicode-tokens.el | 14 |
1 files changed, 8 insertions, 6 deletions
diff --git a/coq/coq-unicode-tokens.el b/coq/coq-unicode-tokens.el index 5f2cd0c6..349038c1 100644 --- a/coq/coq-unicode-tokens.el +++ b/coq/coq-unicode-tokens.el @@ -20,7 +20,7 @@ ;; variable for documentation. ;; ;; For Coq, there is no dedicated token syntax, it's probably -;; preferable to use UTF-8 notation directly (see utf8.v). +;; preferable to use UTF-8 notation directly (see utf8.v). ;; ;; On the other hand, for easily portable files, one can fix ;; ordinary character sequences as tokens, like the old X-Symbol @@ -31,7 +31,7 @@ ;; Unicode characters, whereas ordinary character sequences are ;; displayed as those characters. ;; -;; Recommended ways to work: +;; Recommended ways to work: ;; ;; 1) UTF-8 buffers: ☑ Show Symbol Tokens (ON) ;; ☑ Enable Shortcuts (ON) @@ -45,6 +45,8 @@ (require 'proof-unicode-tokens) +;;; Code: + (defconst coq-token-format "") ; Let generic code do the job (defconst coq-token-match nil) (defconst coq-hexcode-match nil) @@ -103,7 +105,7 @@ ("false" "false" bold sans) ("true" "true" bold sans) - ;; example tokens used in Benjamin C. Pierce et al's + ;; example tokens used in Benjamin C. Pierce et al's ;; Software Foundations course ("WHILE" "WHILE" bold sans) ("DO" "DO" bold sans) @@ -123,7 +125,7 @@ (">=" "≥") ("=>" "⇒") ("->" "→") ; or ⟶ or ⟹ if you prefer - ("<-" "←") ; or ⟵ or ⟸ + ("<-" "←") ; or ⟵ or ⟸ ("<->" "↔") ; or ⟷ ... ("++" "⧺") ("<<" "《") @@ -151,8 +153,8 @@ ("~" "¬") ;; A dirty hack for the goals window, shouldn't be input syntax! - ("============================" - "⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯" + ("============================" + "⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯" bold tactical) ) ;; an alist of token name, unicode char sequence |