From 2541e9de002267359897bf967755172fcc726512 Mon Sep 17 00:00:00 2001
From: Rustan Leino <leino@microsoft.com>
Date: Mon, 22 Oct 2012 02:18:51 -0700
Subject: renamed "abstract module" to "module facade" renamed "ghost module"
 to "abstract module", adding a keyword "abstract"

---
 Util/Emacs/dafny-mode.el                          | 2 +-
 Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs | 3 ++-
 Util/latex/dafny.sty                              | 2 +-
 Util/vim/syntax/dafny.vim                         | 2 +-
 4 files changed, 5 insertions(+), 4 deletions(-)

(limited to 'Util')

diff --git a/Util/Emacs/dafny-mode.el b/Util/Emacs/dafny-mode.el
index 035703cf..d1bdcf12 100644
--- a/Util/Emacs/dafny-mode.el
+++ b/Util/Emacs/dafny-mode.el
@@ -33,7 +33,7 @@
         "class" "datatype" "codatatype" "type" "iterator"
         "function" "predicate" "copredicate"
         "ghost" "var" "method" "constructor" "comethod"
-        "module" "import" "default" "as" "opened" "static" "refines"
+        "abstract" "module" "import" "default" "as" "opened" "static" "refines"
         "returns" "yields" "requires" "ensures" "modifies" "reads" "free"
         "invariant" "decreases"
         )) . font-lock-builtin-face)
diff --git a/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs b/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs
index 2c3a650e..dd910820 100644
--- a/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs
+++ b/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs
@@ -20,7 +20,7 @@ namespace Demo
           "class", "ghost", "static", "var", "method", "constructor", "comethod", "datatype", "codatatype",
           "iterator", "type",
           "assert", "assume", "new", "this", "object", "refines",
-          "module", "import", "as", "default", "opened",
+          "abstract", "module", "import", "as", "default", "opened",
           "if", "then", "else", "while", "invariant",
           "break", "label", "return", "yield", "parallel", "print",
           "returns", "yields", "requires", "ensures", "modifies", "reads", "decreases",
@@ -278,6 +278,7 @@ namespace Demo
           | "this"
           | "object"
           | "refines"
+          | "abstract"
           | "module"
           | "import"
           | "default"
diff --git a/Util/latex/dafny.sty b/Util/latex/dafny.sty
index 8ac9defe..4a3f6dbc 100644
--- a/Util/latex/dafny.sty
+++ b/Util/latex/dafny.sty
@@ -10,7 +10,7 @@
       function,predicate,copredicate,
       ghost,var,static,refines,
       method,constructor,comethod,
-      returns,yields,module,import,default,opened,as,in,
+      returns,yields,abstract,module,import,default,opened,as,in,
       requires,modifies,ensures,reads,decreases,free,
       % expressions
       match,case,false,true,null,old,fresh,choose,this,
diff --git a/Util/vim/syntax/dafny.vim b/Util/vim/syntax/dafny.vim
index fc98156a..b329f0f7 100644
--- a/Util/vim/syntax/dafny.vim
+++ b/Util/vim/syntax/dafny.vim
@@ -8,7 +8,7 @@ syntax case match
 syntax keyword dafnyFunction function predicate copredicate
 syntax keyword method constructor comethod
 syntax keyword dafnyTypeDef class datatype codatatype type iterator
-syntax keyword module import opened as default
+syntax keyword abstract module import opened as default
 syntax keyword dafnyConditional if then else match case 
 syntax keyword dafnyRepeat while parallel
 syntax keyword dafnyStatement assume assert return yield new print break label where calc
-- 
cgit v1.2.3