summaryrefslogtreecommitdiff
path: root/Util
diff options
context:
space:
mode:
authorGravatar Rustan Leino <leino@microsoft.com>2011-07-26 19:02:46 -0700
committerGravatar Rustan Leino <leino@microsoft.com>2011-07-26 19:02:46 -0700
commitb96ec627f9adcd601ae347d08a9013e63187d592 (patch)
treeb9079dae2524253698641997acc4f076fc2ef8c6 /Util
parentee8d3aaea78450c72111c5736bbb3ff500139df9 (diff)
Chalice: added string type and string literals (but no other string operations)
Diffstat (limited to 'Util')
-rw-r--r--Util/Emacs/chalice-mode.el2
-rw-r--r--Util/VS2010/Chalice/ChaliceLanguageService/Grammar.cs2
-rw-r--r--Util/latex/chalice.sty2
-rw-r--r--Util/vim/syntax/chalice.vim2
4 files changed, 4 insertions, 4 deletions
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