diff options
author | David Aspinall <da@inf.ed.ac.uk> | 2009-09-05 12:51:03 +0000 |
---|---|---|
committer | David Aspinall <da@inf.ed.ac.uk> | 2009-09-05 12:51:03 +0000 |
commit | c50c8e3075f9ed2306265b8b13e38f374b9cf404 (patch) | |
tree | c1dc763ad4bdd3334d58d602b8b000f53bcc9253 | |
parent | 477ad117b93890a6b85017ecb25d75765f313200 (diff) |
Add shortcuts for (| and |).
Ensure if shortcuts are customized, replacement-alist is reset too.
-rw-r--r-- | isar/isar-unicode-tokens.el | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/isar/isar-unicode-tokens.el b/isar/isar-unicode-tokens.el index a8b46d44..065f7d16 100644 --- a/isar/isar-unicode-tokens.el +++ b/isar/isar-unicode-tokens.el @@ -580,6 +580,8 @@ For Isabelle, the token TOKNAME is made into the token \\< TNAME >." ("{|" . "\\<lbrace>") ("|}" . "\\<rbrace>") ("---" . "\\<emdash>") + ("(|" . "\\<lparr>") + ("|)" . "\\<rparr>") ;; useful for unicode-tokens-replace-shortcuts ("ALL" . "\\<forall>") ("EX" . "\\<exists>") @@ -589,7 +591,7 @@ For Isabelle, the token TOKNAME is made into the token \\< TNAME >." ;; ("!" . "\\<forall>") ;; ("?" . "\\<exists>") ;; extra misc, switch them off if you don't like them - ;("|>" . "\\<triangleright>") + ;("|>" . "\\<triangleright>") ; clashes with ML parsing combinator ("<|" . "\\<triangleleft>")) "Shortcut key sequence table for symbol tokens input. See `unicode-tokens-shortcut-alist'." @@ -617,7 +619,9 @@ See `unicode-tokens-shortcut-alist'." (cons (concat "\\" (car tokentry)) (format isar-token-format (car tokentry)))) (append isar-greek-letters-tokens - isar-symbols-tokens))))) + isar-symbols-tokens)))) + ;; copy default for this from above + (setq unicode-tokens-shortcut-replacement-alist nil)) (isar-init-shortcut-alists) |