Client in eigenes Git Repo gesplittet

Author: just-me-

.github/ISSUE_TEMPLATE.md

@@ -0,0 +1,31 @@
+## Environment
+
+- VS Code version: XXX
+- Extension version (available under the Extensions sidebar): XXX
+- Dafny version (Hovertext of `Server Up` in Statusbar): XXX
+- OS and version: XXX
+- .NET / Mono Version: XXX
+
+## Expected behaviour
+
+XXX
+
+## Actual behaviour
+
+XXX
+
+## Steps to reproduce:
+1. XXX
+
+## Logs
+Output for `Dafny Language Server` in the `Output` panel (`View`→`Output`, change the drop-down the upper-right of the `Output` panel to `Dafny Language Server`)
+
+```
+XXX
+```   
+
+Output from `Console` under the `Developer Tools` panel (toggle Developer Tools on under `Help`)
+
+```
+XXX
+```

.gitignore

@@ -0,0 +1,5 @@
+/out
+/server
+/dafny
+.vscode-test
+_launch_Tom.bat

.vscode/launch.json

@@ -0,0 +1,28 @@
+// A launch configuration that compiles the extension and then opens it inside a new window
+{
+	"version": "0.1.0",
+	"configurations": [
+		{
+			"name": "Launch Extension",
+			"type": "extensionHost",
+			"request": "launch",
+			"runtimeExecutable": "${execPath}",
+			"args": ["--extensionDevelopmentPath=${workspaceRoot}" ],
+			"stopOnEntry": false,
+			"sourceMaps": true,
+			"outFiles": [ "${workspaceRoot}/out/src/**/*.js" ],
+			"preLaunchTask": "npm"
+		},
+		{
+			"name": "Launch Tests",
+			"type": "extensionHost",
+			"request": "launch",
+			"runtimeExecutable": "${execPath}",
+			"args": ["--extensionDevelopmentPath=${workspaceRoot}", "--extensionTestsPath=${workspaceRoot}/out/test" ],
+			"stopOnEntry": false,
+			"sourceMaps": true,
+			"outFiles": [ "${workspaceRoot}/out/test/**/*.js" ],
+			"preLaunchTask": "npm"
+		}
+	]
+}

.vscode/settings.json

@@ -0,0 +1,10 @@
+// Place your settings in this file to overwrite default and user settings.
+{
+	"files.exclude": {
+		"out": false // set this to true to hide the "out" folder with the compiled JS files
+	},
+	"search.exclude": {
+		"out": true // set this to false to include "out" folder in search results
+	},
+	"typescript.tsdk": "./node_modules/typescript/lib" // we want to use the TS server from our node_modules folder to control its version
+}

.vscode/symbols.json

