diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2009-08-12 19:56:31 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2009-08-12 19:56:31 +0000 |
| commit | 2a9d7ed6a2ea4ba9dc35331d3ad0eb8298f0383c (patch) | |
| tree | 3bce0cb723a66e1e6b86a15adff74b5355f6effc /coq/coq-unicode-tokens.el | |
| parent | 92daa2330135394afcd6ec6836248b105fc16644 (diff) | |
Add indirection for setting unicode tokens variables to add customize menu options
Diffstat (limited to 'coq/coq-unicode-tokens.el')
| -rw-r--r-- | coq/coq-unicode-tokens.el | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/coq/coq-unicode-tokens.el b/coq/coq-unicode-tokens.el index d18964a2..c0691d85 100644 --- a/coq/coq-unicode-tokens.el +++ b/coq/coq-unicode-tokens.el @@ -78,7 +78,7 @@ in this table. When the file is saved, the reverse is done. The string mapping can be anything, but should be such that tokens can be uniquely recovered from a decoded text; otherwise results will be undefined when files are saved." - :type '(repeat (cons (string :tag "Token name") + :type '(repeat (list (string :tag "Token name") (string :tag "Unicode string"))) :set 'proof-set-value :group 'coq @@ -161,13 +161,13 @@ You can adjust this table to add more entries, or to change entries for glyphs that not are available in your Emacs or chosen font. These shortcuts are only used for input; no reverse conversion is -performed. But if tokens exist for the target of shortcuts, they -will be used on saving the buffer." +performed. This means that the target strings need to have a defined +meaning to be useful." :type '(repeat (cons (string :tag "Shortcut sequence") (string :tag "Unicode string"))) :set 'proof-set-value :group 'isabelle - :tag "Coq Unicode Token Mapping") + :tag "Coq Unicode Input Shortcuts") ;; |