From b96ec627f9adcd601ae347d08a9013e63187d592 Mon Sep 17 00:00:00 2001
From: Rustan Leino <leino@microsoft.com>
Date: Tue, 26 Jul 2011 19:02:46 -0700
Subject: Chalice: added string type and string literals (but no other string
 operations)

---
 Util/Emacs/chalice-mode.el                            | 2 +-
 Util/VS2010/Chalice/ChaliceLanguageService/Grammar.cs | 2 +-
 Util/latex/chalice.sty                                | 2 +-
 Util/vim/syntax/chalice.vim                           | 2 +-
 4 files changed, 4 insertions(+), 4 deletions(-)

(limited to 'Util')

diff --git a/Util/Emacs/chalice-mode.el b/Util/Emacs/chalice-mode.el
index d1f21dc8..c8cef685 100644
--- a/Util/Emacs/chalice-mode.el
+++ b/Util/Emacs/chalice-mode.el
@@ -44,7 +44,7 @@
         "old" "rd" "receive" "release" "reorder" "result" "send" "share"
         "this" "unfold" "unfolding" "unshare" "while"
         "false" "true" "null")) . font-lock-keyword-face)
-   `(,(chalice-regexp-opt '("bool" "int" "seq" "token")) . font-lock-type-face)
+   `(,(chalice-regexp-opt '("bool" "int" "string" "seq" "token")) . font-lock-type-face)
    )
   "Minimal highlighting for Chalice mode")
 
diff --git a/Util/VS2010/Chalice/ChaliceLanguageService/Grammar.cs b/Util/VS2010/Chalice/ChaliceLanguageService/Grammar.cs
index a6371d71..4ae603e8 100644
--- a/Util/VS2010/Chalice/ChaliceLanguageService/Grammar.cs
+++ b/Util/VS2010/Chalice/ChaliceLanguageService/Grammar.cs
@@ -22,7 +22,7 @@ namespace Demo
           "call", "if", "else", "while",
           "invariant", "lockchange",
           "returns", "requires", "ensures", "where",
-          "int", "bool", "false", "true", "null", "waitlevel", "lockbottom",
+          "int", "bool", "false", "true", "null", "string", "waitlevel", "lockbottom",
           "module", "external",
           "predicate", "function", "free", "send", "receive",
           "ite", "fold", "unfold", "unfolding", "in", "forall", "exists",
diff --git a/Util/latex/chalice.sty b/Util/latex/chalice.sty
index 4ef98f9c..a04d6f23 100644
--- a/Util/latex/chalice.sty
+++ b/Util/latex/chalice.sty
@@ -27,7 +27,7 @@
     old,%
     predicate,%
     rd,reorder,release,requires,result,returns,%
-    seq,share,%
+    seq,share,string,%
     this,token,true,%
     unfold,unfolding,unshare,%
     var,%
diff --git a/Util/vim/syntax/chalice.vim b/Util/vim/syntax/chalice.vim
index df8b9bee..86b65d74 100644
--- a/Util/vim/syntax/chalice.vim
+++ b/Util/vim/syntax/chalice.vim
@@ -11,7 +11,7 @@ syntax keyword chaliceConditional if then else
 syntax keyword chaliceRepeat foreach while
 syntax keyword chaliceStatement assert assume call reorder share unshare acquire release lock rd downgrade free fold unfold fork join wait signal send receive 
 syntax keyword chaliceKeyword external var ghost returns where const new between and above below waitlevel lockbottom this result holds refines replaces spec by transforms
-syntax keyword chaliceType int bool seq token
+syntax keyword chaliceType int bool string seq token
 syntax keyword chaliceLogic invariant requires ensures lockchange
 syntax keyword chaliceOperator forall exists old fresh old credit acc unfolding in eval ite rd
 syntax keyword chaliceBoolean true false
-- 
cgit v1.2.3