@@ -0,0 +1 @@
+{"symbols":{"VerificationResults":{"hasNamespace":false,"type":0,"moduleName":"verificationResults","relativePath":"..\\server\\src\\backend\\verificationResults"},"DafnyServerProvider":{"hasNamespace":false,"type":0,"moduleName":"dafnyProvider","relativePath":"..\\server\\src\\frontend\\dafnyProvider"},"DafnyInstaller":{"hasNamespace":false,"type":0,"moduleName":"dafnyInstaller","relativePath":"src\\dafnyInstaller"},"DafnyClientProvider":{"hasNamespace":false,"type":0,"moduleName":"dafnyProvider","relativePath":"src\\dafnyProvider"},"Context":{"hasNamespace":false,"type":0,"moduleName":"context","relativePath":"src\\context"},"CounterModelProvider":{"hasNamespace":false,"type":0,"moduleName":"counterModelProvider","relativePath":"src\\counterModelProvider"},"DafnyRunner":{"hasNamespace":false,"type":0,"moduleName":"dafnyRunner","relativePath":"src\\dafnyRunner"},"Priority":{"hasNamespace":false,"type":0,"moduleName":"dafnyStatusbar","relativePath":"src\\dafnyStatusbar"},"Statusbar":{"hasNamespace":false,"type":0,"moduleName":"dafnyStatusbar","relativePath":"src\\dafnyStatusbar"},"DotGraphProvider":{"hasNamespace":false,"type":0,"moduleName":"dotGraphProvider","relativePath":"src\\dotGraphProvider"},"CommandFailedException":{"hasNamespace":false,"type":0,"moduleName":"errors","relativePath":"src\\errors"},"RequestFailedException":{"hasNamespace":false,"type":0,"moduleName":"errors","relativePath":"src\\errors"},"CommandEndFailedException":{"hasNamespace":false,"type":0,"moduleName":"errors","relativePath":"src\\errors"},"ByteOutOfRangeException":{"hasNamespace":false,"type":0,"moduleName":"errors","relativePath":"src\\errors"},"DafnyServerExeption":{"hasNamespace":false,"type":0,"moduleName":"errors","relativePath":"src\\errors"},"IncorrectPathExeption":{"hasNamespace":false,"type":0,"moduleName":"errors","relativePath":"src\\errors"},"DafnyUnsupportedPlatform":{"hasNamespace":false,"type":0,"moduleName":"errors","relativePath":"src\\errors"},"Severity":{"hasNamespace":false,"type":0,"moduleName":"stringRessources","relativePath":"src\\stringRessources"},"WarningMsg":{"hasNamespace":false,"type":0,"moduleName":"stringRessources","relativePath":"src\\stringRessources"},"ErrorMsg":{"hasNamespace":false,"type":0,"moduleName":"stringRessources","relativePath":"src\\stringRessources"},"Config":{"hasNamespace":false,"type":0,"moduleName":"stringRessources","relativePath":"src\\stringRessources"},"Application":{"hasNamespace":false,"type":0,"moduleName":"stringRessources","relativePath":"src\\stringRessources"},"Commands":{"hasNamespace":false,"type":0,"moduleName":"stringRessources","relativePath":"src\\stringRessources"},"InfoMsg":{"hasNamespace":false,"type":0,"moduleName":"stringRessources","relativePath":"src\\stringRessources"},"ServerStatus":{"hasNamespace":false,"type":0,"moduleName":"stringRessources","relativePath":"src\\stringRessources"},"Answer":{"hasNamespace":false,"type":0,"moduleName":"stringRessources","relativePath":"src\\stringRessources"},"EnvironmentConfig":{"hasNamespace":false,"type":0,"moduleName":"stringRessources","relativePath":"src\\stringRessources"},"StatusString":{"hasNamespace":false,"type":0,"moduleName":"stringRessources","relativePath":"src\\stringRessources"},"LanguageServerRequest":{"hasNamespace":false,"type":0,"moduleName":"stringRessources","relativePath":"src\\stringRessources"},"LanguageServerNotification":{"hasNamespace":false,"type":0,"moduleName":"stringRessources","relativePath":"src\\stringRessources"},"VerificationResult":{"hasNamespace":false,"type":0,"moduleName":"verificationResult","relativePath":"src\\verificationResult"},"UnitTestCallback":{"hasNamespace":false,"type":0,"moduleName":"extension.test","relativePath":"src\\extension.test"},"LocalQueue":{"hasNamespace":false,"type":0,"moduleName":"localQueue","relativePath":"src\\serverHelper\\localQueue"},"CompilerResult":{"hasNamespace":false,"type":0,"moduleName":"compilerResult","relativePath":"src\\serverHelper\\compilerResult"}},"files":{"src\\dafnyStatusbar.ts":"2017-06-12T06:28:20.277Z","src\\errors.ts":"2017-06-12T06:28:20.281Z","src\\stringRessources.ts":"2017-06-12T06:28:20.297Z","src\\verificationResult.ts":"2017-06-12T06:28:20.297Z","test\\extension.test.ts":"2017-06-12T06:28:20.297Z","test\\index.ts":"2017-06-12T06:28:20.297Z","src\\commands.ts":"2017-06-12T06:28:18.214Z","src\\serverHelper\\dataConversions.ts":"2017-06-12T06:28:20.281Z","..\\server\\src\\frontend\\dafnyProvider.ts":"2017-04-24T12:42:07.367Z","src\\dafnyRunner.ts":"2017-06-12T06:28:20.273Z","src\\serverHelper\\compilerResult.ts":"2017-06-12T06:28:20.281Z","src\\serverHelper\\localQueue.ts":"2017-06-12T06:28:20.281Z","src\\context.ts":"2017-06-12T06:28:18.230Z","src\\counterModelProvider.ts":"2017-06-12T06:28:18.230Z","src\\dotGraphProvider.ts":"2017-06-12T06:28:20.281Z","src\\extension.ts":"2017-06-12T06:28:20.281Z","src\\dafnyProvider.ts":"2017-06-12T06:28:20.269Z","test\\extension.test.1.ts":"2017-06-12T06:28:20.297Z","src\\extension.test.ts":"2017-06-12T06:28:20.281Z"}}

