renamed "abstract module" to "module facade"

renamed "ghost module" to "abstract module", adding a keyword "abstract"

4 files changed, 5 insertions, 4 deletions

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