diff options
| author |  Unknown <leino@LEINO6.redmond.corp.microsoft.com> | 2012-09-28 16:12:27 -0700 |
|---|---|---|
| committer | Unknown <leino@LEINO6.redmond.corp.microsoft.com> | 2012-09-28 16:12:27 -0700 |
| commit | d3a315961bf6a7b83225f6311dcf40b0dbba6463 (patch) | |
| tree | b5379d0088109450d51e962a9e2d5e70c7400c41 /Util | |
| parent | a9c6c8fcf205a13c759c6f09e69b01d3b144df94 (diff) | |
Boogie: updated syntax highlighting ("real")
Diffstat (limited to 'Util')
| -rw-r--r-- | Util/Emacs/boogie-mode.el | 2 | ||||
| -rw-r--r-- | Util/VS2010/Boogie/BoogieLanguageService/Grammar.cs | 8 | ||||
| -rw-r--r-- | Util/latex/boogie.sty | 2 | ||||
| -rw-r--r-- | Util/vim/syntax/boogie.vim | 2 |
4 files changed, 6 insertions, 8 deletions
diff --git a/Util/Emacs/boogie-mode.el b/Util/Emacs/boogie-mode.el index 86721a74..5763d695 100644 --- a/Util/Emacs/boogie-mode.el +++ b/Util/Emacs/boogie-mode.el @@ -38,7 +38,7 @@ "assert" "assume" "break" "call" "then" "else" "havoc" "if" "goto" "return" "while"
"old" "forall" "exists" "lambda" "cast" "div" "mod"
"false" "true")) . font-lock-keyword-face)
- `(,(boogie-regexp-opt '("bool" "int"
+ `(,(boogie-regexp-opt '("bool" "int" "real"
"bv0" "bv1" "bv2" "bv3" "bv4" "bv5" "bv6" "bv7" "bv8" "bv9"
"bv10" "bv11" "bv12" "bv13" "bv14" "bv15" "bv16" "bv17" "bv18" "bv19"
"bv20" "bv21" "bv22" "bv23" "bv24" "bv25" "bv26" "bv27" "bv28" "bv29"
diff --git a/Util/VS2010/Boogie/BoogieLanguageService/Grammar.cs b/Util/VS2010/Boogie/BoogieLanguageService/Grammar.cs index 4e38f654..fd7c561d 100644 --- a/Util/VS2010/Boogie/BoogieLanguageService/Grammar.cs +++ b/Util/VS2010/Boogie/BoogieLanguageService/Grammar.cs @@ -33,8 +33,7 @@ namespace Demo "mod", "modifies",
"old",
"procedure",
- "requires",
- "return", "returns",
+ "real", "requires", "return", "returns",
"then", "true", "type",
"unique",
"var",
@@ -271,8 +270,7 @@ namespace Demo "modifies" |
"old" |
"procedure" |
- "requires" |
- "return" | "returns" |
+ "real" | "requires" | "return" | "returns" |
"then" | "true" | "type" |
"unique" |
"var" |
@@ -323,7 +321,7 @@ namespace Demo ;
typeDecl.Rule
- = (ToTerm("int") | "bool" | ident)
+ = (ToTerm("int") | "bool" | "real" | ident)
;
fieldDecl.Rule
diff --git a/Util/latex/boogie.sty b/Util/latex/boogie.sty index 43336262..e67c61f4 100644 --- a/Util/latex/boogie.sty +++ b/Util/latex/boogie.sty @@ -19,7 +19,7 @@ \usepackage{listings}
\lstdefinelanguage{boogie}{
- morekeywords={type,finite,bool,int,ref,%
+ morekeywords={type,bool,int,real,%
bv0,bv1,bv2,bv3,bv4,bv5,bv6,bv7,bv8,bv9,%
bv10,bv11,bv12,bv13,bv14,bv15,bv16,bv17,bv18,bv19,%
bv20,bv21,bv22,bv23,bv24,bv25,bv26,bv27,bv28,bv29,%
diff --git a/Util/vim/syntax/boogie.vim b/Util/vim/syntax/boogie.vim index 673f967e..6af66279 100644 --- a/Util/vim/syntax/boogie.vim +++ b/Util/vim/syntax/boogie.vim @@ -13,7 +13,7 @@ set cpo&vim " type -syn keyword bplType bool int +syn keyword bplType bool int real " repeat / condition / label syn keyword bplExpr forall exists cast returns lambda div mod syn keyword bplStmt goto return while call else if assert assume havoc then |