summaryrefslogtreecommitdiff
path: root/Source/DafnyExtension
Commit message (Collapse)AuthorAge
* Discard error messages that refer to a non-nested TokenWrapper.Gravatar Clément Pit--Claudel2015-08-20
| | | | | | | | The VS extension already did that, but it also filtered out nested tokens. That prevented info about triggers from being reported. Other interfaces (the CLI and Emacs, in particular) should have the same ability. Surprinsingly, this doesn't cause any tests failures.
* Enable unicode output in the VS extensionGravatar Clément Pit--Claudel2015-08-19
|
* Refactor the error reporting codeGravatar Clément Pit--Claudel2015-08-18
| | | | | The new error reporting system has a simpler interface, isn't tied to the resolver, and contains error source information.
* Tiny refactoring in the extension's driverGravatar Clément Pit--Claudel2015-07-31
|
* Fix an issue with column numbers in the VS extensionGravatar Clément Pit--Claudel2015-07-31
| | | | | | The error came from the fact that Dafny now consistently used 0-based indexing. Boogie gets its traces from text that's inserted by Dafny in the Boogie file, so there's no need to apply an extra offset in the VS extension.
* Update the VS extension to use the error interface defined in 576eac2e17ffGravatar Clément Pit--Claudel2015-07-29
|
* Update DafnyExtension to use the parser constructor introduced in d2e394fc4b93Gravatar Clément Pit--Claudel2015-07-24
|
* Fix: Visual studio did not show warnings.Gravatar Clément Pit--Claudel2015-07-23
| | | | | To check if the fix works, try declaring a static top level function. Initial work on this patch by Rustan
* Fix identifiers in nested match patterns not showing in the IDE bug. RememberGravatar qunyanm2015-06-29
| | | | | BoundVars that are combined in rewriting of the nested match patterns so they show up in the IDE correctly.
* Added {:auto_generated} trigger, which indicates that a declaration was not ↵Gravatar Rustan Leino2015-06-02
| | | | explicitly mentioned in the input. This lets the Dafny IDE know not to add hovertext for these declarations.
* Add an infinite set collection type.Gravatar qunyanm2015-05-29
|
* DafnyExtension: Added experimental support for diagnosing timeouts.Gravatar wuestholz2015-05-18
|
* Added inductive predicatesGravatar leino2015-05-06
|
* Changed version to 1.9.3.20406 and updated copyright year to include 2015.Gravatar leino2015-04-06
|
* Copy z3.exe and Z3-LICENSE.txt (from Binaries directory to ↵Gravatar leino2015-04-06
| | | | Source/DafnyExtension directory) as pre-build events
* Add z3.exe and z3-license.txt to dafny binary and extension distribution.Gravatar qunyanm2015-04-06
|
* Remove unneeded reference from DafnyExtension.csproj (accidentally added by ↵Gravatar chrishaw2015-03-11
| | | | my previous checkin)
* Add DafnyOptions.txt, and have the Dafny Visual Studio extension read ↵Gravatar chrishaw2015-03-11
| | | | command-line options from DafnyOptions.txt during initialization. DafnyOptions.txt gets built into the VSIX file and is installed as part of the Dafny Visual Studio extension.
* Added 'protected' keyword (syntax)Gravatar leino2015-03-07
|
* Add imap keyword to VS/emacs/vim/latex filesGravatar chrishaw2015-02-26
|
* DafnyExtension: Made it use the more advanced on-demand re-verification by ↵Gravatar wuestholz2015-01-26
| | | | default.
* When ambiguous references all resolve to the same declaration, don't complainGravatar leino2015-01-09
|
* Fixed range bug that was causing extension to sometimes crashGravatar Bryan Parno2014-10-27
|
* Ensure that no file is processed twice, even if one command-line file is ↵Gravatar Bryan Parno2014-10-27
| | | | included by another command-line file.
* MergeGravatar leino2014-10-20
|\
* | Added types "char" and "string" (the latter being a synonym for "seq<char>").Gravatar leino2014-10-20
| | | | | | | | | | | | Added string literals with various escapes--a subset of those supported in C# and similar languages, including the C# verbatim strings. Previously, the "print" statement and custom attributes could support expression-or-string arguments; there is no longer a need to special-case these, so these arguments are now just expressions. Fixed lack of operator resolution in custom attributes.
| * DafnyExtension: Fixed minor issue in the menu.Gravatar wuestholz2014-10-19
|/
* MergeGravatar leino2014-09-29
|\
* | Shorter wait-for-idle time in the Dafny IDEGravatar leino2014-09-29
| |
| * DafnyExtension: Made it not log the pretty-printed program.Gravatar wuestholz2014-09-28
| |
| * DafnyExtension: minor change due to change in BoogieGravatar wuestholz2014-09-28
| |
| * Did more refactoring.Gravatar wuestholz2014-09-23
| |
| * Did more refactoring.Gravatar wuestholz2014-09-23
| |
| * DafnyExtension: minor changeGravatar wuestholz2014-09-22
|/
* Various resolution fixes and improvementsGravatar leino2014-08-26
| | | | | Added IsGoodHeap antecedent in (exists heap ...) in newtype Is axioms. Added IDE tool tips in newtype constraints.
* Changed syntax of derived types to "newtype"Gravatar leino2014-08-21
| | | | Added parsing of constraints (beyond parsing is yet to come)
* Forget the extra copy of DafnyRuntime.cs that gets copied into DafnyExtensionGravatar Rustan Leino2014-08-12
|
* MergeGravatar Dan Rosén2014-08-11
|\
* | Add higher-order-functions and some other goodiesGravatar Dan Rosén2014-08-11
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | * The reads clause now needs to be self framing. * The requires clause now needs to be framed by the reads clause. * There are one-shot lambdas, with a single arrow, but they will probably be removed. * There is a {:heapQuantifier} attribute to quantifiers, but they will probably be removed. * Add smart handling of type variables * Add < and > for datatype & type parameter
| * MergeGravatar leino2014-08-02
| |\
| * | Fixed bug Issue 37: expand type synonyms in more (hopefully all) places in ↵Gravatar leino2014-08-02
|/ / | | | | | | the resolver and translator
| * added trait feature:Gravatar Reza Ahmadi2014-07-18
|/ | | | | | -possibility to declare traits in Dafny -possibility to extend a class by a trait -possibility to override body-less methods
* Fixed build break from recent changeGravatar leino2014-07-15
|
* Worked on the more advanced verification result caching.Gravatar wuestholz2014-07-10
|
* Worked on the more advanced verification result caching.Gravatar wuestholz2014-07-09
|
* Build VS Extension for both VS 2012 and VS 2013.Gravatar Rustan Leino2014-07-08
| | | | Currently builds only in VS 2012. To build in VS 2013, change MinimumVisualStudioVersion from 11.0 to 12.0 in these two .csproj files.
* MergeGravatar Dan Rosén2014-07-07
|\
| * DafnyExtension: Worked on adding support for Visual Studio 2013.Gravatar wuestholz2014-07-02
| |
| * Dispose DafnyTokenTaggerGravatar Rustan Leino2014-07-01
| |
| * Color nested comments correctly in the Dafny IDEGravatar Rustan Leino2014-07-01
| |
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-01 19:25:50 +0000