.vscode/tasks.json

@@ -0,0 +1,30 @@
+// Available variables which can be used inside of strings.
+// ${workspaceRoot}: the root folder of the team
+// ${file}: the current opened file
+// ${fileBasename}: the current opened file's basename
+// ${fileDirname}: the current opened file's dirname
+// ${fileExtname}: the current opened file's extension
+// ${cwd}: the current working directory of the spawned process
+
+// A task runner that calls a custom npm script that compiles the extension.
+{
+	"version": "0.1.0",
+
+	// we want to run npm
+	"command": "npm",
+
+	// the command is a shell script
+	"isShellCommand": true,
+
+	// show the output window only if unrecognized errors occur.
+	"showOutput": "silent",
+
+	// we run the custom script "compile" as defined in package.json
+	"args": ["run", "compile", "--loglevel", "silent"],
+
+	// The tsc compiler is started in watching mode
+	"isWatching": true,
+
+	// use the standard tsc in watch mode problem matcher to find compile problems in the output.
+	"problemMatcher": "$tsc-watch"
+}

.vscodeignore

@@ -0,0 +1,10 @@
+.vscode/**
+.vscode-test/**
+out/test/**
+test/**
+src/**
+**/*.map
+.gitignore
+tsconfig.json
+vsc-extension-quickstart.md
+dafny

CHANGELOG.md

