From d3a315961bf6a7b83225f6311dcf40b0dbba6463 Mon Sep 17 00:00:00 2001
From: Unknown <leino@LEINO6.redmond.corp.microsoft.com>
Date: Fri, 28 Sep 2012 16:12:27 -0700
Subject: Boogie: updated syntax highlighting ("real")

---
 Util/Emacs/boogie-mode.el                           | 2 +-
 Util/VS2010/Boogie/BoogieLanguageService/Grammar.cs | 8 +++-----
 Util/latex/boogie.sty                               | 2 +-
 Util/vim/syntax/boogie.vim                          | 2 +-
 4 files changed, 6 insertions(+), 8 deletions(-)

(limited to 'Util')

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 
-- 
cgit v1.2.3