From 6fae4cb4715b1a55f6af4a39e1eced4038eace4d Mon Sep 17 00:00:00 2001
From: David Aspinall <da@inf.ed.ac.uk>
Date: Sun, 10 Oct 2010 16:57:25 +0000
Subject: Add some more tokens for making pretty pictures

---
 coq/coq-unicode-tokens.el | 19 ++++++++++++++++---
 1 file changed, 16 insertions(+), 3 deletions(-)

(limited to 'coq/coq-unicode-tokens.el')

diff --git a/coq/coq-unicode-tokens.el b/coq/coq-unicode-tokens.el
index 540b6fb5..124a0146 100644
--- a/coq/coq-unicode-tokens.el
+++ b/coq/coq-unicode-tokens.el
@@ -94,6 +94,19 @@
     ("false" "false" bold sans)
     ("true" "true" bold sans)
 
+    ;; example tokens used in Benjamin C. Pierce et al's 
+    ;; Software Foundations course
+    ("WHILE" "WHILE" bold sans)
+    ("DO" "DO" bold sans)
+    ("END" "END" bold sans)
+    ("SKIP" "SKIP" bold sans)
+    ("THEN" "THEN" bold sans)
+    ("ELSE" "ELSE" bold sans)
+    ("IFB" "IFB" bold sans)
+    ("FI" "FI" bold sans)
+    ("{{" "⦃" bold)
+    ("}}" "⦄" bold)
+
     ;; symbols without utf8.v  (but also without context)
     ("lhd" "⊲")
     ("rhd" "⊳")
@@ -116,9 +129,9 @@
     
     ;; ("==" "≡")  ; Setoid equiv (NB: same presentation, pot confusing)
 
-    ;; ("-->" "⟹-") ; Morphisms
-    ;; ("++>" "⟹+") ; 
-    ;; ("==>" "⟹=") ; 
+    ("-->" "⟹-") ; Morphisms
+    ("++>" "⟹+") ; 
+    ("==>" "⟹") ; 
 
     (":=" "≔")
     ("|-" "⊢")
-- 
cgit v1.2.3