diff options
Diffstat (limited to 'Util')
| -rw-r--r-- | Util/Emacs/dafny-mode.el | 6 | ||||
| -rw-r--r-- | Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs | 10 | ||||
| -rw-r--r-- | Util/VS2010/DafnyExtension/DafnyExtension/IdentifierTagger.cs | 20 | ||||
| -rw-r--r-- | Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs | 3 | ||||
| -rw-r--r-- | Util/latex/dafny.sty | 8 | ||||
| -rw-r--r-- | Util/vim/syntax/dafny.vim | 7 |
6 files changed, 35 insertions, 19 deletions
diff --git a/Util/Emacs/dafny-mode.el b/Util/Emacs/dafny-mode.el index 1e197644..1ba6186b 100644 --- a/Util/Emacs/dafny-mode.el +++ b/Util/Emacs/dafny-mode.el @@ -31,13 +31,15 @@ `(,(dafny-regexp-opt '(
"class" "datatype" "codatatype" "type" "function" "predicate" "copredicate"
+ "iterator"
"ghost" "var" "method" "constructor"
"module" "import" "default" "as" "opened" "static" "refines"
- "returns" "requires" "ensures" "modifies" "reads" "free"
+ "returns" "yields" "requires" "ensures" "modifies" "reads" "free"
"invariant" "decreases"
)) . font-lock-builtin-face)
`(,(dafny-regexp-opt '(
- "assert" "assume" "break" "choose" "then" "else" "if" "label" "return" "while" "print" "where"
+ "assert" "assume" "break" "choose" "then" "else" "if" "label" "return" "yield"
+ "while" "print" "where"
"old" "forall" "exists" "new" "parallel" "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)
diff --git a/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs b/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs index 8c3eee59..ac1b755c 100644 --- a/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs +++ b/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs @@ -17,12 +17,13 @@ namespace Demo StringLiteral stringLiteral = TerminalFactory.CreateCSharpString("String");
this.MarkReservedWords( // NOTE: these keywords must also appear once more below
- "class", "ghost", "static", "var", "method", "constructor", "datatype", "codatatype", "type",
+ "class", "ghost", "static", "var", "method", "constructor", "datatype", "codatatype",
+ "iterator", "type",
"assert", "assume", "new", "this", "object", "refines",
"module", "import", "as", "default", "opened",
"if", "then", "else", "while", "invariant",
- "break", "label", "return", "parallel", "print",
- "returns", "requires", "ensures", "modifies", "reads", "decreases",
+ "break", "label", "return", "yield", "parallel", "print",
+ "returns", "yields", "requires", "ensures", "modifies", "reads", "decreases",
"bool", "nat", "int", "false", "true", "null",
"function", "predicate", "copredicate", "free",
"in", "forall", "exists",
@@ -269,6 +270,7 @@ namespace Demo | "datatype"
| "codatatype"
| "type"
+ | "iterator"
| "assert"
| "assume"
| "new"
@@ -288,10 +290,12 @@ namespace Demo | "break"
| "label"
| "return"
+ | "yield"
| "parallel"
| "calc"
| "print"
| "returns"
+ | "yields"
| "requires"
| "ensures"
| "modifies"
diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/IdentifierTagger.cs b/Util/VS2010/DafnyExtension/DafnyExtension/IdentifierTagger.cs index 80a6dbb5..5ecc8dc2 100644 --- a/Util/VS2010/DafnyExtension/DafnyExtension/IdentifierTagger.cs +++ b/Util/VS2010/DafnyExtension/DafnyExtension/IdentifierTagger.cs @@ -139,7 +139,7 @@ namespace DafnyLanguage foreach (var ctor in dt.Ctors) {
foreach (var dtor in ctor.Destructors) {
if (dtor != null) {
- IdRegion.Add(newRegions, dtor.tok, dtor, "destructor", true, module);
+ IdRegion.Add(newRegions, dtor.tok, dtor, null, "destructor", true, module);
}
}
}
@@ -175,7 +175,7 @@ namespace DafnyLanguage }
} else if (member is Field) {
var fld = (Field)member;
- IdRegion.Add(newRegions, fld.tok, fld, "field", true, module);
+ IdRegion.Add(newRegions, fld.tok, fld, null, "field", true, module);
}
}
}
@@ -194,7 +194,8 @@ namespace DafnyLanguage ExprRegions(fe.E, regions, module);
}
if (fe.Field != null) {
- IdRegion.Add(regions, fe.tok, fe.Field, "field", false, module);
+ Microsoft.Dafny.Type showType = null; // TODO: if we had the instantiated type of this field, that would have been nice to use here (but the Resolver currently does not compute or store the instantiated type for a FrameExpression)
+ IdRegion.Add(regions, fe.tok, fe.Field, showType, "field", false, module);
}
}
@@ -206,7 +207,7 @@ namespace DafnyLanguage IdRegion.Add(regions, e.tok, e.Var, false, module);
} else if (expr is FieldSelectExpr) {
var e = (FieldSelectExpr)expr;
- IdRegion.Add(regions, e.tok, e.Field, "field", false, module);
+ IdRegion.Add(regions, e.tok, e.Field, e.Type, "field", false, module);
} else if (expr is ComprehensionExpr) {
var e = (ComprehensionExpr)expr;
foreach (var bv in e.BoundVars) {
@@ -298,13 +299,13 @@ namespace DafnyLanguage regions.Add(new IdRegion(tok, v, isDefinition, context));
}
}
- public static void Add(List<IdRegion> regions, Bpl.IToken tok, Field decl, string kind, bool isDefinition, ModuleDefinition context) {
+ public static void Add(List<IdRegion> regions, Bpl.IToken tok, Field decl, Microsoft.Dafny.Type showType, string kind, bool isDefinition, ModuleDefinition context) {
Contract.Requires(regions != null);
Contract.Requires(tok != null);
Contract.Requires(decl != null);
Contract.Requires(kind != null);
if (SurfaceSyntaxToken(tok)) {
- regions.Add(new IdRegion(tok, decl, kind, isDefinition, context));
+ regions.Add(new IdRegion(tok, decl, showType, kind, isDefinition, context));
}
}
@@ -325,13 +326,16 @@ namespace DafnyLanguage HoverText = string.Format("({2}{3}) {0}: {1}", v.DisplayName, v.Type.TypeName(context), v.IsGhost ? "ghost " : "", kind);
Kind = !isDefinition ? OccurrenceKind.Use : VarDecl.HasWildcardName(v) ? OccurrenceKind.WildDefinition : OccurrenceKind.Definition;
}
- private IdRegion(Bpl.IToken tok, Field decl, string kind, bool isDefinition, ModuleDefinition context) {
+ private IdRegion(Bpl.IToken tok, Field decl, Microsoft.Dafny.Type showType, string kind, bool isDefinition, ModuleDefinition context) {
Contract.Requires(tok != null);
Contract.Requires(decl != null);
Contract.Requires(kind != null);
+ if (showType == null) {
+ showType = decl.Type;
+ }
Start = tok.pos;
Length = decl.Name.Length;
- HoverText = string.Format("({2}{3}) {0}: {1}", decl.FullNameInContext(context), decl.Type.TypeName(context), decl.IsGhost ? "ghost " : "", kind);
+ HoverText = string.Format("({2}{3}) {0}: {1}", decl.FullNameInContext(context), showType.TypeName(context), decl.IsGhost ? "ghost " : "", kind);
Kind = !isDefinition ? OccurrenceKind.Use : OccurrenceKind.Definition;
}
}
diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs b/Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs index ec1514ae..2f295429 100644 --- a/Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs +++ b/Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs @@ -255,6 +255,7 @@ namespace DafnyLanguage case "in":
case "int":
case "invariant":
+ case "iterator":
case "label":
case "match":
case "method":
@@ -285,6 +286,8 @@ namespace DafnyLanguage case "type":
case "var":
case "while":
+ case "yield":
+ case "yields":
#endregion
break;
default:
diff --git a/Util/latex/dafny.sty b/Util/latex/dafny.sty index d60488d1..879b90cb 100644 --- a/Util/latex/dafny.sty +++ b/Util/latex/dafny.sty @@ -5,15 +5,17 @@ \usepackage{listings}
\lstdefinelanguage{dafny}{
- morekeywords={class,datatype,codatatype,type,bool,nat,int,object,set,multiset,seq,array,array2,array3,map,%
+ morekeywords={class,datatype,codatatype,type,iterator,
+ bool,nat,int,object,set,multiset,seq,array,array2,array3,map,
function,predicate,copredicate,
ghost,var,static,refines,
- method,constructor,returns,module,import,default,opened,as,in,
+ method,constructor,returns,yields,module,import,default,opened,as,in,
requires,modifies,ensures,reads,decreases,free,
% expressions
match,case,false,true,null,old,fresh,choose,this,
% statements
- assert,assume,print,new,if,then,else,while,invariant,break,label,return,parallel,where,calc
+ assert,assume,print,new,if,then,else,while,invariant,break,label,return,yield,
+ parallel,where,calc
},
literate=%
{:}{$\colon$}1
diff --git a/Util/vim/syntax/dafny.vim b/Util/vim/syntax/dafny.vim index cc1c9d79..45afbcf0 100644 --- a/Util/vim/syntax/dafny.vim +++ b/Util/vim/syntax/dafny.vim @@ -6,11 +6,12 @@ syntax clear syntax case match syntax keyword dafnyFunction function predicate copredicate method constructor -syntax keyword dafnyTypeDef class datatype codatatype type module import opened as default +syntax keyword dafnyTypeDef class datatype codatatype type iterator +syntax keyword module import opened as default syntax keyword dafnyConditional if then else match case syntax keyword dafnyRepeat while parallel -syntax keyword dafnyStatement assume assert return new print break label where calc -syntax keyword dafnyKeyword var ghost returns null static this refines +syntax keyword dafnyStatement assume assert return yield new print break label where calc +syntax keyword dafnyKeyword var ghost returns yields null static this refines syntax keyword dafnyType bool nat int seq set multiset object array array2 array3 map syntax keyword dafnyLogic requires ensures modifies reads decreases invariant syntax keyword dafnyOperator forall exists old fresh choose |