@@ -0,0 +1,116 @@
+# Release Notes
+
+## 0.17.1
+* Correct Dafny Github repository name ([#49](https://github.com/DafnyVSCode/Dafny-VSCode/issues/49))
+* Change typescript target from es6 to es2017
+* Upgrade `js-yaml` to 3.13.1 to fix security vunerability
+* Upgrade Dafny in tests to 2.3.0
+
+## 0.17.0
+* Rename configuration option `monoPath` to `monoExecutable` ([#40](https://github.com/DafnyVSCode/Dafny-VSCode/pull/40))
+* Update deprecated API calls ([#39](https://github.com/DafnyVSCode/Dafny-VSCode/pull/39))
+* Remove deprecated Flow Graph Visualization
+* Update minimal VSCode version to 1.25.1
+* Update dependencies
+* Extension code clean up
+
+## 0.16.0
+* Allow customizing the arguments passed to the verify backend ([#42](https://github.com/DafnyVSCode/Dafny-VSCode/pull/42)).
+* Update insecure dependencies
+
+## 0.15.0
+* Change extension key from FunctionalCorrectness to correctnessLab.
+* Fix tslint errors ([#38](https://github.com/DafnyVSCode/Dafny-VSCode/pull/38)).
+
+## 0.14.3
+* Rebranding and small readme fixes.
+
+## 0.14.2
+* Add workaround for dafny counterExample bug ([#23](https://github.com/DafnyVSCode/Dafny-VSCode/issues/23)).
+
+## 0.14.1
+* Clearify mono installation message on macOS.
+* Fix incomplete copyright notice and improve contributors section in readme ([#37](https://github.com/DafnyVSCode/Dafny-VSCode/issues/37)).
+
+## 0.14.0
+* Fix installation of Dafny on some constellations on Windows ([#7](https://github.com/DafnyVSCode/Dafny-VSCode/issues/7)).
+* Check for a recent mono version on launch.
+
+## 0.13.0
+
+* Fixed the CodeLens references counter (Thanks [@GoryMoon](https://github.com/GoryMoon)!)
+* Dependencies were upgraded to prevent several vulnerabilities.
+
+## 0.12.0
+* The Dafny base path can now alternatively be set via the environment variable DAFNY_PATH.
+* Dependencies were upgraded to prevent several vulnerabilities.
+
+## 0.11.1 
+Use Dafny releases from Microsoft/dafny. Miscellaneous bug fixes.
+
+## 0.10.10
+BugFix: Decrease guard
+
+## 0.10.9
+BugFix: Rename method
+
+## 0.10.8
+Warning if no workspace is used
+Changelog 
+
+## 0.10.7 
+BugFix Ubuntu
+
+## 0.10.2 
+Added Context Menu Commands
+
+## 0.10.1 
+Manually show counterexample, flow graph
+
+## 0.10.0 
+Display counter example for failing proof. Switched to typescript implementation to download dependencies. Lots of bugfixes
+
+## 0.9.0 
+Switched to Language Server. IntelliSense for classes, compile and execute Dafny program in VSCode. QuickFix for decrease, increase and object may be null. 
+
+## 0.8.0 
+CodeLens showing method references, Go to Definition, version checking for newer Dafny release. 
+
+## 0.6.0 
+DafnyDef allows to get SymbolInformation from DafnyServer, which will allow in the future to implement Refactorings. Go to Definition is already implemented. 
+
+## 0.5.5 
+Fallback to wget, if curl is not found.
+
+## 0.5.4 
+Automatic validation as you type.  
+
+## 0.5.1 
+Smaller bugfixes. 
+
+## 0.5.0
+Automatic download and installation task on osx and ubuntu `dafny.installDafny`. Also added uninstaller `dafny.uninstallDafny`. 
+
+## 0.4.4
+Uninstall task of dafny on windows. 
+
+## 0.4.0
+Automatic download and installation task on windows. 
+
+## 0.2.0
+Full refactoring of the plugin. issues/3 from ferry~ fixed. 
+
+## 0.1.2
+Refactored/tweaked UI code, Added `dafny.restartDafnyServer` ("Restart Dafny Server") command.
+
+## 0.1.0
+Added syntax highlighting, tested on Ubuntu and OSX.
+
+## 0.0.3
+Getting `mono` from PATH when `monoPath` isn't set.
+
+## 0.0.2
+Fixed readme and license, added use animation.
+
+## 0.0.1
+Initial release, some half baked features turned off.

CodeLens.png

@@ -0,0 +1,10 @@
+MIT License
+Copyright (c) 2016 Jonathan Rosca
+Copyright (c) 2017 Markus Schaden, Rafael Krucker
+Copyright (c) 2018 Institute for Software - University of Applied Science (HSR) Rapperswil
+
+Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the "Software"), to deal in the Software without restriction, including without limitation the rights to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is furnished to do so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in all copies or substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.

Compile.png

@@ -0,0 +1,99 @@
+# Dafny for Visual Studio Code
+
+
+This extension adds _Dafny_ support to Visual Studio Code.
+
+## Features
+
+* **Compile and run `.dfy` files.**
+  * Automatic installation of the newest _Dafny_ version.
+* **Automatic verification as one types.**
+  * Errors, warnings and hints are shown through the VSCode interface.
+  * When there are no errors, you get a 👍 on the status bar.
+* **Syntax highlighting** thanks to [sublime-dafny](https://github.com/erggo/sublime-dafny). See file `LICENSE_sublime-dafny.rst` for license. 
+* **Display counter example** for failing proof.
+* _IntelliSense_ for classes and _CodeLens_ showing method references.
+
+![assertions animation](simpleassert.gif)
+
+You can find [more Examples below](#examples).
+
+## Shortcuts
+
+| Shortcut                  | Description                                                          |
+| :------------------------ |:-------------------------------------------------------------------- | 
+| `Ctrl+Shift+B` or `⇧+⌘+B` | Compile `.dfy` file to `.dll` or `.exe`, if there is a `Main` method |
+| `F5`                      | Compile and run, if the source file has a `Main` method              |
+| `F7`                      | Show _CounterExample_                                                |
+| `F8`                      | Hide _CounterExample_                                                |
+
+## Tasks
+
+Choose `Tasks -> Run Task...` to run one of the following:
+
+| Task                    | Description                                                                               |
+| :---------------------- |:----------------------------------------------------------------------------------------- | 
+| `Install DafnyServer`   | Downloads and installs the _DafnyServer_ and sets the `dafny.dafnyServerPath accordingly` |
+| `Uninstall DafnyServer` | Uninstalls the _DafnyServer_                                                              |
+| `Restart DafnyServer`   | Restarts the _DafnyServer_                                                                |
+
+## Requirements
+
+* The plugin needs a _.NET_ runtime to run the _DafnyServer_. If you are not on Windows, please download a distribution from [Mono](http://www.mono-project.com).
+  * Note: When you first open a _Dafny_ file, the extension will prompt you to automatically install _Dafny_ and Mono.
+* In case you would like the plugin to use a different _Dafny_ distribution, set the path to the `DafnyServer.exe` file via the `dafny.dafnyServerPath` user setting.
+
+## Extension Settings
+
+| Setting          | Description                              | Default          |
+| :--------------- |:---------------------------------------- |:---------------- |
+| `dafny.basePath` | Absolute path to the _Dafny_ binary directory (which contains `DafnyServer.exe`). | |
+| `dafny.monoExecutable` | Mono executable with absolute path. Only necessary if mono is not in system PATH (you'll get an error if that's the case). Ignored on Windows when `useMono` is `false`.  | |
+| `dafny.useMono` | Only applicable to _Windows_! Requires _.NET_ 4.5 or higher when set to `false`. | `false` |
+| `dafny.automaticVerification` | Verify as soon as the document is changed. When `false`, only verify on save. | `true` |
+| `dafny.automaticVerificationDelayMS` | Delay in ms to wait after a document change before verifying document. This avoids syntax errors while typing. Only relevant if `automaticVerification` is `true`. | `700` |
+| `dafny.automaticShowCounterModel` | Show _CounterModel_ automatically if a proof fails. Might cause performance issues if `true`. | `false` |
+| `dafny.serverVerifyArguments` | Additional arguments to pass to the "verify" command of the Dafny Server. E.g.`["/timeLimit:40", "/vcsLoad:1"]` | `[]` |
+
+## Examples
+
+### Installation
+On the first start the plugin asks you to install _Dafny_ automatically. 
+
+![assertions animation](installation.gif)
+
+### Syntax Error Underlining
+![Syntax](Syntax.png)
+Whenever a postcondition statement does not hold, the user will be informed.
+
+### Compile and Run
+Pressed `F5` to compile and run the program.
+
+![Compile](Compile.png)
+
+### Show Counter Example
+Pressed `F7` to show counter examples.
+
+![Counter](Counter.png)
+
+### Auto Completion
+Pressed `control + space` to show auto completion suggestions.
+
+![Completion](Completion.png)
+
+### Go to Definition
+Pressed `control + space` to show auto completion suggestions.
+
+![Go to Definition](GoTo.png)
+Press `F12` to jump to the definition. 
+
+### Add null check (coming soon) 
+Some diagnostics can be directly inserted with a quickfix at the beginning of a line.
+
+![assertions animation](addnullcheck.gif)
+
+## Contribute
+
+This is a MIT licensed open-source project that lives from code contributions. All contributors are listed in our [project readme](https://github.com/DafnyVSCode/Dafny-VSCode#contributors).
+
+We welcome your help! For a description of how you can contribute, as well as a list of issues you can work on, please visit the [Dafny-VSCode GitHub repository](https://github.com/DafnyVSCode/Dafny-VSCode#contribute).

Completion.png

@@ -0,0 +1,31 @@
+THIRD-PARTY SOFTWARE NOTICES AND INFORMATION
+For Microsoft vscode-languageserver-node-example
+ 
+This project incorporates material from the project(s) listed below (collectively, “Third Party Code”).
+Microsoft is not the original author of the Third Party Code.  The original copyright notice and license 
+under which Microsoft received such Third Party Code are set out below. This Third Party Code is licensed 
+to you under their original license terms set forth below.  Microsoft reserves all other rights not expressly 
+granted, whether by implication, estoppel or otherwise.
+ 
+1.       DefinitelyTyped version 0.0.1 (https://github.com/borisyankov/DefinitelyTyped)
+ 
+This project is licensed under the MIT license.
+Copyrights are respective of each contributor listed at the beginning of each definition file.
+ 
+Permission is hereby granted, free of charge, to any person obtaining a copy
+of this software and associated documentation files (the "Software"), to deal
+in the Software without restriction, including without limitation the rights
+to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+copies of the Software, and to permit persons to whom the Software is
+furnished to do so, subject to the following conditions:
+ 
+The above copyright notice and this permission notice shall be included in
+all copies or substantial portions of the Software.
+ 
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN
+THE SOFTWARE.