From 6897d8be8a9c5ebef140398f682021acfea393bb Mon Sep 17 00:00:00 2001
From: Rustan Leino <unknown>
Date: Thu, 13 Feb 2014 20:00:42 -0800
Subject: Syntax highlighting for reals

---
 Source/DafnyExtension/TokenTagger.cs | 1 +
 Util/Emacs/dafny-mode.el             | 2 +-
 Util/latex/dafny.sty                 | 2 +-
 Util/vim/dafny.vim                   | 2 +-
 4 files changed, 4 insertions(+), 3 deletions(-)

diff --git a/Source/DafnyExtension/TokenTagger.cs b/Source/DafnyExtension/TokenTagger.cs
index b17fe7db..88f956bd 100644
--- a/Source/DafnyExtension/TokenTagger.cs
+++ b/Source/DafnyExtension/TokenTagger.cs
@@ -303,6 +303,7 @@ namespace DafnyLanguage
                 case "predicate":
                 case "print":
                 case "reads":
+                case "real":
                 case "refines":
                 case "requires":
                 case "return":
diff --git a/Util/Emacs/dafny-mode.el b/Util/Emacs/dafny-mode.el
index 204dec45..c77fed74 100644
--- a/Util/Emacs/dafny-mode.el
+++ b/Util/Emacs/dafny-mode.el
@@ -42,7 +42,7 @@
         "while" "print" "where"
         "old" "forall" "exists" "new" "calc" "in" "this" "fresh"
         "match" "case" "false" "true" "null")) . font-lock-keyword-face)
-   `(,(dafny-regexp-opt '("array" "array2" "array3" "bool" "multiset" "map" "nat" "int" "object" "set" "seq")) . font-lock-type-face)
+   `(,(dafny-regexp-opt '("array" "array2" "array3" "bool" "multiset" "map" "nat" "int" "real" "object" "set" "seq")) . font-lock-type-face)
    )
   "Minimal highlighting for Dafny mode")
 
diff --git a/Util/latex/dafny.sty b/Util/latex/dafny.sty
index 56b92a1e..d4624def 100644
--- a/Util/latex/dafny.sty
+++ b/Util/latex/dafny.sty
@@ -6,7 +6,7 @@
 
 \lstdefinelanguage{dafny}{
   morekeywords={class,datatype,codatatype,type,iterator,
-      bool,nat,int,object,set,multiset,seq,array,array2,array3,map,
+      bool,nat,int,real,object,set,multiset,seq,array,array2,array3,map,
       function,predicate,copredicate,
       ghost,var,static,refines,
       method,lemma,constructor,comethod,colemma,
diff --git a/Util/vim/dafny.vim b/Util/vim/dafny.vim
index ad6839aa..06e1252e 100644
--- a/Util/vim/dafny.vim
+++ b/Util/vim/dafny.vim
@@ -13,7 +13,7 @@ syntax keyword dafnyConditional if then else match case
 syntax keyword dafnyRepeat while
 syntax keyword dafnyStatement assume assert return yield new print break label where calc
 syntax keyword dafnyKeyword var ghost returns yields null static this refines include
-syntax keyword dafnyType bool nat int seq set multiset object array array2 array3 map
+syntax keyword dafnyType bool nat int real seq set multiset object array array2 array3 map
 syntax keyword dafnyLogic requires ensures modifies reads decreases invariant 
 syntax keyword dafnyOperator forall exists old fresh
 syntax keyword dafnyBoolean true false
-- 
cgit v1.2.3