From c819fabbb8da669952cb7e2e5937c73ff6dcfabe Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Tue, 5 Mar 2013 16:58:16 -0800 Subject: Removed Dafny, Jennisys, Chalice, and BCT, which now live in different Codeplex repositories. --- Util/BoogieBuildAndTest.cmd | 27 ++ Util/BoogieDafnyBuildandTest.cmd | 35 -- Util/Emacs/chalice-mode.el | 118 ------ Util/Emacs/dafny-mode.el | 116 ------ Util/Emacs/jennisys-mode.el | 113 ------ Util/VS2010/Chalice/ChaliceLanguageService.sln | 20 - .../ChaliceLanguageService.csproj | 179 --------- .../ChaliceLanguageService/Configuration.cs | 24 -- .../ChaliceLanguageService/GlobalSuppressions.cs | 11 - .../Chalice/ChaliceLanguageService/Grammar.cs | 399 -------------------- .../VS2010/Chalice/ChaliceLanguageService/Guids.cs | 13 - .../Integration/AuthoringScope.cs | 66 ---- .../Integration/Configuration.cs | 116 ------ .../Integration/Declaration.cs | 30 -- .../Integration/Declarations.cs | 56 --- .../Integration/IASTResolver.cs | 13 - .../Integration/IronyLanguageService.cs | 347 ----------------- .../Integration/IronyViewFilter.cs | 42 --- .../Integration/LineScanner.cs | 58 --- .../ChaliceLanguageService/Integration/Method.cs | 20 - .../ChaliceLanguageService/Integration/Methods.cs | 50 --- .../ChaliceLanguageService/Integration/Package.cs | 130 ------- .../ChaliceLanguageService/Integration/Resolver.cs | 50 --- .../ChaliceLanguageService/Integration/Source.cs | 41 -- .../IronyLanguageServicePackage.cs | 91 ----- Util/VS2010/Chalice/ChaliceLanguageService/Key.snk | Bin 596 -> 0 bytes .../Properties/AssemblyInfo.cs | 36 -- .../ChaliceLanguageService/Resources.Designer.cs | 63 ---- .../Chalice/ChaliceLanguageService/Resources.resx | 130 ------- .../ChaliceLanguageService/Resources/Irony.dll | Bin 236032 -> 0 bytes .../Chalice/ChaliceLanguageService/VSPackage.resx | 129 ------- .../source.extension.vsixmanifest | 27 -- Util/VS2010/Chalice/StartChalice.bat | 10 - Util/VS2010/Dafny/DafnyLanguageService.sln | 20 - .../Dafny/DafnyLanguageService/Configuration.cs | 24 -- .../DafnyLanguageService.csproj | 179 --------- .../DafnyLanguageService/GlobalSuppressions.cs | 11 - Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs | 388 ------------------- Util/VS2010/Dafny/DafnyLanguageService/Guids.cs | 13 - .../Integration/AuthoringScope.cs | 66 ---- .../Integration/Configuration.cs | 116 ------ .../Integration/Declaration.cs | 30 -- .../Integration/Declarations.cs | 56 --- .../Integration/IASTResolver.cs | 13 - .../Integration/IronyLanguageService.cs | 373 ------------------ .../Integration/IronyViewFilter.cs | 42 --- .../Integration/LineScanner.cs | 58 --- .../DafnyLanguageService/Integration/Method.cs | 20 - .../DafnyLanguageService/Integration/Methods.cs | 50 --- .../DafnyLanguageService/Integration/Package.cs | 130 ------- .../DafnyLanguageService/Integration/Resolver.cs | 50 --- .../DafnyLanguageService/Integration/Source.cs | 41 -- .../IronyLanguageServicePackage.cs | 90 ----- Util/VS2010/Dafny/DafnyLanguageService/Key.snk | Bin 596 -> 0 bytes .../Properties/AssemblyInfo.cs | 36 -- .../DafnyLanguageService/Resources.Designer.cs | 63 ---- .../Dafny/DafnyLanguageService/Resources.resx | 130 ------- .../Dafny/DafnyLanguageService/Resources/Irony.dll | Bin 236032 -> 0 bytes .../Dafny/DafnyLanguageService/VSPackage.resx | 129 ------- .../source.extension.vsixmanifest | 27 -- Util/VS2010/Dafny/StartDafny.bat | 10 - Util/VS2010/DafnyExtension/DafnyExtension.sln | 20 - .../DafnyExtension/DafnyExtension/BraceMatching.cs | 253 ------------- .../DafnyExtension/BufferIdleEventUtil.cs | 155 -------- .../DafnyExtension/ClassificationTagger.cs | 107 ------ .../DafnyExtension/DafnyExtension/ContentType.cs | 18 - .../DafnyExtension/DafnyExtension/DafnyDriver.cs | 419 --------------------- .../DafnyExtension/DafnyExtension.csproj | 191 ---------- .../DafnyExtension/DafnyExtension/ErrorTagger.cs | 85 ----- .../DafnyExtension/DafnyExtension/HoverText.cs | 126 ------- .../DafnyExtension/IdentifierTagger.cs | 344 ----------------- .../DafnyExtension/OutliningTagger.cs | 185 --------- .../DafnyExtension/ProgressMargin.cs | 260 ------------- .../DafnyExtension/Properties/AssemblyInfo.cs | 33 -- .../DafnyExtension/ResolverTagger.cs | 321 ---------------- .../DafnyExtension/DafnyExtension/TokenTagger.cs | 342 ----------------- .../DafnyExtension/WordHighlighter.cs | 211 ----------- .../DafnyExtension/source.extension.vsixmanifest | 25 -- Util/latex/chalice.sty | 63 ---- Util/latex/dafny.sty | 110 ------ Util/vim/syntax/chalice.vim | 44 --- Util/vim/syntax/dafny.vim | 44 --- 82 files changed, 27 insertions(+), 8054 deletions(-) create mode 100644 Util/BoogieBuildAndTest.cmd delete mode 100644 Util/BoogieDafnyBuildandTest.cmd delete mode 100644 Util/Emacs/chalice-mode.el delete mode 100644 Util/Emacs/dafny-mode.el delete mode 100644 Util/Emacs/jennisys-mode.el delete mode 100644 Util/VS2010/Chalice/ChaliceLanguageService.sln delete mode 100644 Util/VS2010/Chalice/ChaliceLanguageService/ChaliceLanguageService.csproj delete mode 100644 Util/VS2010/Chalice/ChaliceLanguageService/Configuration.cs delete mode 100644 Util/VS2010/Chalice/ChaliceLanguageService/GlobalSuppressions.cs delete mode 100644 Util/VS2010/Chalice/ChaliceLanguageService/Grammar.cs delete mode 100644 Util/VS2010/Chalice/ChaliceLanguageService/Guids.cs delete mode 100644 Util/VS2010/Chalice/ChaliceLanguageService/Integration/AuthoringScope.cs delete mode 100644 Util/VS2010/Chalice/ChaliceLanguageService/Integration/Configuration.cs delete mode 100644 Util/VS2010/Chalice/ChaliceLanguageService/Integration/Declaration.cs delete mode 100644 Util/VS2010/Chalice/ChaliceLanguageService/Integration/Declarations.cs delete mode 100644 Util/VS2010/Chalice/ChaliceLanguageService/Integration/IASTResolver.cs delete mode 100644 Util/VS2010/Chalice/ChaliceLanguageService/Integration/IronyLanguageService.cs delete mode 100644 Util/VS2010/Chalice/ChaliceLanguageService/Integration/IronyViewFilter.cs delete mode 100644 Util/VS2010/Chalice/ChaliceLanguageService/Integration/LineScanner.cs delete mode 100644 Util/VS2010/Chalice/ChaliceLanguageService/Integration/Method.cs delete mode 100644 Util/VS2010/Chalice/ChaliceLanguageService/Integration/Methods.cs delete mode 100644 Util/VS2010/Chalice/ChaliceLanguageService/Integration/Package.cs delete mode 100644 Util/VS2010/Chalice/ChaliceLanguageService/Integration/Resolver.cs delete mode 100644 Util/VS2010/Chalice/ChaliceLanguageService/Integration/Source.cs delete mode 100644 Util/VS2010/Chalice/ChaliceLanguageService/IronyLanguageServicePackage.cs delete mode 100644 Util/VS2010/Chalice/ChaliceLanguageService/Key.snk delete mode 100644 Util/VS2010/Chalice/ChaliceLanguageService/Properties/AssemblyInfo.cs delete mode 100644 Util/VS2010/Chalice/ChaliceLanguageService/Resources.Designer.cs delete mode 100644 Util/VS2010/Chalice/ChaliceLanguageService/Resources.resx delete mode 100644 Util/VS2010/Chalice/ChaliceLanguageService/Resources/Irony.dll delete mode 100644 Util/VS2010/Chalice/ChaliceLanguageService/VSPackage.resx delete mode 100644 Util/VS2010/Chalice/ChaliceLanguageService/source.extension.vsixmanifest delete mode 100644 Util/VS2010/Chalice/StartChalice.bat delete mode 100644 Util/VS2010/Dafny/DafnyLanguageService.sln delete mode 100644 Util/VS2010/Dafny/DafnyLanguageService/Configuration.cs delete mode 100644 Util/VS2010/Dafny/DafnyLanguageService/DafnyLanguageService.csproj delete mode 100644 Util/VS2010/Dafny/DafnyLanguageService/GlobalSuppressions.cs delete mode 100644 Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs delete mode 100644 Util/VS2010/Dafny/DafnyLanguageService/Guids.cs delete mode 100644 Util/VS2010/Dafny/DafnyLanguageService/Integration/AuthoringScope.cs delete mode 100644 Util/VS2010/Dafny/DafnyLanguageService/Integration/Configuration.cs delete mode 100644 Util/VS2010/Dafny/DafnyLanguageService/Integration/Declaration.cs delete mode 100644 Util/VS2010/Dafny/DafnyLanguageService/Integration/Declarations.cs delete mode 100644 Util/VS2010/Dafny/DafnyLanguageService/Integration/IASTResolver.cs delete mode 100644 Util/VS2010/Dafny/DafnyLanguageService/Integration/IronyLanguageService.cs delete mode 100644 Util/VS2010/Dafny/DafnyLanguageService/Integration/IronyViewFilter.cs delete mode 100644 Util/VS2010/Dafny/DafnyLanguageService/Integration/LineScanner.cs delete mode 100644 Util/VS2010/Dafny/DafnyLanguageService/Integration/Method.cs delete mode 100644 Util/VS2010/Dafny/DafnyLanguageService/Integration/Methods.cs delete mode 100644 Util/VS2010/Dafny/DafnyLanguageService/Integration/Package.cs delete mode 100644 Util/VS2010/Dafny/DafnyLanguageService/Integration/Resolver.cs delete mode 100644 Util/VS2010/Dafny/DafnyLanguageService/Integration/Source.cs delete mode 100644 Util/VS2010/Dafny/DafnyLanguageService/IronyLanguageServicePackage.cs delete mode 100644 Util/VS2010/Dafny/DafnyLanguageService/Key.snk delete mode 100644 Util/VS2010/Dafny/DafnyLanguageService/Properties/AssemblyInfo.cs delete mode 100644 Util/VS2010/Dafny/DafnyLanguageService/Resources.Designer.cs delete mode 100644 Util/VS2010/Dafny/DafnyLanguageService/Resources.resx delete mode 100644 Util/VS2010/Dafny/DafnyLanguageService/Resources/Irony.dll delete mode 100644 Util/VS2010/Dafny/DafnyLanguageService/VSPackage.resx delete mode 100644 Util/VS2010/Dafny/DafnyLanguageService/source.extension.vsixmanifest delete mode 100644 Util/VS2010/Dafny/StartDafny.bat delete mode 100644 Util/VS2010/DafnyExtension/DafnyExtension.sln delete mode 100644 Util/VS2010/DafnyExtension/DafnyExtension/BraceMatching.cs delete mode 100644 Util/VS2010/DafnyExtension/DafnyExtension/BufferIdleEventUtil.cs delete mode 100644 Util/VS2010/DafnyExtension/DafnyExtension/ClassificationTagger.cs delete mode 100644 Util/VS2010/DafnyExtension/DafnyExtension/ContentType.cs delete mode 100644 Util/VS2010/DafnyExtension/DafnyExtension/DafnyDriver.cs delete mode 100644 Util/VS2010/DafnyExtension/DafnyExtension/DafnyExtension.csproj delete mode 100644 Util/VS2010/DafnyExtension/DafnyExtension/ErrorTagger.cs delete mode 100644 Util/VS2010/DafnyExtension/DafnyExtension/HoverText.cs delete mode 100644 Util/VS2010/DafnyExtension/DafnyExtension/IdentifierTagger.cs delete mode 100644 Util/VS2010/DafnyExtension/DafnyExtension/OutliningTagger.cs delete mode 100644 Util/VS2010/DafnyExtension/DafnyExtension/ProgressMargin.cs delete mode 100644 Util/VS2010/DafnyExtension/DafnyExtension/Properties/AssemblyInfo.cs delete mode 100644 Util/VS2010/DafnyExtension/DafnyExtension/ResolverTagger.cs delete mode 100644 Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs delete mode 100644 Util/VS2010/DafnyExtension/DafnyExtension/WordHighlighter.cs delete mode 100644 Util/VS2010/DafnyExtension/DafnyExtension/source.extension.vsixmanifest delete mode 100644 Util/latex/chalice.sty delete mode 100644 Util/latex/dafny.sty delete mode 100644 Util/vim/syntax/chalice.vim delete mode 100644 Util/vim/syntax/dafny.vim (limited to 'Util') diff --git a/Util/BoogieBuildAndTest.cmd b/Util/BoogieBuildAndTest.cmd new file mode 100644 index 00000000..08d5baeb --- /dev/null +++ b/Util/BoogieBuildAndTest.cmd @@ -0,0 +1,27 @@ +@echo off +pushd ..\test +goto Cleanandbuild + +:Cleanandbuild +cls +@echo on +devenv ..\Source\Boogie.sln /Clean +@echo off +if errorlevel 1 goto fail +@echo on +devenv ..\source\Boogie.sln /Build +@echo off +if errorlevel 1 goto fail +goto reg + +:Reg +cls +call runtestall +goto end + +:fail +echo Some part of the rebuild failed. +goto end + +:end +popd \ No newline at end of file diff --git a/Util/BoogieDafnyBuildandTest.cmd b/Util/BoogieDafnyBuildandTest.cmd deleted file mode 100644 index 97bf32ce..00000000 --- a/Util/BoogieDafnyBuildandTest.cmd +++ /dev/null @@ -1,35 +0,0 @@ -@echo off -pushd ..\test -goto Cleanandbuild - -:Cleanandbuild -cls -@echo on -devenv ..\Source\Boogie.sln /Clean -@echo off -if errorlevel 1 goto fail -@echo on -devenv ..\source\Boogie.sln /Build -@echo off -if errorlevel 1 goto fail -@echo on -devenv ..\Source\Dafny.sln /Clean -@echo off -if errorlevel 1 goto fail -@echo on -devenv ..\Source\Dafny.sln /Build -@echo off -if errorlevel 1 goto fail -goto reg - -:Reg -cls -call runtestall -goto end - -:fail -echo Some part of the rebuild failed. -goto end - -:end -popd \ No newline at end of file diff --git a/Util/Emacs/chalice-mode.el b/Util/Emacs/chalice-mode.el deleted file mode 100644 index c8cef685..00000000 --- a/Util/Emacs/chalice-mode.el +++ /dev/null @@ -1,118 +0,0 @@ -;; chalice-mode.el - GNU Emacs mode for Chalice -;; Adapted by Rustan Leino from Jean-Christophe FILLIATRE's GNU Emancs mode for Why - -(defvar chalice-mode-hook nil) - -(defvar chalice-mode-map nil - "Keymap for Chalice major mode") - -(if chalice-mode-map nil - (setq chalice-mode-map (make-keymap)) - (define-key chalice-mode-map "\C-c\C-c" 'chalice-run-boogie) - (define-key chalice-mode-map [(control return)] 'font-lock-fontify-buffer)) - -(setq auto-mode-alist - (append - '(("\\.chalice" . chalice-mode)) - auto-mode-alist)) - -;; font-lock - -(defun chalice-regexp-opt (l) - (concat "\\<" (concat (regexp-opt l t) "\\>"))) - -(defconst chalice-font-lock-keywords-1 - (list - ; comments have the form /* ... */ - '("/\\*\\([^*]\\|\\*[^/]\\)*\\*/" . font-lock-comment-face) - ; or // ... - '("//\\([^ -]\\)*" . font-lock-comment-face) - - `(,(chalice-regexp-opt '( - "class" "ghost" "var" "const" "external" "function" "method" - "predicate" "returns" "requires" "ensures" "lockchange" - "invariant" "channel" "condition" "where" - "refines" "transforms" - )) . font-lock-builtin-face) - `(,(chalice-regexp-opt '( - "above" "acc" "acquire" "and" "assert" "assigned" "assume" - "below" "between" "call" "credit" - "downgrade" "else" "eval" "exists" "fold" "forall" "fork" "free" "havoc" "holds" - "spec" "replaces" "by" - "if" "in" "ite" "join" "lock" "lockbottom" "waitlevel" "module" "new" "nil" - "old" "rd" "receive" "release" "reorder" "result" "send" "share" - "this" "unfold" "unfolding" "unshare" "while" - "false" "true" "null")) . font-lock-keyword-face) - `(,(chalice-regexp-opt '("bool" "int" "string" "seq" "token")) . font-lock-type-face) - ) - "Minimal highlighting for Chalice mode") - -(defvar chalice-font-lock-keywords chalice-font-lock-keywords-1 - "Default highlighting for Chalice mode") - -;; syntax - -(defvar chalice-mode-syntax-table nil - "Syntax table for chalice-mode") - -(defun chalice-create-syntax-table () - (if chalice-mode-syntax-table - () - (setq chalice-mode-syntax-table (make-syntax-table)) - (set-syntax-table chalice-mode-syntax-table) - (modify-syntax-entry ?' "w" chalice-mode-syntax-table) - (modify-syntax-entry ?_ "w" chalice-mode-syntax-table))) - -;; menu - -(require 'easymenu) - -(defun chalice-menu () - (easy-menu-define - chalice-mode-menu (list chalice-mode-map) - "Chalice Mode Menu." - '("Chalice" - ["Run Boogie" chalice-run-boogie t] - "---" - ["Recolor buffer" font-lock-fontify-buffer t] - "---" - )) - (easy-menu-add chalice-mode-menu)) - -;; commands - -(defun chalice-command-line (file) - (concat "boogie " file)) - -(defun chalice-run-boogie () - "run Boogie to check the Chalice program" - (interactive) - (let ((f (buffer-name))) - (compile (chalice-command-line f)))) - -;; setting the mode - -(defun chalice-mode () - "Major mode for editing Chalice programs. - -\\{chalice-mode-map}" - (interactive) - (kill-all-local-variables) - (chalice-create-syntax-table) - ; hilight - (make-local-variable 'font-lock-defaults) - (setq font-lock-defaults '(chalice-font-lock-keywords)) - ; indentation - ; (make-local-variable 'indent-line-function) - ; (setq indent-line-function 'chalice-indent-line) - ; menu - ; providing the mode - (setq major-mode 'chalice-mode) - (setq mode-name "Chalice") - (use-local-map chalice-mode-map) - (font-lock-mode 1) - (chalice-menu) - (run-hooks 'chalice-mode-hook)) - -(provide 'chalice-mode) diff --git a/Util/Emacs/dafny-mode.el b/Util/Emacs/dafny-mode.el deleted file mode 100644 index 1ba6186b..00000000 --- a/Util/Emacs/dafny-mode.el +++ /dev/null @@ -1,116 +0,0 @@ -;; dafny-mode.el - GNU Emacs mode for Dafny -;; Adapted by Rustan Leino from Jean-Christophe FILLIATRE's GNU Emancs mode for Why - -(defvar dafny-mode-hook nil) - -(defvar dafny-mode-map nil - "Keymap for Dafny major mode") - -(if dafny-mode-map nil - (setq dafny-mode-map (make-keymap)) - (define-key dafny-mode-map "\C-c\C-c" 'dafny-run-verifier) - (define-key dafny-mode-map [(control return)] 'font-lock-fontify-buffer)) - -(setq auto-mode-alist - (append - '(("\\.dfy" . dafny-mode)) - auto-mode-alist)) - -;; font-lock - -(defun dafny-regexp-opt (l) - (concat "\\<" (concat (regexp-opt l t) "\\>"))) - -(defconst dafny-font-lock-keywords-1 - (list - ; comments have the form /* ... */ - '("/\\*\\([^*]\\|\\*[^/]\\)*\\*/" . font-lock-comment-face) - ; or // ... - '("//\\([^ -]\\)*" . font-lock-comment-face) - - `(,(dafny-regexp-opt '( - "class" "datatype" "codatatype" "type" "function" "predicate" "copredicate" - "iterator" - "ghost" "var" "method" "constructor" - "module" "import" "default" "as" "opened" "static" "refines" - "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" "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) - ) - "Minimal highlighting for Dafny mode") - -(defvar dafny-font-lock-keywords dafny-font-lock-keywords-1 - "Default highlighting for Dafny mode") - -;; syntax - -(defvar dafny-mode-syntax-table nil - "Syntax table for dafny-mode") - -(defun dafny-create-syntax-table () - (if dafny-mode-syntax-table - () - (setq dafny-mode-syntax-table (make-syntax-table)) - (set-syntax-table dafny-mode-syntax-table) - (modify-syntax-entry ?' "w" dafny-mode-syntax-table) - (modify-syntax-entry ?_ "w" dafny-mode-syntax-table))) - -;; menu - -(require 'easymenu) - -(defun dafny-menu () - (easy-menu-define - dafny-mode-menu (list dafny-mode-map) - "Dafny Mode Menu." - '("Dafny" - ["Run Dafny" dafny-run-verifier t] - "---" - ["Recolor buffer" font-lock-fontify-buffer t] - "---" - )) - (easy-menu-add dafny-mode-menu)) - -;; commands - -(defun dafny-command-line (file) - (concat "boogie " file)) - -(defun dafny-run-verifier () - "run Dafny verifier" - (interactive) - (let ((f (buffer-name))) - (compile (dafny-command-line f)))) - -;; setting the mode - -(defun dafny-mode () - "Major mode for editing Dafny programs. - -\\{dafny-mode-map}" - (interactive) - (kill-all-local-variables) - (dafny-create-syntax-table) - ; hilight - (make-local-variable 'font-lock-defaults) - (setq font-lock-defaults '(dafny-font-lock-keywords)) - ; indentation - ; (make-local-variable 'indent-line-function) - ; (setq indent-line-function 'dafny-indent-line) - ; menu - ; providing the mode - (setq major-mode 'dafny-mode) - (setq mode-name "Dafny") - (use-local-map dafny-mode-map) - (font-lock-mode 1) - (dafny-menu) - (run-hooks 'dafny-mode-hook)) - -(provide 'dafny-mode) diff --git a/Util/Emacs/jennisys-mode.el b/Util/Emacs/jennisys-mode.el deleted file mode 100644 index d8f20a31..00000000 --- a/Util/Emacs/jennisys-mode.el +++ /dev/null @@ -1,113 +0,0 @@ -;; jennisys-mode.el - GNU Emacs mode for Jennisys -;; Adapted by Rustan Leino from Jean-Christophe FILLIATRE's GNU Emancs mode for Why - -(defvar jennisys-mode-hook nil) - -(defvar jennisys-mode-map nil - "Keymap for Jennisys major mode") - -(if jennisys-mode-map nil - (setq jennisys-mode-map (make-keymap)) - (define-key jennisys-mode-map "\C-c\C-c" 'jennisys-run-boogie) - (define-key jennisys-mode-map [(control return)] 'font-lock-fontify-buffer)) - -(setq auto-mode-alist - (append - '(("\\.jen" . jennisys-mode)) - auto-mode-alist)) - -;; font-lock - -(defun jennisys-regexp-opt (l) - (concat "\\<" (concat (regexp-opt l t) "\\>"))) - -(defconst jennisys-font-lock-keywords-1 - (list - ; comments have the form /* ... */ - '("/\\*\\([^*]\\|\\*[^/]\\)*\\*/" . font-lock-comment-face) - ; or // ... - '("//\\([^ -]\\)*" . font-lock-comment-face) - - `(,(jennisys-regexp-opt '( - "interface" "datamodel" "code" - "var" "constructor" "method" - "frame" "invariant" "returns" "requires" "ensures" - )) . font-lock-builtin-face) - `(,(jennisys-regexp-opt '( - "if" "then" "else" - "forall" "exists" - "this" "in" - "false" "true" "null")) . font-lock-keyword-face) - `(,(jennisys-regexp-opt '("array" "bool" "int" "set" "seq")) . font-lock-type-face) - ) - "Minimal highlighting for Jennisys mode") - -(defvar jennisys-font-lock-keywords jennisys-font-lock-keywords-1 - "Default highlighting for Jennisys mode") - -;; syntax - -(defvar jennisys-mode-syntax-table nil - "Syntax table for jennisys-mode") - -(defun jennisys-create-syntax-table () - (if jennisys-mode-syntax-table - () - (setq jennisys-mode-syntax-table (make-syntax-table)) - (set-syntax-table jennisys-mode-syntax-table) - (modify-syntax-entry ?' "w" jennisys-mode-syntax-table) - (modify-syntax-entry ?_ "w" jennisys-mode-syntax-table))) - -;; menu - -(require 'easymenu) - -(defun jennisys-menu () - (easy-menu-define - jennisys-mode-menu (list jennisys-mode-map) - "Jennisys Mode Menu." - '("Jennisys" - ["Run Boogie" jennisys-run-boogie t] - "---" - ["Recolor buffer" font-lock-fontify-buffer t] - "---" - )) - (easy-menu-add jennisys-mode-menu)) - -;; commands - -(defun jennisys-command-line (file) - (concat "boogie " file)) - -(defun jennisys-run-boogie () - "run Boogie to check the Jennisys program" - (interactive) - (let ((f (buffer-name))) - (compile (jennisys-command-line f)))) - -;; setting the mode - -(defun jennisys-mode () - "Major mode for editing Jennisys programs. - -\\{jennisys-mode-map}" - (interactive) - (kill-all-local-variables) - (jennisys-create-syntax-table) - ; hilight - (make-local-variable 'font-lock-defaults) - (setq font-lock-defaults '(jennisys-font-lock-keywords)) - ; indentation - ; (make-local-variable 'indent-line-function) - ; (setq indent-line-function 'jennisys-indent-line) - ; menu - ; providing the mode - (setq major-mode 'jennisys-mode) - (setq mode-name "Jennisys") - (use-local-map jennisys-mode-map) - (font-lock-mode 1) - (jennisys-menu) - (run-hooks 'jennisys-mode-hook)) - -(provide 'jennisys-mode) diff --git a/Util/VS2010/Chalice/ChaliceLanguageService.sln b/Util/VS2010/Chalice/ChaliceLanguageService.sln deleted file mode 100644 index dfda1244..00000000 --- a/Util/VS2010/Chalice/ChaliceLanguageService.sln +++ /dev/null @@ -1,20 +0,0 @@ - -Microsoft Visual Studio Solution File, Format Version 11.00 -# Visual Studio 2010 -Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "ChaliceLanguageService", "ChaliceLanguageService\ChaliceLanguageService.csproj", "{66E611EE-84D8-4EB9-9A33-164A53E00553}" -EndProject -Global - GlobalSection(SolutionConfigurationPlatforms) = preSolution - Debug|Any CPU = Debug|Any CPU - Release|Any CPU = Release|Any CPU - EndGlobalSection - GlobalSection(ProjectConfigurationPlatforms) = postSolution - {66E611EE-84D8-4EB9-9A33-164A53E00553}.Debug|Any CPU.ActiveCfg = Debug|Any CPU - {66E611EE-84D8-4EB9-9A33-164A53E00553}.Debug|Any CPU.Build.0 = Debug|Any CPU - {66E611EE-84D8-4EB9-9A33-164A53E00553}.Release|Any CPU.ActiveCfg = Release|Any CPU - {66E611EE-84D8-4EB9-9A33-164A53E00553}.Release|Any CPU.Build.0 = Release|Any CPU - EndGlobalSection - GlobalSection(SolutionProperties) = preSolution - HideSolutionNode = FALSE - EndGlobalSection -EndGlobal diff --git a/Util/VS2010/Chalice/ChaliceLanguageService/ChaliceLanguageService.csproj b/Util/VS2010/Chalice/ChaliceLanguageService/ChaliceLanguageService.csproj deleted file mode 100644 index 44a36137..00000000 --- a/Util/VS2010/Chalice/ChaliceLanguageService/ChaliceLanguageService.csproj +++ /dev/null @@ -1,179 +0,0 @@ - - - - Debug - AnyCPU - 9.0.30729 - 2.0 - Library - Properties - Demo.ChaliceLanguageService - ChaliceLanguageService - True - Key.snk - v4.0 - {66E611EE-84D8-4EB9-9A33-164A53E00553} - - - 4.0 - - - publish\ - true - Disk - false - Foreground - 7 - Days - false - false - true - 0 - 1.0.0.%2a - false - false - true - - - - true - full - false - bin\Debug\ - DEBUG;TRACE - prompt - 4 - AllRules.ruleset - - - pdbonly - true - bin\Release\ - TRACE - prompt - 4 - true - AllRules.ruleset - - - - False - Resources\Irony.dll - - - - False - C:\Program Files\Microsoft Visual Studio 2010 Beta2 SDK\VisualStudioIntegration\Common\Assemblies\Microsoft.VisualStudio.Package.LanguageService.10.0.dll - - - C:\Program Files\Microsoft Visual Studio 2010 Beta2 SDK\VisualStudioIntegration\Common\Assemblies\Microsoft.VisualStudio.Shell.10.0.dll - - - False - C:\Program Files\Microsoft Visual Studio 2010 Beta2 SDK\VisualStudioIntegration\Common\Assemblies\Microsoft.VisualStudio.Shell.Immutable.10.0.dll - - - - False - True - C:\Program Files\Microsoft Visual Studio 2010 Beta2 SDK\VisualStudioIntegration\Common\Assemblies\Microsoft.VisualStudio.Shell.Interop.10.0.dll - - - - - - False - ..\..\..\..\..\Program Files\Microsoft Visual Studio 2008 SDK\VisualStudioIntegration\Common\Assemblies\Microsoft.VisualStudio.TextManager.Interop.8.0.dll - - - - - - - - - - - - - - - - - - - - - - - - - - - True - True - Resources.resx - - - - - - - - ResXFileCodeGenerator - Resources.Designer.cs - Designer - - - true - Designer - - - - - - - - - - - - False - .NET Framework 3.5 SP1 Client Profile - false - - - False - .NET Framework 3.5 SP1 - true - - - False - Microsoft Visual Basic PowerPacks 10.0 - true - - - False - Windows Installer 3.1 - true - - - - - true - true - - - - - \ No newline at end of file diff --git a/Util/VS2010/Chalice/ChaliceLanguageService/Configuration.cs b/Util/VS2010/Chalice/ChaliceLanguageService/Configuration.cs deleted file mode 100644 index e5b10f00..00000000 --- a/Util/VS2010/Chalice/ChaliceLanguageService/Configuration.cs +++ /dev/null @@ -1,24 +0,0 @@ -using System; -using System.Collections.Generic; -using Microsoft.VisualStudio.Package; -using Microsoft.VisualStudio.TextManager.Interop; - -namespace Demo -{ - public static partial class Configuration - { - public const string Name = "Chalice"; - public const string FormatList = "Chalice File (*.chalice)\n*.chalice"; - - static Configuration() - { - // default colors - currently, these need to be declared - CreateColor("Keyword", COLORINDEX.CI_BLUE, COLORINDEX.CI_USERTEXT_BK); - CreateColor("Comment", COLORINDEX.CI_DARKGREEN, COLORINDEX.CI_USERTEXT_BK); - CreateColor("Identifier", COLORINDEX.CI_SYSPLAINTEXT_FG, COLORINDEX.CI_USERTEXT_BK); - CreateColor("String", COLORINDEX.CI_MAROON, COLORINDEX.CI_USERTEXT_BK); - CreateColor("Number", COLORINDEX.CI_MAROON, COLORINDEX.CI_USERTEXT_BK); - CreateColor("Text", COLORINDEX.CI_SYSPLAINTEXT_FG, COLORINDEX.CI_USERTEXT_BK); - } - } -} \ No newline at end of file diff --git a/Util/VS2010/Chalice/ChaliceLanguageService/GlobalSuppressions.cs b/Util/VS2010/Chalice/ChaliceLanguageService/GlobalSuppressions.cs deleted file mode 100644 index f0857cbb..00000000 --- a/Util/VS2010/Chalice/ChaliceLanguageService/GlobalSuppressions.cs +++ /dev/null @@ -1,11 +0,0 @@ -// This file is used by Code Analysis to maintain SuppressMessage -// attributes that are applied to this project. Project-level -// suppressions either have no target or are given a specific target -// and scoped to a namespace, type, member, etc. -// -// To add a suppression to this file, right-click the message in the -// Error List, point to "Suppress Message(s)", and click "In Project -// Suppression File". You do not need to add suppressions to this -// file manually. - -[assembly: System.Diagnostics.CodeAnalysis.SuppressMessage("Microsoft.Design", "CA1017:MarkAssembliesWithComVisible")] diff --git a/Util/VS2010/Chalice/ChaliceLanguageService/Grammar.cs b/Util/VS2010/Chalice/ChaliceLanguageService/Grammar.cs deleted file mode 100644 index 8a05d7b2..00000000 --- a/Util/VS2010/Chalice/ChaliceLanguageService/Grammar.cs +++ /dev/null @@ -1,399 +0,0 @@ -using System; -using System.Collections.Generic; -using System.Linq; -using Irony.Parsing; - -namespace Demo -{ - [Language("Chalice", "1.0", "Chalice Programming Language")] - public class Grammar : Irony.Parsing.Grammar - { - public Grammar() { - #region 1. Terminals - NumberLiteral n = TerminalFactory.CreateCSharpNumber("number"); - StringLiteral s = new StringLiteral("String", "\"", StringFlags.AllowsAllEscapes); - IdentifierTerminal ident = new IdentifierTerminal("Identifier"); - - // Copy pasted directly from Parser.scala - string[] reserved = new string[] { - "class", "ghost", "var", "const", "method", "channel", "condition", - "assert", "assume", "new", "this", "reorder", - "between", "and", "above", "below", "share", "unshare", "acquire", "release", "downgrade", - "lock", "fork", "join", "rd", "acc", "credit", "holds", "old", "assigned", - "call", "if", "else", "while", - "invariant", "lockchange", - "returns", "requires", "ensures", "where", - "int", "bool", "false", "true", "null", "string", "waitlevel", "lockbottom", - "module", "external", - "predicate", "function", "free", "send", "receive", - "ite", "fold", "unfold", "unfolding", "in", "forall", "exists", - "seq", "nil", "result", "eval", "token", - "wait", "signal", - "refines", "transforms", "replaces", "by", "spec" - }; - - string[] delimiters = new string[] { - "(", ")", "{", "}", "[[", "]]", - "<==>", "==>", "&&", "||", - "==", "!=", "<", "<=", ">=", ">", "<<", "in", "!in", - "+", "-", "*", "/", "%", "!", ".", "..", - ";", ":", ":=", ",", "?", "|", "[", "]", "++", "::", - "_" - }; - - this.MarkReservedWords(reserved); - - Terminal Comment = new CommentTerminal("Comment", "/*", "*/"); - NonGrammarTerminals.Add(Comment); - Terminal LineComment = new CommentTerminal("LineComment", "//", "\n"); - NonGrammarTerminals.Add(LineComment); - - #endregion - - #region Disabled for a simpler grammar - /* - Terminal dot = ToTerm(".", "dot"); - Terminal less = ToTerm("<"); - Terminal greater = ToTerm(">"); - Terminal arrow = ToTerm("->"); - Terminal LBracket = ToTerm("["); - Terminal RBracket = ToTerm("]"); - Terminal LParen = ToTerm("("); - Terminal RParen = ToTerm(")"); - Terminal RCurly = ToTerm("}"); - Terminal LCurly = ToTerm("{"); - Terminal LMb = ToTerm("<["); - Terminal RMb = ToTerm("]>"); - Terminal comma = ToTerm(","); - Terminal semicolon = ToTerm(";"); - Terminal colon = ToTerm(":"); - - #region 2. Non-terminals - #region 2.1 Expressions - NonTerminal expression = new NonTerminal("Expr"); - NonTerminal BinOp = new NonTerminal("BinOp"); - NonTerminal LUnOp = new NonTerminal("LUnOp"); - NonTerminal RUnOp = new NonTerminal("RUnOp"); - - NonTerminal ArrayConstructor = new NonTerminal("ArrayConstructor"); - NonTerminal MObjectConstructor = new NonTerminal("MObjectConstructor"); - NonTerminal MObjectList = new NonTerminal("MObjectList"); - #endregion - - #region 2.2 QualifiedName - //Expression List: expr1, expr2, expr3, .. - NonTerminal expressionList = new NonTerminal("ExprList"); - NonTerminal identList = new NonTerminal("identList"); - //A name in form: a.b.c().d[1,2].e .... - NonTerminal NewStmt = new NonTerminal("NewStmt"); - NonTerminal NewArrStmt = new NonTerminal("NewArrStmt"); - NonTerminal QualifiedName = new NonTerminal("QualifiedName"); - NonTerminal AccessQualName = new NonTerminal("AccessQualName"); - NonTerminal GenericsPostfix = new NonTerminal("GenericsPostfix"); - NonTerminal ArrayExpression = new NonTerminal("ArrayExpression"); - NonTerminal FunctionExpression = new NonTerminal("FunctionExpression"); - NonTerminal selectExpr = new NonTerminal("selectExpr"); - NonTerminal accessExpr = new NonTerminal("accessExpr"); - #endregion - - #region 2.3 Statement - NonTerminal Condition = new NonTerminal("Condition"); - - NonTerminal Statement = new NonTerminal("Statement"); - NonTerminal Statements = new NonTerminal("Statements"); - - //Block - NonTerminal blockStatement = new NonTerminal("CompoundStatement"); - #endregion - - #region 2.4 Program and Functions - NonTerminal Prog = new NonTerminal("Prog"); - NonTerminal declaration = new NonTerminal("declaration"); - NonTerminal classDecl = new NonTerminal("class decl"); - NonTerminal memberDecl = new NonTerminal("member decl"); - NonTerminal fieldDecl = new NonTerminal("field declaration"); - NonTerminal idType = new NonTerminal("identifier type"); - NonTerminal typeDecl = new NonTerminal("type reference"); - NonTerminal methodDecl = new NonTerminal("method declaration"); - NonTerminal formalParameters = new NonTerminal("formals"); - NonTerminal methodSpec = new NonTerminal("method spec"); - NonTerminal formalsList = new NonTerminal("ParamaterListOpt"); - NonTerminal functionDecl = new NonTerminal("function declaration"); - NonTerminal predicateDecl = new NonTerminal("predicate declaration"); - NonTerminal invariantDecl = new NonTerminal("invariant declaration"); - NonTerminal Semi = new NonTerminal("semi"); - NonTerminal Rhs = new NonTerminal("right-hand side"); - NonTerminal FieldInit = new NonTerminal("field init"); - NonTerminal FieldInits = new NonTerminal("field inits"); - NonTerminal installBounds = new NonTerminal("installBounds"); - NonTerminal localVarStmt = new NonTerminal("localVarStmt"); - NonTerminal evalstate = new NonTerminal("evalstate"); - NonTerminal channelDecl = new NonTerminal("channel declaration"); - NonTerminal loopSpec = new NonTerminal("loop specification"); - NonTerminal rdPermArg = new NonTerminal("rdPermArg"); - #endregion - - #endregion - - #region 3. BNF rules - - Semi.Rule = semicolon; - - #region 3.1 Expressions - selectExpr.Rule = (ToTerm("this") + ".").Q() + QualifiedName; - accessExpr.Rule = (ToTerm("this") + ".").Q() + AccessQualName; - evalstate.Rule = - ident + ToTerm(".") + - (ToTerm("acquire") - | "release" - | "fork" + FunctionExpression - ) - ; - rdPermArg.Rule = ToTerm("*") | expression; - - expression.Rule = ToTerm("true") - | "false" - | "null" - | "waitlevel" - | "lockbottom" - | "this" - | "result" - | s - | n - | QualifiedName - // The following is needed: to parse "A=" | "<=" | "is" - | "=" | "+=" | "-=" - | "." - | "==>" | "<==>" | "<<" - ; - - LUnOp.Rule = ToTerm("-") | "~" | "!"; - RUnOp.Rule = ToTerm("++") | "--"; - - ArrayConstructor.Rule = LBracket + expressionList + RBracket; - MObjectConstructor.Rule = LBracket + ident + arrow + expression + MObjectList.Star() + RBracket; - MObjectList.Rule = comma + ident + arrow + expression; - #endregion - - #region 3.2 QualifiedName - ArrayExpression.Rule = QualifiedName + LBracket + expressionList + RBracket; - FunctionExpression.Rule = QualifiedName + LParen + expressionList.Q() + RParen; - - QualifiedName.Rule = ident | QualifiedName + dot + ident; - AccessQualName.Rule = ident | "*" | QualifiedName + dot + (ident | "*" | "[*]" + dot + "*" | "[*]" + dot + ident); - - - GenericsPostfix.Rule = less + QualifiedName + greater; - - //ExprList.Rule = Expr.Plus(comma); - #endregion - - #region 3.3 Statement - Condition.Rule = LParen + expression + RParen; - installBounds.Rule - = "installBounds" - //= ToTerm("between") + expressionList + "and" + expressionList - //| "below" + expressionList - //| "below" + expressionList + "above" + expressionList - //| "above" + expressionList - //| "above" + expressionList + "below" + expressionList - ; - FieldInit.Rule - = ident + ":=" + expression - ; - FieldInits.Rule = MakeStarRule(FieldInits, ToTerm(","), FieldInit); - Rhs.Rule - = ToTerm("new") + ident - | ToTerm("new") + ident + "{" + FieldInits + "}" - | ToTerm("new") + ident + installBounds - | ToTerm("new") + ident + "{" + FieldInits + "}" + installBounds - | expression - ; - localVarStmt.Rule - = idType + ":=" + Rhs + Semi - | idType + Semi - ; - loopSpec.Rule - = ToTerm("invariant") + expression + Semi - | "lockchange" + expressionList + Semi - ; - - - - Statement.Rule = Semi - | "if" + Condition + Statement - | "if" + Condition + Statement + PreferShiftHere() + "else" + Statement - | "while" + Condition + loopSpec.Star() + Statement - | "for" + LParen + expression.Q() + Semi + expression.Q() + Semi + expression.Q() + RParen + Statement - | "foreach" + LParen + ident + "in" + expression + RParen + Statement - | blockStatement - | expression + Semi - | "break" + Semi - | "continue" + Semi - | "return" + expression + Semi - | QualifiedName + ":=" + Rhs - - | "var" + localVarStmt - | "const" + localVarStmt - - | "call" + identList + ":=" + FunctionExpression + Semi - | "call" + FunctionExpression + Semi - | "assert" + expression + Semi - | "assume" + expression + Semi - | "unshare" + expression + Semi - | "lock" + Condition + Statement - | "[[" + Statements + "]]" - | "acquire" + expression + Semi - | "release" + expression + Semi - | "downgrade" + expression + Semi - | "free" + expression + Semi - | "fold" + expression + Semi - | "unfold" + expression + Semi - | "reorder" + expression + installBounds + Semi - | "reorder" + expression + Semi - | "share" + expression + installBounds + Semi - | "share" + expression + Semi - | "fork" + identList + ":=" + FunctionExpression + Semi - | "fork" + FunctionExpression + Semi - | "join" + identList + ":=" + expression + Semi - | "join" + expression + Semi - | "send" + expression + Semi - | "receive" + identList + ":=" + expression + Semi - | "receive" + expression + Semi - - ; - Statements.Rule = MakeStarRule(Statements, null, Statement); - blockStatement.Rule = LCurly + Statements + RCurly; - - - #endregion - - #region 3.4 Prog - Prog.Rule = declaration.Star() + Eof; - idType.Rule - = ident + ":" + typeDecl - | ident - ; - - typeDecl.Rule - = (ToTerm("int") | "bool" | ident | "seq") + (("<" + MakePlusRule(typeDecl, ToTerm(","), typeDecl) + ">") | Empty) - | ToTerm("token") + "<" + (typeDecl + ".") + ident + ">" - ; - - fieldDecl.Rule - = ToTerm("var") + idType + Semi - | ToTerm("ghost") + "var" + idType + Semi - ; - - methodSpec.Rule = (ToTerm("requires") | "ensures" | "lockchange") + expression + Semi; - - formalsList.Rule = MakeStarRule(formalsList, comma, idType); - formalParameters.Rule = LParen + formalsList + RParen; - methodDecl.Rule = "method" + ident + formalParameters - + (("returns" + formalParameters) | Empty) - + methodSpec.Star() - + blockStatement; - functionDecl.Rule - = ToTerm("function") + ident + formalParameters + ":" + typeDecl + methodSpec.Star() + "{" + expression + "}"; - predicateDecl.Rule - = ToTerm("predicate") + ident + "{" + expression + "}"; - invariantDecl.Rule - = ToTerm("invariant") + expression + Semi; - - memberDecl.Rule - = fieldDecl - | invariantDecl - | methodDecl - //| conditionDecl - | predicateDecl - | functionDecl - ; - classDecl.Rule - = (ToTerm("external") | Empty) + "class" + ident + ("module" + ident | Empty) + "{" + memberDecl.Star() + "}"; - channelDecl.Rule - = ToTerm("channel") + ident + formalParameters + "where" + expression + Semi - | ToTerm("channel") + ident + formalParameters + Semi; - declaration.Rule = classDecl | channelDecl - ; - - #endregion - #endregion - - #region 4. Set starting symbol - this.Root = Prog; // Set grammar root - #endregion - - - #region 5. Operators precedence - RegisterOperators(1, "=", "+=", "-="); - RegisterOperators(2, "+", "-"); - RegisterOperators(3, "*", "/", "%"); - RegisterOperators(4, Associativity.Right, "^"); - RegisterOperators(5, "|", "||"); - RegisterOperators(6, "&", "&&"); - RegisterOperators(7, "==", "!=", ">", "<", ">=", "<=", "<<"); - RegisterOperators(8, "is"); - RegisterOperators(9, "~", "!", "++", "--"); - RegisterOperators(10, "==>", "<==>"); - RegisterOperators(11, "."); - - //RegisterOperators(10, Associativity.Right, ".",",", ")", "(", "]", "[", "{", "}"); - //RegisterOperators(11, Associativity.Right, "else"); - #endregion - - #region 6. Punctuation symbols - RegisterPunctuation("(", ")", "[", "]", "{", "}", ",", ";"); - #endregion - */ - #endregion - - #region Simple grammar - NonTerminal Simple = new NonTerminal("SimpleProg"); - NonTerminal Anything = new NonTerminal("Token"); - Simple.Rule = Anything.Star() + Eof; - Anything.Rule = n | s; - foreach (string keyword in reserved) Anything.Rule = Anything.Rule | ToTerm(keyword); - Anything.Rule = Anything.Rule | ident; - foreach (string delimiter in delimiters) Anything.Rule = Anything.Rule | ToTerm(delimiter); - - RegisterBracePair("{", "}"); - RegisterBracePair("(", ")"); - - this.Root = Simple; - #endregion - } - } -} diff --git a/Util/VS2010/Chalice/ChaliceLanguageService/Guids.cs b/Util/VS2010/Chalice/ChaliceLanguageService/Guids.cs deleted file mode 100644 index ba02ca8c..00000000 --- a/Util/VS2010/Chalice/ChaliceLanguageService/Guids.cs +++ /dev/null @@ -1,13 +0,0 @@ -using System; - -namespace Demo -{ - static class GuidList - { - public const string guidIronyLanguageServiceString = "7bcbed0f-df47-4729-b796-b54f14853e2e"; - public const string guidIronyLanguageServicePkgString = "a681f79a-0ed1-4ae0-b79f-4ae69e178800"; - public const string guidIronyLanguageServiceCmdSetString = "be21e7e3-e9c5-4287-95ab-e5125c5063f7"; - - public static readonly Guid guidIronyLanguageServiceCmdSet = new Guid(guidIronyLanguageServiceCmdSetString); - }; -} \ No newline at end of file diff --git a/Util/VS2010/Chalice/ChaliceLanguageService/Integration/AuthoringScope.cs b/Util/VS2010/Chalice/ChaliceLanguageService/Integration/AuthoringScope.cs deleted file mode 100644 index 9a49dbe4..00000000 --- a/Util/VS2010/Chalice/ChaliceLanguageService/Integration/AuthoringScope.cs +++ /dev/null @@ -1,66 +0,0 @@ -using System; -using System.Collections.Generic; -using Microsoft.VisualStudio; -using Microsoft.VisualStudio.TextManager.Interop; -using Microsoft.VisualStudio.Package; - -namespace Demo -{ - public class AuthoringScope : Microsoft.VisualStudio.Package.AuthoringScope - { - public AuthoringScope(object parseResult) - { - this.parseResult = parseResult; - - // how should this be set? - this.resolver = new Resolver(); - } - - object parseResult; - IASTResolver resolver; - - // ParseReason.QuickInfo - public override string GetDataTipText(int line, int col, out TextSpan span) - { - span = new TextSpan(); - return null; - } - - // ParseReason.CompleteWord - // ParseReason.DisplayMemberList - // ParseReason.MemberSelect - // ParseReason.MemberSelectAndHilightBraces - public override Microsoft.VisualStudio.Package.Declarations GetDeclarations(IVsTextView view, int line, int col, TokenInfo info, ParseReason reason) - { - IList declarations; - switch (reason) - { - case ParseReason.CompleteWord: - declarations = resolver.FindCompletions(parseResult, line, col); - break; - case ParseReason.DisplayMemberList: - case ParseReason.MemberSelect: - case ParseReason.MemberSelectAndHighlightBraces: - declarations = resolver.FindMembers(parseResult, line, col); - break; - default: - throw new ArgumentException("reason"); - } - - return new Declarations(declarations); - } - - // ParseReason.GetMethods - public override Microsoft.VisualStudio.Package.Methods GetMethods(int line, int col, string name) - { - return new Methods(resolver.FindMethods(parseResult, line, col, name)); - } - - // ParseReason.Goto - public override string Goto(VSConstants.VSStd97CmdID cmd, IVsTextView textView, int line, int col, out TextSpan span) - { - span = new TextSpan(); - return null; - } - } -} \ No newline at end of file diff --git a/Util/VS2010/Chalice/ChaliceLanguageService/Integration/Configuration.cs b/Util/VS2010/Chalice/ChaliceLanguageService/Integration/Configuration.cs deleted file mode 100644 index f7412393..00000000 --- a/Util/VS2010/Chalice/ChaliceLanguageService/Integration/Configuration.cs +++ /dev/null @@ -1,116 +0,0 @@ -using System; -using System.Collections.Generic; -using Microsoft.VisualStudio.Package; -using Microsoft.VisualStudio.TextManager.Interop; - -namespace Demo -{ - public static partial class Configuration - { - public static Grammar Grammar = new Grammar(); - static List colorableItems = new List(); - - public static IList ColorableItems - { - get { return colorableItems; } - } - - public static TokenColor CreateColor(string name, COLORINDEX foreground, COLORINDEX background) - { - return CreateColor(name, foreground, background, false, false); - } - - public static TokenColor CreateColor(string name, COLORINDEX foreground, COLORINDEX background, bool bold, bool strikethrough) - { - colorableItems.Add(new ColorableItem(name, foreground, background, bold, strikethrough)); - return (TokenColor)colorableItems.Count; - } - - public static void ColorToken(string tokenName, TokenType type, TokenColor color, TokenTriggers trigger) - { - definitions[tokenName] = new TokenDefinition(type, color, trigger); - } - - public static TokenDefinition GetDefinition(string tokenName) - { - TokenDefinition result; - return definitions.TryGetValue(tokenName, out result) ? result : defaultDefinition; - } - - private static TokenDefinition defaultDefinition = new TokenDefinition(TokenType.Text, TokenColor.Text, TokenTriggers.None); - private static Dictionary definitions = new Dictionary(); - - public struct TokenDefinition - { - public TokenDefinition(TokenType type, TokenColor color, TokenTriggers triggers) - { - this.TokenType = type; - this.TokenColor = color; - this.TokenTriggers = triggers; - } - - public TokenType TokenType; - public TokenColor TokenColor; - public TokenTriggers TokenTriggers; - } - } - - public class ColorableItem : Microsoft.VisualStudio.TextManager.Interop.IVsColorableItem - { - private string displayName; - private COLORINDEX background; - private COLORINDEX foreground; - private uint fontFlags = (uint)FONTFLAGS.FF_DEFAULT; - - public ColorableItem(string displayName, COLORINDEX foreground, COLORINDEX background, bool bold, bool strikethrough) - { - this.displayName = displayName; - this.background = background; - this.foreground = foreground; - - if (bold) - this.fontFlags = this.fontFlags | (uint)FONTFLAGS.FF_BOLD; - if (strikethrough) - this.fontFlags = this.fontFlags | (uint)FONTFLAGS.FF_STRIKETHROUGH; - } - - #region IVsColorableItem Members - public int GetDefaultColors(COLORINDEX[] piForeground, COLORINDEX[] piBackground) - { - if (null == piForeground) - { - throw new ArgumentNullException("piForeground"); - } - if (0 == piForeground.Length) - { - throw new ArgumentOutOfRangeException("piForeground"); - } - piForeground[0] = foreground; - - if (null == piBackground) - { - throw new ArgumentNullException("piBackground"); - } - if (0 == piBackground.Length) - { - throw new ArgumentOutOfRangeException("piBackground"); - } - piBackground[0] = background; - - return Microsoft.VisualStudio.VSConstants.S_OK; - } - - public int GetDefaultFontFlags(out uint pdwFontFlags) - { - pdwFontFlags = this.fontFlags; - return Microsoft.VisualStudio.VSConstants.S_OK; - } - - public int GetDisplayName(out string pbstrName) - { - pbstrName = displayName; - return Microsoft.VisualStudio.VSConstants.S_OK; - } - #endregion - } -} \ No newline at end of file diff --git a/Util/VS2010/Chalice/ChaliceLanguageService/Integration/Declaration.cs b/Util/VS2010/Chalice/ChaliceLanguageService/Integration/Declaration.cs deleted file mode 100644 index c0fda5ca..00000000 --- a/Util/VS2010/Chalice/ChaliceLanguageService/Integration/Declaration.cs +++ /dev/null @@ -1,30 +0,0 @@ -using System; -using System.Collections.Generic; - -namespace Demo -{ - public struct Declaration : IComparable - { - public Declaration(string description, string displayText, int glyph, string name) - { - this.Description = description; - this.DisplayText = displayText; - this.Glyph = glyph; - this.Name = name; - } - - public string Description; - public string DisplayText; - public int Glyph; - public string Name; - - #region IComparable Members - - public int CompareTo(Declaration other) - { - return DisplayText.CompareTo(other.DisplayText); - } - - #endregion - } -} \ No newline at end of file diff --git a/Util/VS2010/Chalice/ChaliceLanguageService/Integration/Declarations.cs b/Util/VS2010/Chalice/ChaliceLanguageService/Integration/Declarations.cs deleted file mode 100644 index 98a411ce..00000000 --- a/Util/VS2010/Chalice/ChaliceLanguageService/Integration/Declarations.cs +++ /dev/null @@ -1,56 +0,0 @@ -/*************************************************************************** - -Copyright (c) Microsoft Corporation. All rights reserved. -This code is licensed under the Visual Studio SDK license terms. -THIS CODE IS PROVIDED *AS IS* WITHOUT WARRANTY OF -ANY KIND, EITHER EXPRESS OR IMPLIED, INCLUDING ANY -IMPLIED WARRANTIES OF FITNESS FOR A PARTICULAR -PURPOSE, MERCHANTABILITY, OR NON-INFRINGEMENT. - -***************************************************************************/ - -using System; -using System.Collections.Generic; -using System.Text; -using Microsoft.VisualStudio.TextManager.Interop; -using Microsoft.VisualStudio.Package; - -namespace Demo -{ - public class Declarations : Microsoft.VisualStudio.Package.Declarations - { - IList declarations; - public Declarations(IList declarations) - { - this.declarations = declarations; - } - - public override int GetCount() - { - return declarations.Count; - } - - public override string GetDescription(int index) - { - return declarations[index].Description; - } - - public override string GetDisplayText(int index) - { - return declarations[index].DisplayText; - } - - public override int GetGlyph(int index) - { - return declarations[index].Glyph; - } - - public override string GetName(int index) - { - if (index >= 0) - return declarations[index].Name; - - return null; - } - } -} \ No newline at end of file diff --git a/Util/VS2010/Chalice/ChaliceLanguageService/Integration/IASTResolver.cs b/Util/VS2010/Chalice/ChaliceLanguageService/Integration/IASTResolver.cs deleted file mode 100644 index 8de1a454..00000000 --- a/Util/VS2010/Chalice/ChaliceLanguageService/Integration/IASTResolver.cs +++ /dev/null @@ -1,13 +0,0 @@ -using System; -using System.Collections.Generic; - -namespace Demo -{ - interface IASTResolver - { - IList FindCompletions(object result, int line, int col); - IList FindMembers(object result, int line, int col); - string FindQuickInfo(object result, int line, int col); - IList FindMethods(object result, int line, int col, string name); - } -} \ No newline at end of file diff --git a/Util/VS2010/Chalice/ChaliceLanguageService/Integration/IronyLanguageService.cs b/Util/VS2010/Chalice/ChaliceLanguageService/Integration/IronyLanguageService.cs deleted file mode 100644 index bb7cfebb..00000000 --- a/Util/VS2010/Chalice/ChaliceLanguageService/Integration/IronyLanguageService.cs +++ /dev/null @@ -1,347 +0,0 @@ -using System; -using System.Collections.Generic; -using System.Diagnostics; -using Microsoft.VisualStudio; -using Microsoft.VisualStudio.TextManager.Interop; -using Microsoft.VisualStudio.Package; - -using Irony.Parsing; -using Irony.Ast; - -using System.IO; -using System.Text.RegularExpressions; - -namespace Demo -{ - public class IronyLanguageService : Microsoft.VisualStudio.Package.LanguageService - { - private Grammar grammar; - private Parser parser; - private ParsingContext context; - - public IronyLanguageService() - { - grammar = new Grammar(); - parser = new Parser(Configuration.Grammar); - context = new ParsingContext(parser); - } - - - #region Custom Colors - public override int GetColorableItem(int index, out IVsColorableItem item) - { - if (index <= Configuration.ColorableItems.Count) - { - item = Configuration.ColorableItems[index - 1]; - return Microsoft.VisualStudio.VSConstants.S_OK; - } - else - { - throw new ArgumentNullException("index"); - } - } - - public override int GetItemCount(out int count) - { - count = Configuration.ColorableItems.Count; - return Microsoft.VisualStudio.VSConstants.S_OK; - } - #endregion - - #region MPF Accessor and Factory specialisation - private LanguagePreferences preferences; - public override LanguagePreferences GetLanguagePreferences() - { - if (this.preferences == null) - { - this.preferences = new LanguagePreferences(this.Site, - typeof(IronyLanguageService).GUID, - this.Name); - this.preferences.Init(); - } - - return this.preferences; - } - - public override Microsoft.VisualStudio.Package.Source CreateSource(IVsTextLines buffer) - { - return new Source(this, buffer, this.GetColorizer(buffer)); - } - - private IScanner scanner; - public override IScanner GetScanner(IVsTextLines buffer) - { - if (scanner == null) - this.scanner = new LineScanner(grammar); - - return this.scanner; - } - #endregion - - public override void OnIdle(bool periodic) - { - // from IronPythonLanguage sample - // this appears to be necessary to get a parse request with ParseReason = Check? - Source src = (Source)GetSource(this.LastActiveTextView); - if (src != null && src.LastParseTime >= Int32.MaxValue >> 12) - { - src.LastParseTime = 0; - } - base.OnIdle(periodic); - } - - public override Microsoft.VisualStudio.Package.AuthoringScope ParseSource(ParseRequest req) - { - Debug.Print("ParseSource at ({0}:{1}), reason {2}", req.Line, req.Col, req.Reason); - Source source = (Source)this.GetSource(req.FileName); - switch (req.Reason) - { - case ParseReason.Check: - // This is where you perform your syntax highlighting. - // Parse entire source as given in req.Text. - // Store results in the AuthoringScope object. - var parsed = parser.Parse(req.Text, req.FileName); - var root = parsed.Root; - if (root != null) { - - AstNode node = (AstNode)root.AstNode; - source.ParseResult = node; - } - - // Used for brace matching. - //TokenStack braces = parser.Context.OpenBraces; - //foreach (Token brace in braces) { - // if (brace.OtherBrace == null) continue; - // TextSpan openBrace = new TextSpan(); - // openBrace.iStartLine = brace.Location.Line; - // openBrace.iStartIndex = brace.Location.Column; - // openBrace.iEndLine = brace.Location.Line; - // openBrace.iEndIndex = openBrace.iStartIndex + brace.Length; - - // TextSpan closeBrace = new TextSpan(); - // closeBrace.iStartLine = brace.OtherBrace.Location.Line; - // closeBrace.iStartIndex = brace.OtherBrace.Location.Column; - // closeBrace.iEndLine = brace.OtherBrace.Location.Line; - // closeBrace.iEndIndex = closeBrace.iStartIndex + brace.OtherBrace.Length; - - // if (source.Braces == null) { - // source.Braces = new List(); - // } - // source.Braces.Add(new TextSpan[2] { openBrace, closeBrace }); - //} - - if (parser.Context.CurrentParseTree.ParserMessages.Count > 0) { - foreach (ParserMessage error in parser.Context.CurrentParseTree.ParserMessages) { - TextSpan span = new TextSpan(); - span.iStartLine = span.iEndLine = error.Location.Line; - span.iStartIndex = error.Location.Column; - span.iEndIndex = error.Location.Position; - req.Sink.AddError(req.FileName, error.Message, span, Severity.Error); - } - } else { // parse looks okay, send it to Chalice. - if (!File.Exists(@"C:\tmp\StartChalice.bat")) { - AddErrorBecauseOfToolProblems(req, @"Can't find C:\tmp\StartChalice.bat"); - } else { - - // From: http://dotnetperls.com/process-redirect-standard-output - // (Also, see: http://msdn.microsoft.com/en-us/library/system.diagnostics.processstartinfo.redirectstandardoutput.aspx) - // - // Setup the process with the ProcessStartInfo class. - // - ProcessStartInfo start = new ProcessStartInfo(); - start.FileName = @"cmd.exe"; - start.Arguments = @"/c C:\tmp\StartChalice.bat"; // Specify exe name. - start.UseShellExecute = false; - start.RedirectStandardInput = true; - start.RedirectStandardOutput = true; - start.CreateNoWindow = true; - //start.WindowStyle = ProcessWindowStyle.Minimized; // need this or else you see the window pop up - // - // Start the process. - // - using (Process process = Process.Start(start)) { - // - // Push the file contents to the new process - // - StreamWriter myStreamWriter = process.StandardInput; - myStreamWriter.WriteLine(req.Text); - myStreamWriter.Close(); - // - // Read in all the text from the process with the StreamReader. - // - using (StreamReader reader = process.StandardOutput) { - //string result = reader.ReadToEnd(); - //Console.Write(result); - - for (string line = reader.ReadLine(); line != null; line = reader.ReadLine()) { - if (line == "") - continue; - if (line.StartsWith("Boogie program verifier")) { - if (!Regex.IsMatch(line, "Boogie program verifier finished with [0-9]* verified, 0 errors")) - AddErrorBecauseOfToolProblems(req, line, false); - continue; - } - - // each line is of the form: "x,y,w,z:arbitrary text" - int colonIndex = line.IndexOf(':'); - if (colonIndex == -1) { - AddErrorBecauseOfToolProblems(req, "Couldn't find colon in '" + line + "'"); - continue; - } - string numbers = line.Substring(0, colonIndex); - var message = line.Substring(colonIndex + 1); - string[] positions = numbers.Split(','); - if (positions.Length != 4) { - AddErrorBecauseOfToolProblems(req, "Couldn't find four numbers in '" + numbers + "'"); - continue; - } - try { - TextSpan span = new TextSpan(); - span.iStartLine = span.iEndLine = Math.Max(0, Int32.Parse(positions[0]) - 1); - span.iStartIndex = Math.Max(0, Int32.Parse(positions[1]) - 1); - span.iEndLine = Math.Max(0, Int32.Parse(positions[2]) - 1); - span.iEndIndex = Math.Max(0, Int32.Parse(positions[3]) - 1); - req.Sink.AddError(req.FileName, message, span, Severity.Error); - } catch (System.ArgumentNullException) { - AddErrorBecauseOfToolProblems(req, "Couldn't parse numbers: '" + numbers + "'"); - } catch (System.FormatException) { - AddErrorBecauseOfToolProblems(req, "Couldn't parse numbers: '" + numbers + "'"); - } catch (System.OverflowException) { - AddErrorBecauseOfToolProblems(req, "Couldn't parse numbers: '" + numbers + "'"); - } - } - } - } - } - } - - break; - - case ParseReason.DisplayMemberList: - // Parse the line specified in req.Line for the two - // tokens just before req.Col to obtain the identifier - // and the member connector symbol. - // Examine existing parse tree for members of the identifer - // and return a list of members in your version of the - // Declarations class as stored in the AuthoringScope - // object. - break; - - case ParseReason.MethodTip: - // Parse the line specified in req.Line for the token - // just before req.Col to obtain the name of the method - // being entered. - // Examine the existing parse tree for all method signatures - // with the same name and return a list of those signatures - // in your version of the Methods class as stored in the - // AuthoringScope object. - break; - - case ParseReason.HighlightBraces: - case ParseReason.MemberSelectAndHighlightBraces: - //if (source.Braces != null) - //{ - // foreach (TextSpan[] brace in source.Braces) - // { - // if (brace.Length == 2) - // req.Sink.MatchPair(brace[0], brace[1], 1); - // else if (brace.Length >= 3) - // req.Sink.MatchTriple(brace[0], brace[1], brace[2], 1); - // } - //} - break; - } - - return new AuthoringScope(source.ParseResult); - } - - private static void AddErrorBecauseOfToolProblems(ParseRequest req, string msg) { - AddErrorBecauseOfToolProblems(req, msg, true); - } - private static void AddErrorBecauseOfToolProblems(ParseRequest req, string msg, bool error) { - TextSpan span = new TextSpan(); - span.iStartLine = span.iEndLine = 0; - span.iStartIndex = 0; - span.iEndIndex = 5; - req.Sink.AddError(req.FileName, msg, span, error ? Severity.Error : Severity.Hint); - } - - /// - /// Called to determine if the given location can have a breakpoint applied to it. - /// - /// The IVsTextBuffer object containing the source file. - /// The line number where the breakpoint is to be set. - /// The offset into the line where the breakpoint is to be set. - /// - /// Returns the TextSpan giving the extent of the code affected by the breakpoint if the - /// breakpoint can be set. - /// - /// - /// If successful, returns S_OK; otherwise returns S_FALSE if there is no code at the given - /// position or returns an error code (the validation is deferred until the debug engine is loaded). - /// - /// - /// - /// CAUTION: Even if you do not intend to support the ValidateBreakpointLocation but your language - /// does support breakpoints, you must override the ValidateBreakpointLocation method and return a - /// span that contains the specified line and column; otherwise, breakpoints cannot be set anywhere - /// except line 1. You can return E_NOTIMPL to indicate that you do not otherwise support this - /// method but the span must always be set. The example shows how this can be done. - /// - /// - /// Since the language service parses the code, it generally knows what is considered code and what - /// is not. Normally, the debug engine is loaded and the pending breakpoints are bound to the source. It is at this time the breakpoint location is validated. This method is a fast way to determine if a breakpoint can be set at a particular location without loading the debug engine. - /// - /// - /// You can implement this method to call the ParseSource method with the parse reason of CodeSpan. - /// The parser examines the specified location and returns a span identifying the code at that - /// location. If there is code at the location, the span identifying that code should be passed to - /// your implementation of the CodeSpan method in your version of the AuthoringSink class. Then your - /// implementation of the ValidateBreakpointLocation method retrieves that span from your version of - /// the AuthoringSink class and returns that span in the pCodeSpan argument. - /// - /// - /// The base method returns E_NOTIMPL. - /// - /// - public override int ValidateBreakpointLocation(IVsTextBuffer buffer, int line, int col, TextSpan[] pCodeSpan) - { - // TODO: Add code to not allow breakpoints to be placed on non-code lines. - // TODO: Refactor to allow breakpoint locations to span multiple lines. - if (pCodeSpan != null) - { - pCodeSpan[0].iStartLine = line; - pCodeSpan[0].iStartIndex = col; - pCodeSpan[0].iEndLine = line; - pCodeSpan[0].iEndIndex = col; - if (buffer != null) - { - int length; - buffer.GetLengthOfLine(line, out length); - pCodeSpan[0].iStartIndex = 0; - pCodeSpan[0].iEndIndex = length; - } - return VSConstants.S_OK; - } - else - { - return VSConstants.S_FALSE; - } - } - - public override ViewFilter CreateViewFilter(CodeWindowManager mgr, IVsTextView newView) - { - return new IronyViewFilter(mgr, newView); - } - - public override string Name - { - get { return Configuration.Name; } - } - - public override string GetFormatFilterList() - { - return Configuration.FormatList; - } - } -} \ No newline at end of file diff --git a/Util/VS2010/Chalice/ChaliceLanguageService/Integration/IronyViewFilter.cs b/Util/VS2010/Chalice/ChaliceLanguageService/Integration/IronyViewFilter.cs deleted file mode 100644 index 55c3509e..00000000 --- a/Util/VS2010/Chalice/ChaliceLanguageService/Integration/IronyViewFilter.cs +++ /dev/null @@ -1,42 +0,0 @@ -using System; -using System.Collections.Generic; -using System.Linq; -using System.Text; -using Microsoft.VisualStudio.Package; -using Microsoft.VisualStudio.TextManager.Interop; - -using VsCommands2K = Microsoft.VisualStudio.VSConstants.VSStd2KCmdID; - -namespace Demo -{ - public class IronyViewFilter : ViewFilter - { - public IronyViewFilter(CodeWindowManager mgr, IVsTextView view) - : base(mgr, view) - { - - } - - public override void HandlePostExec(ref Guid guidCmdGroup, uint nCmdId, uint nCmdexecopt, IntPtr pvaIn, IntPtr pvaOut, bool bufferWasChanged) - { - if (guidCmdGroup == typeof(VsCommands2K).GUID) - { - VsCommands2K cmd = (VsCommands2K)nCmdId; - switch (cmd) - { - case VsCommands2K.UP: - case VsCommands2K.UP_EXT: - case VsCommands2K.UP_EXT_COL: - case VsCommands2K.DOWN: - case VsCommands2K.DOWN_EXT: - case VsCommands2K.DOWN_EXT_COL: - Source.OnCommand(TextView, cmd, '\0'); - return; - } - } - - - base.HandlePostExec(ref guidCmdGroup, nCmdId, nCmdexecopt, pvaIn, pvaOut, bufferWasChanged); - } - } -} diff --git a/Util/VS2010/Chalice/ChaliceLanguageService/Integration/LineScanner.cs b/Util/VS2010/Chalice/ChaliceLanguageService/Integration/LineScanner.cs deleted file mode 100644 index 966e9c43..00000000 --- a/Util/VS2010/Chalice/ChaliceLanguageService/Integration/LineScanner.cs +++ /dev/null @@ -1,58 +0,0 @@ -using System; -using Microsoft.VisualStudio.Package; -using Irony.Parsing; - -namespace Demo -{ - public class LineScanner : IScanner - { - private Parser parser; - - public LineScanner(Grammar grammar) - { - this.parser = new Parser(grammar); - this.parser.Context.Mode = ParseMode.VsLineScan; - } - - public bool ScanTokenAndProvideInfoAboutIt(TokenInfo tokenInfo, ref int state) - { - // Reads each token in a source line and performs syntax coloring. It will continue to - // be called for the source until false is returned. - Token token = parser.Scanner.VsReadToken(ref state); - - // !EOL and !EOF - if (token != null && token.Terminal != Grammar.CurrentGrammar.Eof && token.Category != TokenCategory.Error) - { - tokenInfo.StartIndex = token.Location.Position; - tokenInfo.EndIndex = tokenInfo.StartIndex + token.Length - 1; - if (token.EditorInfo != null) { - tokenInfo.Color = (Microsoft.VisualStudio.Package.TokenColor)token.EditorInfo.Color; - tokenInfo.Type = (Microsoft.VisualStudio.Package.TokenType)token.EditorInfo.Type; - } - - if (token.KeyTerm != null && token.KeyTerm.EditorInfo != null) - { - tokenInfo.Trigger = - (Microsoft.VisualStudio.Package.TokenTriggers)token.KeyTerm.EditorInfo.Triggers; - } - else - { - if (token.EditorInfo != null) { - tokenInfo.Trigger = - (Microsoft.VisualStudio.Package.TokenTriggers)token.EditorInfo.Triggers; - } - } - - return true; - } - - return false; - } - - public void SetSource(string source, int offset) - { - // Stores line of source to be used by ScanTokenAndProvideInfoAboutIt. - parser.Scanner.VsSetSource(source, offset); - } - } -} diff --git a/Util/VS2010/Chalice/ChaliceLanguageService/Integration/Method.cs b/Util/VS2010/Chalice/ChaliceLanguageService/Integration/Method.cs deleted file mode 100644 index c5071612..00000000 --- a/Util/VS2010/Chalice/ChaliceLanguageService/Integration/Method.cs +++ /dev/null @@ -1,20 +0,0 @@ -using System; -using System.Collections.Generic; - -namespace Demo -{ - public struct Method - { - public string Name; - public string Description; - public string Type; - public IList Parameters; - } - - public struct Parameter - { - public string Name; - public string Display; - public string Description; - } -} \ No newline at end of file diff --git a/Util/VS2010/Chalice/ChaliceLanguageService/Integration/Methods.cs b/Util/VS2010/Chalice/ChaliceLanguageService/Integration/Methods.cs deleted file mode 100644 index 1d7c124f..00000000 --- a/Util/VS2010/Chalice/ChaliceLanguageService/Integration/Methods.cs +++ /dev/null @@ -1,50 +0,0 @@ -using System; -using System.Collections.Generic; -using System.Text; -using Microsoft.VisualStudio.TextManager.Interop; -using Microsoft.VisualStudio.Package; - -namespace Demo -{ - public class Methods : Microsoft.VisualStudio.Package.Methods - { - IList methods; - public Methods(IList methods) - { - this.methods = methods; - } - - public override int GetCount() - { - return methods.Count; - } - - public override string GetName(int index) - { - return methods[index].Name; - } - - public override string GetDescription(int index) - { - return methods[index].Description; - } - - public override string GetType(int index) - { - return methods[index].Type; - } - - public override int GetParameterCount(int index) - { - return (methods[index].Parameters == null) ? 0 : methods[index].Parameters.Count; - } - - public override void GetParameterInfo(int index, int paramIndex, out string name, out string display, out string description) - { - Parameter parameter = methods[index].Parameters[paramIndex]; - name = parameter.Name; - display = parameter.Display; - description = parameter.Description; - } - } -} \ No newline at end of file diff --git a/Util/VS2010/Chalice/ChaliceLanguageService/Integration/Package.cs b/Util/VS2010/Chalice/ChaliceLanguageService/Integration/Package.cs deleted file mode 100644 index dc1244d6..00000000 --- a/Util/VS2010/Chalice/ChaliceLanguageService/Integration/Package.cs +++ /dev/null @@ -1,130 +0,0 @@ -using System; -using System.Collections.Generic; -using System.Text; -using System.Runtime.InteropServices; -using Microsoft.VisualStudio.OLE.Interop; -using MPF = Microsoft.VisualStudio.Package; -using System.ComponentModel.Design; - -namespace Demo -{ - public class IronyPackage : Microsoft.VisualStudio.Shell.Package, IOleComponent - { - uint componentID = 0; - public IronyPackage() - { - ServiceCreatorCallback callback = new ServiceCreatorCallback( - delegate(IServiceContainer container, Type serviceType) - { - if (typeof(IronyLanguageService) == serviceType) - { - IronyLanguageService language = new IronyLanguageService(); - language.SetSite(this); - - // register for idle time callbacks - IOleComponentManager mgr = GetService(typeof(SOleComponentManager)) as IOleComponentManager; - if (componentID == 0 && mgr != null) - { - OLECRINFO[] crinfo = new OLECRINFO[1]; - crinfo[0].cbSize = (uint)Marshal.SizeOf(typeof(OLECRINFO)); - crinfo[0].grfcrf = (uint)_OLECRF.olecrfNeedIdleTime | - (uint)_OLECRF.olecrfNeedPeriodicIdleTime; - crinfo[0].grfcadvf = (uint)_OLECADVF.olecadvfModal | - (uint)_OLECADVF.olecadvfRedrawOff | - (uint)_OLECADVF.olecadvfWarningsOff; - crinfo[0].uIdleTimeInterval = 300; - int hr = mgr.FRegisterComponent(this, crinfo, out componentID); - } - - return language; - } - else - { - return null; - } - }); - - // proffer the LanguageService - (this as IServiceContainer).AddService(typeof(IronyLanguageService), callback, true); - } - - protected override void Dispose(bool disposing) - { - try - { - if (componentID != 0) - { - IOleComponentManager mgr = GetService(typeof(SOleComponentManager)) as IOleComponentManager; - if (mgr != null) - { - mgr.FRevokeComponent(componentID); - } - componentID = 0; - } - } - finally - { - base.Dispose(disposing); - } - } - - #region IOleComponent Members - public int FContinueMessageLoop(uint uReason, IntPtr pvLoopData, MSG[] pMsgPeeked) - { - return 1; - } - - public int FDoIdle(uint grfidlef) - { - IronyLanguageService ls = GetService(typeof(IronyLanguageService)) as IronyLanguageService; - - if (ls != null) - { - ls.OnIdle((grfidlef & (uint)_OLEIDLEF.oleidlefPeriodic) != 0); - } - - return 0; - } - - public int FPreTranslateMessage(MSG[] pMsg) - { - return 0; - } - - public int FQueryTerminate(int fPromptUser) - { - return 1; - } - - public int FReserved1(uint dwReserved, uint message, IntPtr wParam, IntPtr lParam) - { - return 1; - } - - public IntPtr HwndGetWindow(uint dwWhich, uint dwReserved) - { - return IntPtr.Zero; - } - - public void OnActivationChange(IOleComponent pic, int fSameComponent, OLECRINFO[] pcrinfo, int fHostIsActivating, OLECHOSTINFO[] pchostinfo, uint dwReserved) - { - } - - public void OnAppActivate(int fActive, uint dwOtherThreadID) - { - } - - public void OnEnterState(uint uStateID, int fEnter) - { - } - - public void OnLoseActivation() - { - } - - public void Terminate() - { - } - #endregion - } -} \ No newline at end of file diff --git a/Util/VS2010/Chalice/ChaliceLanguageService/Integration/Resolver.cs b/Util/VS2010/Chalice/ChaliceLanguageService/Integration/Resolver.cs deleted file mode 100644 index 9f6ddeba..00000000 --- a/Util/VS2010/Chalice/ChaliceLanguageService/Integration/Resolver.cs +++ /dev/null @@ -1,50 +0,0 @@ -using System; -using System.Collections.Generic; -using System.Text; -using Irony.Parsing; - -namespace Demo -{ - public class Resolver : Demo.IASTResolver - { - #region IASTResolver Members - - - public IList FindCompletions(object result, int line, int col) - { - // Used for intellisense. - List declarations = new List(); - - // Add keywords defined by grammar - foreach (KeyTerm key in Configuration.Grammar.KeyTerms.Values) - { - if(key.OptionIsSet(TermOptions.IsKeyword)) - { - declarations.Add(new Declaration("", key.Name, 206, key.Name)); - } - } - - declarations.Sort(); - return declarations; - } - - public IList FindMembers(object result, int line, int col) - { - List members = new List(); - - return members; - } - - public string FindQuickInfo(object result, int line, int col) - { - return "unknown"; - } - - public IList FindMethods(object result, int line, int col, string name) - { - return new List(); - } - - #endregion - } -} diff --git a/Util/VS2010/Chalice/ChaliceLanguageService/Integration/Source.cs b/Util/VS2010/Chalice/ChaliceLanguageService/Integration/Source.cs deleted file mode 100644 index 418bec01..00000000 --- a/Util/VS2010/Chalice/ChaliceLanguageService/Integration/Source.cs +++ /dev/null @@ -1,41 +0,0 @@ -/*************************************************************************** - -Copyright (c) Microsoft Corporation. All rights reserved. -This code is licensed under the Visual Studio SDK license terms. -THIS CODE IS PROVIDED *AS IS* WITHOUT WARRANTY OF -ANY KIND, EITHER EXPRESS OR IMPLIED, INCLUDING ANY -IMPLIED WARRANTIES OF FITNESS FOR A PARTICULAR -PURPOSE, MERCHANTABILITY, OR NON-INFRINGEMENT. - -***************************************************************************/ - -using System; -using System.Collections.Generic; -using System.Text; -using Microsoft.VisualStudio.TextManager.Interop; -using Microsoft.VisualStudio.Package; - -namespace Demo -{ - public class Source : Microsoft.VisualStudio.Package.Source - { - public Source(LanguageService service, IVsTextLines textLines, Colorizer colorizer) - : base(service, textLines, colorizer) - { - } - - private object parseResult; - public object ParseResult - { - get { return parseResult; } - set { parseResult = value; } - } - - private IList braces; - public IList Braces - { - get { return braces; } - set { braces = value; } - } - } -} \ No newline at end of file diff --git a/Util/VS2010/Chalice/ChaliceLanguageService/IronyLanguageServicePackage.cs b/Util/VS2010/Chalice/ChaliceLanguageService/IronyLanguageServicePackage.cs deleted file mode 100644 index 8b9cb825..00000000 --- a/Util/VS2010/Chalice/ChaliceLanguageService/IronyLanguageServicePackage.cs +++ /dev/null @@ -1,91 +0,0 @@ -// VsPkg.cs : Implementation of IronyLanguageService -// - -using System; -using System.Diagnostics; -using System.Globalization; -using System.Runtime.InteropServices; -using System.ComponentModel.Design; -using Microsoft.Win32; -using Microsoft.VisualStudio.Shell.Interop; -using Microsoft.VisualStudio.OLE.Interop; -using Microsoft.VisualStudio.Shell; - -namespace Demo -{ - /// - /// This is the class that implements the package exposed by this assembly. - /// - /// The minimum requirement for a class to be considered a valid package for Visual Studio - /// is to implement the IVsPackage interface and register itself with the shell. - /// This package uses the helper classes defined inside the Managed Package Framework (MPF) - /// to do it: it derives from the Package class that provides the implementation of the - /// IVsPackage interface and uses the registration attributes defined in the framework to - /// register itself and its components with the shell. - /// - // This attribute tells the registration utility (regpkg.exe) that this class needs - // to be registered as package. - [PackageRegistration(UseManagedResourcesOnly = true)] - // A Visual Studio component can be registered under different regitry roots; for instance - // when you debug your package you want to register it in the experimental hive. This - // attribute specifies the registry root to use if no one is provided to regpkg.exe with - // the /root switch. - [DefaultRegistryRoot("Software\\Microsoft\\VisualStudio\\10.0Exp")] - // This attribute is used to register the informations needed to show the this package - // in the Help/About dialog of Visual Studio. - [InstalledProductRegistration(/*false,*/ "#110", "#112", "1.0", IconResourceID = 400)] - // This attribute will make your language service accessible by other packages installed. - [ProvideService(typeof(IronyLanguageService))] - // This attribute(s) associates file extensions with your language service. -// [ProvideLanguageExtension(typeof(IronyLanguageService), ".myc")] - [ProvideLanguageExtension(typeof(IronyLanguageService), ".chalice")] - - // This attributes informs Visual Studio that this package provides a langauge service and - // which features are implemented. - [ProvideLanguageService(typeof(IronyLanguageService), Configuration.Name, 0, - CodeSense = true, - EnableCommenting = true, - MatchBraces = true, - MatchBracesAtCaret = true, - ShowMatchingBrace = true, - AutoOutlining = true)] - // In order be loaded inside Visual Studio in a machine that has not the VS SDK installed, - // package needs to have a valid load key (it can be requested at - // http://msdn.microsoft.com/vstudio/extend/). This attributes tells the shell that this - // package has a load key embedded in its resources. - [ProvideLoadKey("Standard", "1.0", "Chalice", "Demo", 104)] - [Guid(GuidList.guidIronyLanguageServicePkgString)] - public sealed class MyCLanguageService : IronyPackage - { - /// - /// Default constructor of the package. - /// Inside this method you can place any initialization code that does not require - /// any Visual Studio service because at this point the package object is created but - /// not sited yet inside Visual Studio environment. The place to do all the other - /// initialization is the Initialize method. - /// - public MyCLanguageService() - { - Trace.WriteLine(string.Format(CultureInfo.CurrentCulture, "Entering constructor for: {0}", this.ToString())); - } - - - - ///////////////////////////////////////////////////////////////////////////// - // Overriden Package Implementation - #region Package Members - - /// - /// Initialization of the package; this method is called right after the package is sited, so this is the place - /// where you can put all the initilaization code that rely on services provided by VisualStudio. - /// - protected override void Initialize() - { - Trace.WriteLine(string.Format(CultureInfo.CurrentCulture, "Entering Initialize() of: {0}", this.ToString())); - base.Initialize(); - - } - #endregion - - } -} \ No newline at end of file diff --git a/Util/VS2010/Chalice/ChaliceLanguageService/Key.snk b/Util/VS2010/Chalice/ChaliceLanguageService/Key.snk deleted file mode 100644 index f80a4ceb..00000000 Binary files a/Util/VS2010/Chalice/ChaliceLanguageService/Key.snk and /dev/null differ diff --git a/Util/VS2010/Chalice/ChaliceLanguageService/Properties/AssemblyInfo.cs b/Util/VS2010/Chalice/ChaliceLanguageService/Properties/AssemblyInfo.cs deleted file mode 100644 index 118d4488..00000000 --- a/Util/VS2010/Chalice/ChaliceLanguageService/Properties/AssemblyInfo.cs +++ /dev/null @@ -1,36 +0,0 @@ -using System; -using System.Reflection; -using System.Resources; -using System.Runtime.CompilerServices; -using System.Runtime.InteropServices; - -// General Information about an assembly is controlled through the following -// set of attributes. Change these attribute values to modify the information -// associated with an assembly. -[assembly: AssemblyTitle("Package Name")] -[assembly: AssemblyDescription("")] -[assembly: AssemblyConfiguration("")] -[assembly: AssemblyCompany("Company")] -[assembly: AssemblyProduct("Package Name")] -[assembly: AssemblyCopyright("")] -[assembly: AssemblyTrademark("")] -[assembly: AssemblyCulture("")] -[assembly: ComVisible(false)] -[assembly: CLSCompliant(false)] -[assembly: NeutralResourcesLanguage("en-US")] - -// Version information for an assembly consists of the following four values: -// -// Major Version -// Minor Version -// Build Number -// Revision -// -// You can specify all the values or you can default the Revision and Build Numbers -// by using the '*' as shown below: - -[assembly: AssemblyVersion("1.0.0.0")] -[assembly: AssemblyFileVersion("1.0.0.0")] - - - diff --git a/Util/VS2010/Chalice/ChaliceLanguageService/Resources.Designer.cs b/Util/VS2010/Chalice/ChaliceLanguageService/Resources.Designer.cs deleted file mode 100644 index cd9f79db..00000000 --- a/Util/VS2010/Chalice/ChaliceLanguageService/Resources.Designer.cs +++ /dev/null @@ -1,63 +0,0 @@ -//------------------------------------------------------------------------------ -// -// This code was generated by a tool. -// Runtime Version:4.0.21006.1 -// -// Changes to this file may cause incorrect behavior and will be lost if -// the code is regenerated. -// -//------------------------------------------------------------------------------ - -namespace Demo { - using System; - - - /// - /// A strongly-typed resource class, for looking up localized strings, etc. - /// - // This class was auto-generated by the StronglyTypedResourceBuilder - // class via a tool like ResGen or Visual Studio. - // To add or remove a member, edit your .ResX file then rerun ResGen - // with the /str option, or rebuild your VS project. - [global::System.CodeDom.Compiler.GeneratedCodeAttribute("System.Resources.Tools.StronglyTypedResourceBuilder", "4.0.0.0")] - [global::System.Diagnostics.DebuggerNonUserCodeAttribute()] - [global::System.Runtime.CompilerServices.CompilerGeneratedAttribute()] - internal class Resources { - - private static global::System.Resources.ResourceManager resourceMan; - - private static global::System.Globalization.CultureInfo resourceCulture; - - [global::System.Diagnostics.CodeAnalysis.SuppressMessageAttribute("Microsoft.Performance", "CA1811:AvoidUncalledPrivateCode")] - internal Resources() { - } - - /// - /// Returns the cached ResourceManager instance used by this class. - /// - [global::System.ComponentModel.EditorBrowsableAttribute(global::System.ComponentModel.EditorBrowsableState.Advanced)] - internal static global::System.Resources.ResourceManager ResourceManager { - get { - if (object.ReferenceEquals(resourceMan, null)) { - global::System.Resources.ResourceManager temp = new global::System.Resources.ResourceManager("Demo.MyCLanguageService.Resources", typeof(Resources).Assembly); - resourceMan = temp; - } - return resourceMan; - } - } - - /// - /// Overrides the current thread's CurrentUICulture property for all - /// resource lookups using this strongly typed resource class. - /// - [global::System.ComponentModel.EditorBrowsableAttribute(global::System.ComponentModel.EditorBrowsableState.Advanced)] - internal static global::System.Globalization.CultureInfo Culture { - get { - return resourceCulture; - } - set { - resourceCulture = value; - } - } - } -} diff --git a/Util/VS2010/Chalice/ChaliceLanguageService/Resources.resx b/Util/VS2010/Chalice/ChaliceLanguageService/Resources.resx deleted file mode 100644 index 03fef612..00000000 --- a/Util/VS2010/Chalice/ChaliceLanguageService/Resources.resx +++ /dev/null @@ -1,130 +0,0 @@ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - text/microsoft-resx - - - 2.0 - - - System.Resources.ResXResourceReader, System.Windows.Forms, Version=2.0.0.0, Culture=neutral, PublicKeyToken=b77a5c561934e089 - - - System.Resources.ResXResourceWriter, System.Windows.Forms, Version=2.0.0.0, Culture=neutral, PublicKeyToken=b77a5c561934e089 - - - \ No newline at end of file diff --git a/Util/VS2010/Chalice/ChaliceLanguageService/Resources/Irony.dll b/Util/VS2010/Chalice/ChaliceLanguageService/Resources/Irony.dll deleted file mode 100644 index e2021a72..00000000 Binary files a/Util/VS2010/Chalice/ChaliceLanguageService/Resources/Irony.dll and /dev/null differ diff --git a/Util/VS2010/Chalice/ChaliceLanguageService/VSPackage.resx b/Util/VS2010/Chalice/ChaliceLanguageService/VSPackage.resx deleted file mode 100644 index 4c4adabd..00000000 --- a/Util/VS2010/Chalice/ChaliceLanguageService/VSPackage.resx +++ /dev/null @@ -1,129 +0,0 @@ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - text/microsoft-resx - - - 2.0 - - - System.Resources.ResXResourceReader, System.Windows.Forms, Version=2.0.0.0, Culture=neutral, PublicKeyToken=b77a5c561934e089 - - - System.Resources.ResXResourceWriter, System.Windows.Forms, Version=2.0.0.0, Culture=neutral, PublicKeyToken=b77a5c561934e089 - - - Paste PLK Here - - - Chalice - - - Chalice Programming Language - - \ No newline at end of file diff --git a/Util/VS2010/Chalice/ChaliceLanguageService/source.extension.vsixmanifest b/Util/VS2010/Chalice/ChaliceLanguageService/source.extension.vsixmanifest deleted file mode 100644 index 15fd4e9a..00000000 --- a/Util/VS2010/Chalice/ChaliceLanguageService/source.extension.vsixmanifest +++ /dev/null @@ -1,27 +0,0 @@ - - - - - ChaliceService - Microsoft Research - 1.0 - Information about my package - 1033 - - - - Pro - VST_All - - - - - - - - - - ChaliceService.pkgdef - - - diff --git a/Util/VS2010/Chalice/StartChalice.bat b/Util/VS2010/Chalice/StartChalice.bat deleted file mode 100644 index e2de0e65..00000000 --- a/Util/VS2010/Chalice/StartChalice.bat +++ /dev/null @@ -1,10 +0,0 @@ -@echo off -echo ---------- Starting ------------ < nul >> c:\tmp\coo.out -time < nul >> c:\tmp\coo.out -echo. < nul >> c:\tmp\coo.out - -call "c:\Program Files\Scala\bin\scala" -cp c:\boogie\Chalice\target\scala-2.8.1.final\classes chalice.Chalice /boogieOpt:nologo /vs %* 2>> c:\tmp\coo.out - -time < nul >> c:\tmp\coo.out -echo. < nul >> c:\tmp\coo.out -echo ---------- Done ------------ < nul >> c:\tmp\coo.out diff --git a/Util/VS2010/Dafny/DafnyLanguageService.sln b/Util/VS2010/Dafny/DafnyLanguageService.sln deleted file mode 100644 index d900cbb5..00000000 --- a/Util/VS2010/Dafny/DafnyLanguageService.sln +++ /dev/null @@ -1,20 +0,0 @@ - -Microsoft Visual Studio Solution File, Format Version 11.00 -# Visual Studio 2010 -Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "DafnyLanguageService", "DafnyLanguageService\DafnyLanguageService.csproj", "{66E611EE-84D8-4EB9-9A33-164A53E00553}" -EndProject -Global - GlobalSection(SolutionConfigurationPlatforms) = preSolution - Debug|Any CPU = Debug|Any CPU - Release|Any CPU = Release|Any CPU - EndGlobalSection - GlobalSection(ProjectConfigurationPlatforms) = postSolution - {66E611EE-84D8-4EB9-9A33-164A53E00553}.Debug|Any CPU.ActiveCfg = Debug|Any CPU - {66E611EE-84D8-4EB9-9A33-164A53E00553}.Debug|Any CPU.Build.0 = Debug|Any CPU - {66E611EE-84D8-4EB9-9A33-164A53E00553}.Release|Any CPU.ActiveCfg = Release|Any CPU - {66E611EE-84D8-4EB9-9A33-164A53E00553}.Release|Any CPU.Build.0 = Release|Any CPU - EndGlobalSection - GlobalSection(SolutionProperties) = preSolution - HideSolutionNode = FALSE - EndGlobalSection -EndGlobal diff --git a/Util/VS2010/Dafny/DafnyLanguageService/Configuration.cs b/Util/VS2010/Dafny/DafnyLanguageService/Configuration.cs deleted file mode 100644 index f32c75ab..00000000 --- a/Util/VS2010/Dafny/DafnyLanguageService/Configuration.cs +++ /dev/null @@ -1,24 +0,0 @@ -using System; -using System.Collections.Generic; -using Microsoft.VisualStudio.Package; -using Microsoft.VisualStudio.TextManager.Interop; - -namespace Demo -{ - public static partial class Configuration - { - public const string Name = "Dafny"; - public const string FormatList = "Dafny File (*.dfy)\n*.dfy"; - - static Configuration() - { - // default colors - currently, these need to be declared - CreateColor("Keyword", COLORINDEX.CI_BLUE, COLORINDEX.CI_USERTEXT_BK); - CreateColor("Comment", COLORINDEX.CI_DARKGREEN, COLORINDEX.CI_USERTEXT_BK); - CreateColor("Identifier", COLORINDEX.CI_SYSPLAINTEXT_FG, COLORINDEX.CI_USERTEXT_BK); - CreateColor("String", COLORINDEX.CI_MAROON, COLORINDEX.CI_USERTEXT_BK); - CreateColor("Number", COLORINDEX.CI_RED, COLORINDEX.CI_USERTEXT_BK); - CreateColor("Text", COLORINDEX.CI_SYSPLAINTEXT_FG, COLORINDEX.CI_USERTEXT_BK); - } - } -} diff --git a/Util/VS2010/Dafny/DafnyLanguageService/DafnyLanguageService.csproj b/Util/VS2010/Dafny/DafnyLanguageService/DafnyLanguageService.csproj deleted file mode 100644 index 175c12dc..00000000 --- a/Util/VS2010/Dafny/DafnyLanguageService/DafnyLanguageService.csproj +++ /dev/null @@ -1,179 +0,0 @@ - - - - Debug - AnyCPU - 9.0.30729 - 2.0 - Library - Properties - Demo.DafnyLanguageService - DafnyLanguageService - True - Key.snk - v4.0 - {66E611EE-84D8-4EB9-9A33-164A53E00553} - - - 4.0 - - - publish\ - true - Disk - false - Foreground - 7 - Days - false - false - true - 0 - 1.0.0.%2a - false - false - true - - - - true - full - false - bin\Debug\ - DEBUG;TRACE - prompt - 4 - AllRules.ruleset - - - pdbonly - true - bin\Release\ - TRACE - prompt - 4 - true - AllRules.ruleset - - - - False - Resources\Irony.dll - - - - False - C:\Program Files\Microsoft Visual Studio 2010 Beta2 SDK\VisualStudioIntegration\Common\Assemblies\Microsoft.VisualStudio.Package.LanguageService.10.0.dll - - - C:\Program Files\Microsoft Visual Studio 2010 Beta2 SDK\VisualStudioIntegration\Common\Assemblies\Microsoft.VisualStudio.Shell.10.0.dll - - - False - C:\Program Files\Microsoft Visual Studio 2010 Beta2 SDK\VisualStudioIntegration\Common\Assemblies\Microsoft.VisualStudio.Shell.Immutable.10.0.dll - - - - False - True - C:\Program Files\Microsoft Visual Studio 2010 Beta2 SDK\VisualStudioIntegration\Common\Assemblies\Microsoft.VisualStudio.Shell.Interop.10.0.dll - - - - - - False - ..\..\..\..\..\Program Files\Microsoft Visual Studio 2008 SDK\VisualStudioIntegration\Common\Assemblies\Microsoft.VisualStudio.TextManager.Interop.8.0.dll - - - - - - - - - - - - - - - - - - - - - - - - - - - True - True - Resources.resx - - - - - - - - ResXFileCodeGenerator - Resources.Designer.cs - Designer - - - true - Designer - - - - - - - - - - - - False - .NET Framework 3.5 SP1 Client Profile - false - - - False - .NET Framework 3.5 SP1 - true - - - False - Microsoft Visual Basic PowerPacks 10.0 - true - - - False - Windows Installer 3.1 - true - - - - - true - true - - - - - \ No newline at end of file diff --git a/Util/VS2010/Dafny/DafnyLanguageService/GlobalSuppressions.cs b/Util/VS2010/Dafny/DafnyLanguageService/GlobalSuppressions.cs deleted file mode 100644 index f0857cbb..00000000 --- a/Util/VS2010/Dafny/DafnyLanguageService/GlobalSuppressions.cs +++ /dev/null @@ -1,11 +0,0 @@ -// This file is used by Code Analysis to maintain SuppressMessage -// attributes that are applied to this project. Project-level -// suppressions either have no target or are given a specific target -// and scoped to a namespace, type, member, etc. -// -// To add a suppression to this file, right-click the message in the -// Error List, point to "Suppress Message(s)", and click "In Project -// Suppression File". You do not need to add suppressions to this -// file manually. - -[assembly: System.Diagnostics.CodeAnalysis.SuppressMessage("Microsoft.Design", "CA1017:MarkAssembliesWithComVisible")] diff --git a/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs b/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs deleted file mode 100644 index ac1b755c..00000000 --- a/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs +++ /dev/null @@ -1,388 +0,0 @@ -using System; -using System.Collections.Generic; -using System.Linq; -using Irony.Parsing; - -namespace Demo -{ - [Language("Dafny", "1.0", "Dafny Programming Language")] - public class Grammar : Irony.Parsing.Grammar - { - public Grammar() { - #region 1. Terminals - NumberLiteral n = TerminalFactory.CreateCSharpNumber("number"); - - IdentifierTerminal ident = new IdentifierTerminal("Identifier", "'_?", "'_?"); - - StringLiteral stringLiteral = TerminalFactory.CreateCSharpString("String"); - - this.MarkReservedWords( // NOTE: these keywords must also appear once more below - "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", "yield", "parallel", "print", - "returns", "yields", "requires", "ensures", "modifies", "reads", "decreases", - "bool", "nat", "int", "false", "true", "null", - "function", "predicate", "copredicate", "free", - "in", "forall", "exists", - "seq", "set", "map", "multiset", "array", "array2", "array3", - "match", "case", - "fresh", "old", "choose", "where", "calc" - ); - - StringLiteral s = new StringLiteral("String", "'", StringFlags.AllowsDoubledQuote); - - Terminal dot = ToTerm(".", "dot"); - Terminal less = ToTerm("<"); - Terminal greater = ToTerm(">"); - Terminal arrow = ToTerm("=>"); - Terminal LBracket = ToTerm("["); - Terminal RBracket = ToTerm("]"); - Terminal LParen = ToTerm("("); - Terminal RParen = ToTerm(")"); - Terminal RCurly = ToTerm("}"); - Terminal LCurly = ToTerm("{"); - Terminal LMb = ToTerm("<["); - Terminal RMb = ToTerm("]>"); - Terminal comma = ToTerm(","); - Terminal semicolon = ToTerm(";"); - Terminal colon = ToTerm(":"); - - #endregion - - #region 2. Non-terminals - #region 2.1 Expressions - NonTerminal expression = new NonTerminal("Expr"); - NonTerminal BinOp = new NonTerminal("BinOp"); - NonTerminal LUnOp = new NonTerminal("LUnOp"); - NonTerminal RUnOp = new NonTerminal("RUnOp"); - - NonTerminal ArrayConstructor = new NonTerminal("ArrayConstructor"); - NonTerminal MObjectConstructor = new NonTerminal("MObjectConstructor"); - NonTerminal MObjectList = new NonTerminal("MObjectList"); - #endregion - - #region 2.2 QualifiedName - //Expression List: expr1, expr2, expr3, .. - NonTerminal expressionList = new NonTerminal("ExprList"); - NonTerminal identList = new NonTerminal("identList"); - //A name in form: a.b.c().d[1,2].e .... - NonTerminal NewStmt = new NonTerminal("NewStmt"); - NonTerminal NewArrStmt = new NonTerminal("NewArrStmt"); - NonTerminal QualifiedName = new NonTerminal("QualifiedName"); - NonTerminal GenericsPostfix = new NonTerminal("GenericsPostfix"); - NonTerminal ArrayExpression = new NonTerminal("ArrayExpression"); - NonTerminal FunctionExpression = new NonTerminal("FunctionExpression"); - NonTerminal selectExpr = new NonTerminal("selectExpr"); - #endregion - - #region 2.3 Statement - NonTerminal Condition = new NonTerminal("Condition"); - - NonTerminal Statement = new NonTerminal("Statement"); - NonTerminal Statements = new NonTerminal("Statements"); - - //Block - NonTerminal blockStatement = new NonTerminal("CompoundStatement"); - #endregion - - #region 2.4 Program and Functions - NonTerminal Prog = new NonTerminal("Prog"); - NonTerminal anything = new NonTerminal("anything"); // temporary hack - NonTerminal declaration = new NonTerminal("declaration"); - NonTerminal classDecl = new NonTerminal("class decl"); - NonTerminal memberDecl = new NonTerminal("member decl"); - NonTerminal fieldDecl = new NonTerminal("field declaration"); - NonTerminal idType = new NonTerminal("identifier type"); - NonTerminal typeDecl = new NonTerminal("type reference"); - NonTerminal methodDecl = new NonTerminal("method declaration"); - NonTerminal formalParameters = new NonTerminal("formals"); - NonTerminal methodSpec = new NonTerminal("method spec"); - NonTerminal formalsList = new NonTerminal("ParamaterListOpt"); - NonTerminal functionDecl = new NonTerminal("function declaration"); - NonTerminal predicateDecl = new NonTerminal("predicate declaration"); - NonTerminal invariantDecl = new NonTerminal("invariant declaration"); - NonTerminal Semi = new NonTerminal("semi"); - NonTerminal Rhs = new NonTerminal("right-hand side"); - NonTerminal FieldInit = new NonTerminal("field init"); - NonTerminal FieldInits = new NonTerminal("field inits"); - NonTerminal installBounds = new NonTerminal("installBounds"); - NonTerminal localVarStmt = new NonTerminal("localVarStmt"); - NonTerminal evalstate = new NonTerminal("evalstate"); - NonTerminal channelDecl = new NonTerminal("channel declaration"); - NonTerminal loopSpec = new NonTerminal("loop specification"); - NonTerminal rdPermArg = new NonTerminal("rdPermArg"); - #endregion - - #endregion - - #region 3. BNF rules - - Semi.Rule = semicolon; - - #region 3.1 Expressions - selectExpr.Rule = (ToTerm("this") + ".").Q() + QualifiedName; - evalstate.Rule = - ident + ToTerm(".") + - (ToTerm("acquire") - | "release" - | "fork" + FunctionExpression - ) - ; - rdPermArg.Rule = ToTerm("*") | expression; - - expression.Rule = ToTerm("true") - | "false" - | "null" - | "maxlock" - | "lockbottom" - | "this" - | "result" - | s - | n - | QualifiedName - // The following is needed: to parse "A=" | "<=" | "is" - | "=" | "+=" | "-=" - | "." - | "==>" | "<==>" | "<<" - | "=" // this is for datatype declarations, not an operator - ; - - LUnOp.Rule = ToTerm("-") | "~" | "!"; - RUnOp.Rule = ToTerm("++") | "--"; - - ArrayConstructor.Rule = LBracket + expressionList + RBracket; - MObjectConstructor.Rule = LBracket + ident + arrow + expression + MObjectList.Star() + RBracket; - MObjectList.Rule = comma + ident + arrow + expression; - #endregion - - #region 3.2 QualifiedName - ArrayExpression.Rule = QualifiedName + LBracket + expressionList + RBracket; - FunctionExpression.Rule = QualifiedName + LParen + expressionList.Q() + RParen; - - QualifiedName.Rule = ident | QualifiedName + dot + ident; - - - GenericsPostfix.Rule = less + QualifiedName + greater; - - //ExprList.Rule = Expr.Plus(comma); - #endregion - - #region 3.3 Statement - Condition.Rule = LParen + expression + RParen; - installBounds.Rule - = "installBounds" - //= ToTerm("between") + expressionList + "and" + expressionList - //| "below" + expressionList - //| "below" + expressionList + "above" + expressionList - //| "above" + expressionList - //| "above" + expressionList + "below" + expressionList - ; - FieldInit.Rule - = ident + ":=" + expression - ; - FieldInits.Rule = MakeStarRule(FieldInits, ToTerm(","), FieldInit); - Rhs.Rule - = ToTerm("new") + ident - | ToTerm("new") + ident + "{" + FieldInits + "}" - | ToTerm("new") + ident + installBounds - | ToTerm("new") + ident + "{" + FieldInits + "}" + installBounds - | expression - ; - localVarStmt.Rule - = idType + ":=" + Rhs + Semi - | idType + Semi - ; - loopSpec.Rule - = ToTerm("invariant") + expression + Semi - | "lockchange" + expressionList + Semi - ; - - - - Statement.Rule = Semi - | "if" + Condition + Statement - | "if" + Condition + Statement + PreferShiftHere() + "else" + Statement - | "while" + Condition + loopSpec.Star() + Statement - | "for" + LParen + expression.Q() + Semi + expression.Q() + Semi + expression.Q() + RParen + Statement - | blockStatement - | expression + Semi - | "break" + Semi - | QualifiedName + ":=" + Rhs - - | "var" + localVarStmt - - | "assert" + expression + Semi - | "assume" + expression + Semi - - ; - Statements.Rule = MakeStarRule(Statements, null, Statement); - blockStatement.Rule = LCurly + Statements + RCurly; - - - #endregion - - #region 3.4 Prog - Prog.Rule = anything.Star() + Eof; - - anything.Rule - = ToTerm("class") - | "ghost" - | "static" - | "var" - | "method" - | "constructor" - | "datatype" - | "codatatype" - | "type" - | "iterator" - | "assert" - | "assume" - | "new" - | "this" - | "object" - | "refines" - | "module" - | "import" - | "default" - | "opened" - | "as" - | "if" - | "then" - | "else" - | "while" - | "invariant" - | "break" - | "label" - | "return" - | "yield" - | "parallel" - | "calc" - | "print" - | "returns" - | "yields" - | "requires" - | "ensures" - | "modifies" - | "reads" - | "decreases" - | "bool" - | "nat" - | "int" - | "false" - | "true" - | "null" - | "function" - | "predicate" - | "copredicate" - | "free" - | "in" - | "forall" - | "exists" - | "seq" - | "set" - | "map" - | "multiset" - | "array" - | "array2" - | "array3" - | "match" - | "case" - | "fresh" - | "old" - | "choose" - | "where" - | ident - | "}" - | "{" - | "(" - | ")" - | "[" - | "]" - | "," - | ":" - | ";" - | "=" // this is for datatype declarations, not an operator - | "." - | "`" - | "==" - | "!=" - | "<" - | "<=" - | ">=" - | ">" - | "=>" - | ":=" - | "+" - | "-" - | "*" - | "/" - | "%" - | "!!" - | "|" - | "!" - | "&&" - | "||" - | "==>" - | "<==>" - | "#" - | n - | stringLiteral - ; - - Terminal Comment = new CommentTerminal("Comment", "/*", "*/"); - NonGrammarTerminals.Add(Comment); - Terminal LineComment = new CommentTerminal("LineComment", "//", "\n"); - NonGrammarTerminals.Add(LineComment); - #endregion - #endregion - - #region 4. Set starting symbol - this.Root = Prog; // Set grammar root - #endregion - - #region 5. Operators precedence - // not used - #endregion - - #region 6. Punctuation symbols - RegisterPunctuation("(", ")", "[", "]", "{", "}", ",", ";"); - #endregion - } - } -} diff --git a/Util/VS2010/Dafny/DafnyLanguageService/Guids.cs b/Util/VS2010/Dafny/DafnyLanguageService/Guids.cs deleted file mode 100644 index 61ea05d4..00000000 --- a/Util/VS2010/Dafny/DafnyLanguageService/Guids.cs +++ /dev/null @@ -1,13 +0,0 @@ -using System; - -namespace Demo -{ - static class GuidList - { - public const string guidIronyLanguageServiceString = "1F9687D0-937C-428E-ACFF-A7622A14100C"; - public const string guidIronyLanguageServicePkgString = "F85E7515-4CA6-42A5-86E0-D2312AE91D23"; - public const string guidIronyLanguageServiceCmdSetString = "68251AE3-0205-4FC9-8B12-D4C3EA9F8D6C"; - - public static readonly Guid guidIronyLanguageServiceCmdSet = new Guid(guidIronyLanguageServiceCmdSetString); - }; -} \ No newline at end of file diff --git a/Util/VS2010/Dafny/DafnyLanguageService/Integration/AuthoringScope.cs b/Util/VS2010/Dafny/DafnyLanguageService/Integration/AuthoringScope.cs deleted file mode 100644 index 9a49dbe4..00000000 --- a/Util/VS2010/Dafny/DafnyLanguageService/Integration/AuthoringScope.cs +++ /dev/null @@ -1,66 +0,0 @@ -using System; -using System.Collections.Generic; -using Microsoft.VisualStudio; -using Microsoft.VisualStudio.TextManager.Interop; -using Microsoft.VisualStudio.Package; - -namespace Demo -{ - public class AuthoringScope : Microsoft.VisualStudio.Package.AuthoringScope - { - public AuthoringScope(object parseResult) - { - this.parseResult = parseResult; - - // how should this be set? - this.resolver = new Resolver(); - } - - object parseResult; - IASTResolver resolver; - - // ParseReason.QuickInfo - public override string GetDataTipText(int line, int col, out TextSpan span) - { - span = new TextSpan(); - return null; - } - - // ParseReason.CompleteWord - // ParseReason.DisplayMemberList - // ParseReason.MemberSelect - // ParseReason.MemberSelectAndHilightBraces - public override Microsoft.VisualStudio.Package.Declarations GetDeclarations(IVsTextView view, int line, int col, TokenInfo info, ParseReason reason) - { - IList declarations; - switch (reason) - { - case ParseReason.CompleteWord: - declarations = resolver.FindCompletions(parseResult, line, col); - break; - case ParseReason.DisplayMemberList: - case ParseReason.MemberSelect: - case ParseReason.MemberSelectAndHighlightBraces: - declarations = resolver.FindMembers(parseResult, line, col); - break; - default: - throw new ArgumentException("reason"); - } - - return new Declarations(declarations); - } - - // ParseReason.GetMethods - public override Microsoft.VisualStudio.Package.Methods GetMethods(int line, int col, string name) - { - return new Methods(resolver.FindMethods(parseResult, line, col, name)); - } - - // ParseReason.Goto - public override string Goto(VSConstants.VSStd97CmdID cmd, IVsTextView textView, int line, int col, out TextSpan span) - { - span = new TextSpan(); - return null; - } - } -} \ No newline at end of file diff --git a/Util/VS2010/Dafny/DafnyLanguageService/Integration/Configuration.cs b/Util/VS2010/Dafny/DafnyLanguageService/Integration/Configuration.cs deleted file mode 100644 index f7412393..00000000 --- a/Util/VS2010/Dafny/DafnyLanguageService/Integration/Configuration.cs +++ /dev/null @@ -1,116 +0,0 @@ -using System; -using System.Collections.Generic; -using Microsoft.VisualStudio.Package; -using Microsoft.VisualStudio.TextManager.Interop; - -namespace Demo -{ - public static partial class Configuration - { - public static Grammar Grammar = new Grammar(); - static List colorableItems = new List(); - - public static IList ColorableItems - { - get { return colorableItems; } - } - - public static TokenColor CreateColor(string name, COLORINDEX foreground, COLORINDEX background) - { - return CreateColor(name, foreground, background, false, false); - } - - public static TokenColor CreateColor(string name, COLORINDEX foreground, COLORINDEX background, bool bold, bool strikethrough) - { - colorableItems.Add(new ColorableItem(name, foreground, background, bold, strikethrough)); - return (TokenColor)colorableItems.Count; - } - - public static void ColorToken(string tokenName, TokenType type, TokenColor color, TokenTriggers trigger) - { - definitions[tokenName] = new TokenDefinition(type, color, trigger); - } - - public static TokenDefinition GetDefinition(string tokenName) - { - TokenDefinition result; - return definitions.TryGetValue(tokenName, out result) ? result : defaultDefinition; - } - - private static TokenDefinition defaultDefinition = new TokenDefinition(TokenType.Text, TokenColor.Text, TokenTriggers.None); - private static Dictionary definitions = new Dictionary(); - - public struct TokenDefinition - { - public TokenDefinition(TokenType type, TokenColor color, TokenTriggers triggers) - { - this.TokenType = type; - this.TokenColor = color; - this.TokenTriggers = triggers; - } - - public TokenType TokenType; - public TokenColor TokenColor; - public TokenTriggers TokenTriggers; - } - } - - public class ColorableItem : Microsoft.VisualStudio.TextManager.Interop.IVsColorableItem - { - private string displayName; - private COLORINDEX background; - private COLORINDEX foreground; - private uint fontFlags = (uint)FONTFLAGS.FF_DEFAULT; - - public ColorableItem(string displayName, COLORINDEX foreground, COLORINDEX background, bool bold, bool strikethrough) - { - this.displayName = displayName; - this.background = background; - this.foreground = foreground; - - if (bold) - this.fontFlags = this.fontFlags | (uint)FONTFLAGS.FF_BOLD; - if (strikethrough) - this.fontFlags = this.fontFlags | (uint)FONTFLAGS.FF_STRIKETHROUGH; - } - - #region IVsColorableItem Members - public int GetDefaultColors(COLORINDEX[] piForeground, COLORINDEX[] piBackground) - { - if (null == piForeground) - { - throw new ArgumentNullException("piForeground"); - } - if (0 == piForeground.Length) - { - throw new ArgumentOutOfRangeException("piForeground"); - } - piForeground[0] = foreground; - - if (null == piBackground) - { - throw new ArgumentNullException("piBackground"); - } - if (0 == piBackground.Length) - { - throw new ArgumentOutOfRangeException("piBackground"); - } - piBackground[0] = background; - - return Microsoft.VisualStudio.VSConstants.S_OK; - } - - public int GetDefaultFontFlags(out uint pdwFontFlags) - { - pdwFontFlags = this.fontFlags; - return Microsoft.VisualStudio.VSConstants.S_OK; - } - - public int GetDisplayName(out string pbstrName) - { - pbstrName = displayName; - return Microsoft.VisualStudio.VSConstants.S_OK; - } - #endregion - } -} \ No newline at end of file diff --git a/Util/VS2010/Dafny/DafnyLanguageService/Integration/Declaration.cs b/Util/VS2010/Dafny/DafnyLanguageService/Integration/Declaration.cs deleted file mode 100644 index c0fda5ca..00000000 --- a/Util/VS2010/Dafny/DafnyLanguageService/Integration/Declaration.cs +++ /dev/null @@ -1,30 +0,0 @@ -using System; -using System.Collections.Generic; - -namespace Demo -{ - public struct Declaration : IComparable - { - public Declaration(string description, string displayText, int glyph, string name) - { - this.Description = description; - this.DisplayText = displayText; - this.Glyph = glyph; - this.Name = name; - } - - public string Description; - public string DisplayText; - public int Glyph; - public string Name; - - #region IComparable Members - - public int CompareTo(Declaration other) - { - return DisplayText.CompareTo(other.DisplayText); - } - - #endregion - } -} \ No newline at end of file diff --git a/Util/VS2010/Dafny/DafnyLanguageService/Integration/Declarations.cs b/Util/VS2010/Dafny/DafnyLanguageService/Integration/Declarations.cs deleted file mode 100644 index 98a411ce..00000000 --- a/Util/VS2010/Dafny/DafnyLanguageService/Integration/Declarations.cs +++ /dev/null @@ -1,56 +0,0 @@ -/*************************************************************************** - -Copyright (c) Microsoft Corporation. All rights reserved. -This code is licensed under the Visual Studio SDK license terms. -THIS CODE IS PROVIDED *AS IS* WITHOUT WARRANTY OF -ANY KIND, EITHER EXPRESS OR IMPLIED, INCLUDING ANY -IMPLIED WARRANTIES OF FITNESS FOR A PARTICULAR -PURPOSE, MERCHANTABILITY, OR NON-INFRINGEMENT. - -***************************************************************************/ - -using System; -using System.Collections.Generic; -using System.Text; -using Microsoft.VisualStudio.TextManager.Interop; -using Microsoft.VisualStudio.Package; - -namespace Demo -{ - public class Declarations : Microsoft.VisualStudio.Package.Declarations - { - IList declarations; - public Declarations(IList declarations) - { - this.declarations = declarations; - } - - public override int GetCount() - { - return declarations.Count; - } - - public override string GetDescription(int index) - { - return declarations[index].Description; - } - - public override string GetDisplayText(int index) - { - return declarations[index].DisplayText; - } - - public override int GetGlyph(int index) - { - return declarations[index].Glyph; - } - - public override string GetName(int index) - { - if (index >= 0) - return declarations[index].Name; - - return null; - } - } -} \ No newline at end of file diff --git a/Util/VS2010/Dafny/DafnyLanguageService/Integration/IASTResolver.cs b/Util/VS2010/Dafny/DafnyLanguageService/Integration/IASTResolver.cs deleted file mode 100644 index 8de1a454..00000000 --- a/Util/VS2010/Dafny/DafnyLanguageService/Integration/IASTResolver.cs +++ /dev/null @@ -1,13 +0,0 @@ -using System; -using System.Collections.Generic; - -namespace Demo -{ - interface IASTResolver - { - IList FindCompletions(object result, int line, int col); - IList FindMembers(object result, int line, int col); - string FindQuickInfo(object result, int line, int col); - IList FindMethods(object result, int line, int col, string name); - } -} \ No newline at end of file diff --git a/Util/VS2010/Dafny/DafnyLanguageService/Integration/IronyLanguageService.cs b/Util/VS2010/Dafny/DafnyLanguageService/Integration/IronyLanguageService.cs deleted file mode 100644 index ce43e6e4..00000000 --- a/Util/VS2010/Dafny/DafnyLanguageService/Integration/IronyLanguageService.cs +++ /dev/null @@ -1,373 +0,0 @@ -using System; -using System.Collections.Generic; -using System.Diagnostics; -using Microsoft.VisualStudio; -using Microsoft.VisualStudio.TextManager.Interop; -using Microsoft.VisualStudio.Package; - -using Irony.Parsing; -using Irony.Ast; - -using System.IO; - -namespace Demo -{ - public class IronyLanguageService : Microsoft.VisualStudio.Package.LanguageService - { - private Grammar grammar; - private Parser parser; - private ParsingContext context; - - public IronyLanguageService() - { - grammar = new Grammar(); - parser = new Parser(Configuration.Grammar); - context = new ParsingContext(parser); - } - - - #region Custom Colors - public override int GetColorableItem(int index, out IVsColorableItem item) - { - if (index <= Configuration.ColorableItems.Count) - { - item = Configuration.ColorableItems[index - 1]; - return Microsoft.VisualStudio.VSConstants.S_OK; - } - else - { - throw new ArgumentNullException("index"); - } - } - - public override int GetItemCount(out int count) - { - count = Configuration.ColorableItems.Count; - return Microsoft.VisualStudio.VSConstants.S_OK; - } - #endregion - - #region MPF Accessor and Factory specialisation - private LanguagePreferences preferences; - public override LanguagePreferences GetLanguagePreferences() - { - if (this.preferences == null) - { - this.preferences = new LanguagePreferences(this.Site, - typeof(IronyLanguageService).GUID, - this.Name); - this.preferences.Init(); - } - - return this.preferences; - } - - public override Microsoft.VisualStudio.Package.Source CreateSource(IVsTextLines buffer) - { - return new Source(this, buffer, this.GetColorizer(buffer)); - } - - private IScanner scanner; - public override IScanner GetScanner(IVsTextLines buffer) - { - if (scanner == null) - this.scanner = new LineScanner(grammar); - - return this.scanner; - } - #endregion - - public override void OnIdle(bool periodic) - { - // from IronPythonLanguage sample - // this appears to be necessary to get a parse request with ParseReason = Check? - Source src = (Source)GetSource(this.LastActiveTextView); - if (src != null && src.LastParseTime >= Int32.MaxValue >> 12) - { - src.LastParseTime = 0; - } - base.OnIdle(periodic); - } - - public override Microsoft.VisualStudio.Package.AuthoringScope ParseSource(ParseRequest req) - { - Debug.Print("ParseSource at ({0}:{1}), reason {2}", req.Line, req.Col, req.Reason); - Source source = (Source)this.GetSource(req.FileName); - switch (req.Reason) - { - case ParseReason.Check: - // This is where you perform your syntax highlighting. - // Parse entire source as given in req.Text. - // Store results in the AuthoringScope object. - var parsed = parser.Parse(req.Text, req.FileName); - var root = parsed.Root; - if (root != null) { - - AstNode node = (AstNode)root.AstNode; - source.ParseResult = node; - } - - // Used for brace matching. - TokenStack braces = parser.Context.OpenBraces; - foreach (Token brace in braces) { - if (brace.OtherBrace == null) continue; - TextSpan openBrace = new TextSpan(); - openBrace.iStartLine = brace.Location.Line; - openBrace.iStartIndex = brace.Location.Column; - openBrace.iEndLine = brace.Location.Line; - openBrace.iEndIndex = openBrace.iStartIndex + brace.Length; - - TextSpan closeBrace = new TextSpan(); - closeBrace.iStartLine = brace.OtherBrace.Location.Line; - closeBrace.iStartIndex = brace.OtherBrace.Location.Column; - closeBrace.iEndLine = brace.OtherBrace.Location.Line; - closeBrace.iEndIndex = closeBrace.iStartIndex + brace.OtherBrace.Length; - - if (source.Braces == null) { - source.Braces = new List(); - } - source.Braces.Add(new TextSpan[2] { openBrace, closeBrace }); - } - - if (parser.Context.CurrentParseTree.ParserMessages.Count > 0) { - foreach (ParserMessage error in parser.Context.CurrentParseTree.ParserMessages) { - TextSpan span = new TextSpan(); - span.iStartLine = span.iEndLine = error.Location.Line - 1; - span.iStartIndex = error.Location.Column; - span.iEndIndex = error.Location.Position; - req.Sink.AddError(req.FileName, error.Message, span, Severity.Error); - } - } else { // parse looks okay, send it to Dafny. - if (!File.Exists(@"C:\tmp\StartDafny.bat")) { - AddErrorBecauseOfToolProblems(req, @"Can't find C:\tmp\StartDafny.bat"); - } else { - - // From: http://dotnetperls.com/process-redirect-standard-output - // (Also, see: http://msdn.microsoft.com/en-us/library/system.diagnostics.processstartinfo.redirectstandardoutput.aspx) - // - // Setup the process with the ProcessStartInfo class. - // - ProcessStartInfo start = new ProcessStartInfo(); - start.FileName = @"cmd.exe"; - start.Arguments = @"/c C:\tmp\StartDafny.bat"; // Specify exe name. - start.UseShellExecute = false; - start.RedirectStandardInput = true; - start.RedirectStandardOutput = true; - start.CreateNoWindow = true; - //start.WindowStyle = ProcessWindowStyle.Minimized; // need this or else you see the window pop up - // - // Start the process. - // - using (Process process = Process.Start(start)) { - // - // Push the file contents to the new process - // - StreamWriter myStreamWriter = process.StandardInput; - myStreamWriter.WriteLine(req.Text); - myStreamWriter.Close(); - // - // Read in all the text from the process with the StreamReader. - // - using (StreamReader reader = process.StandardOutput) { - //string result = reader.ReadToEnd(); - //Console.Write(result); - - for (string line = reader.ReadLine(); line != null; line = reader.ReadLine()) { - // the lines of interest have the form "filename(line,col): some_error_label: error_message" - // where "some_error_label" is "Error" or "syntax error" or "Error BP5003" or "Related location" - if (line.Equals("")) continue; - if (line.StartsWith("Dafny program verifier finished with")) - { - if (line.Contains("time out")) - { - AddErrorBecauseOfToolProblems(req, "Verification timed out."); - } - else - { - if (!line.Contains("inconclusive") && !line.Contains("out of memory")) - { - if (line.Contains(" 0 errors")) - AddMessage(req, "Verification successful."); - } - else - { - AddErrorBecauseOfToolProblems(req, "Internal verification fault."); - } - } - break; - } - string message; - int n = line.IndexOf("): ", 2); // we start at 2, to avoid problems with "C:\..." - if (n == -1) { - continue; - } else { - int m = line.IndexOf(": ", n + 3); - if (m == -1) { - continue; - } - message = line.Substring(m + 2); - } - line = line.Substring(0, n); // line now has the form "filename(line,col" - - n = line.LastIndexOf(','); - if (n == -1) { continue; } - var colString = line.Substring(n + 1); - line = line.Substring(0, n); // line now has the form "filename(line" - - n = line.LastIndexOf('('); - if (n == -1) { continue; } - var lineString = line.Substring(n + 1); - - try { - TextSpan span = new TextSpan(); - span.iStartLine = span.iEndLine = Int32.Parse(lineString) - 1; - span.iStartIndex = Int32.Parse(colString) - 1; - span.iEndIndex = span.iStartIndex + 5; // hack - req.Sink.AddError(req.FileName, message, span, Severity.Error); - } catch (System.FormatException) { - continue; - } catch (System.OverflowException) { - continue; - } - } - } - } - } - } - - break; - - case ParseReason.DisplayMemberList: - // Parse the line specified in req.Line for the two - // tokens just before req.Col to obtain the identifier - // and the member connector symbol. - // Examine existing parse tree for members of the identifer - // and return a list of members in your version of the - // Declarations class as stored in the AuthoringScope - // object. - break; - - case ParseReason.MethodTip: - // Parse the line specified in req.Line for the token - // just before req.Col to obtain the name of the method - // being entered. - // Examine the existing parse tree for all method signatures - // with the same name and return a list of those signatures - // in your version of the Methods class as stored in the - // AuthoringScope object. - break; - - case ParseReason.HighlightBraces: - case ParseReason.MemberSelectAndHighlightBraces: - if (source.Braces != null) - { - foreach (TextSpan[] brace in source.Braces) - { - if (brace.Length == 2) - req.Sink.MatchPair(brace[0], brace[1], 1); - else if (brace.Length >= 3) - req.Sink.MatchTriple(brace[0], brace[1], brace[2], 1); - } - } - break; - } - - return new AuthoringScope(source.ParseResult); - } - - private static void AddErrorBecauseOfToolProblems(ParseRequest req, string msg) - { - TextSpan span = new TextSpan(); - span.iStartLine = span.iEndLine = 0; - span.iStartIndex = 0; - span.iEndIndex = 0; - req.Sink.AddError(req.FileName, msg, span, Severity.Error); - } - private static void AddMessage(ParseRequest req, string msg) - { - TextSpan span = new TextSpan(); - span.iStartLine = span.iEndLine = 0; - span.iStartIndex = 0; - span.iEndIndex = 1; - req.Sink.AddError(req.FileName, msg, span, Severity.Hint); - } - - /// - /// Called to determine if the given location can have a breakpoint applied to it. - /// - /// The IVsTextBuffer object containing the source file. - /// The line number where the breakpoint is to be set. - /// The offset into the line where the breakpoint is to be set. - /// - /// Returns the TextSpan giving the extent of the code affected by the breakpoint if the - /// breakpoint can be set. - /// - /// - /// If successful, returns S_OK; otherwise returns S_FALSE if there is no code at the given - /// position or returns an error code (the validation is deferred until the debug engine is loaded). - /// - /// - /// - /// CAUTION: Even if you do not intend to support the ValidateBreakpointLocation but your language - /// does support breakpoints, you must override the ValidateBreakpointLocation method and return a - /// span that contains the specified line and column; otherwise, breakpoints cannot be set anywhere - /// except line 1. You can return E_NOTIMPL to indicate that you do not otherwise support this - /// method but the span must always be set. The example shows how this can be done. - /// - /// - /// Since the language service parses the code, it generally knows what is considered code and what - /// is not. Normally, the debug engine is loaded and the pending breakpoints are bound to the source. It is at this time the breakpoint location is validated. This method is a fast way to determine if a breakpoint can be set at a particular location without loading the debug engine. - /// - /// - /// You can implement this method to call the ParseSource method with the parse reason of CodeSpan. - /// The parser examines the specified location and returns a span identifying the code at that - /// location. If there is code at the location, the span identifying that code should be passed to - /// your implementation of the CodeSpan method in your version of the AuthoringSink class. Then your - /// implementation of the ValidateBreakpointLocation method retrieves that span from your version of - /// the AuthoringSink class and returns that span in the pCodeSpan argument. - /// - /// - /// The base method returns E_NOTIMPL. - /// - /// - public override int ValidateBreakpointLocation(IVsTextBuffer buffer, int line, int col, TextSpan[] pCodeSpan) - { - // TODO: Add code to not allow breakpoints to be placed on non-code lines. - // TODO: Refactor to allow breakpoint locations to span multiple lines. - if (pCodeSpan != null) - { - pCodeSpan[0].iStartLine = line; - pCodeSpan[0].iStartIndex = col; - pCodeSpan[0].iEndLine = line; - pCodeSpan[0].iEndIndex = col; - if (buffer != null) - { - int length; - buffer.GetLengthOfLine(line, out length); - pCodeSpan[0].iStartIndex = 0; - pCodeSpan[0].iEndIndex = length; - } - return VSConstants.S_OK; - } - else - { - return VSConstants.S_FALSE; - } - } - - public override ViewFilter CreateViewFilter(CodeWindowManager mgr, IVsTextView newView) - { - return new IronyViewFilter(mgr, newView); - } - - public override string Name - { - get { return Configuration.Name; } - } - - public override string GetFormatFilterList() - { - return Configuration.FormatList; - } - } -} diff --git a/Util/VS2010/Dafny/DafnyLanguageService/Integration/IronyViewFilter.cs b/Util/VS2010/Dafny/DafnyLanguageService/Integration/IronyViewFilter.cs deleted file mode 100644 index 55c3509e..00000000 --- a/Util/VS2010/Dafny/DafnyLanguageService/Integration/IronyViewFilter.cs +++ /dev/null @@ -1,42 +0,0 @@ -using System; -using System.Collections.Generic; -using System.Linq; -using System.Text; -using Microsoft.VisualStudio.Package; -using Microsoft.VisualStudio.TextManager.Interop; - -using VsCommands2K = Microsoft.VisualStudio.VSConstants.VSStd2KCmdID; - -namespace Demo -{ - public class IronyViewFilter : ViewFilter - { - public IronyViewFilter(CodeWindowManager mgr, IVsTextView view) - : base(mgr, view) - { - - } - - public override void HandlePostExec(ref Guid guidCmdGroup, uint nCmdId, uint nCmdexecopt, IntPtr pvaIn, IntPtr pvaOut, bool bufferWasChanged) - { - if (guidCmdGroup == typeof(VsCommands2K).GUID) - { - VsCommands2K cmd = (VsCommands2K)nCmdId; - switch (cmd) - { - case VsCommands2K.UP: - case VsCommands2K.UP_EXT: - case VsCommands2K.UP_EXT_COL: - case VsCommands2K.DOWN: - case VsCommands2K.DOWN_EXT: - case VsCommands2K.DOWN_EXT_COL: - Source.OnCommand(TextView, cmd, '\0'); - return; - } - } - - - base.HandlePostExec(ref guidCmdGroup, nCmdId, nCmdexecopt, pvaIn, pvaOut, bufferWasChanged); - } - } -} diff --git a/Util/VS2010/Dafny/DafnyLanguageService/Integration/LineScanner.cs b/Util/VS2010/Dafny/DafnyLanguageService/Integration/LineScanner.cs deleted file mode 100644 index 966e9c43..00000000 --- a/Util/VS2010/Dafny/DafnyLanguageService/Integration/LineScanner.cs +++ /dev/null @@ -1,58 +0,0 @@ -using System; -using Microsoft.VisualStudio.Package; -using Irony.Parsing; - -namespace Demo -{ - public class LineScanner : IScanner - { - private Parser parser; - - public LineScanner(Grammar grammar) - { - this.parser = new Parser(grammar); - this.parser.Context.Mode = ParseMode.VsLineScan; - } - - public bool ScanTokenAndProvideInfoAboutIt(TokenInfo tokenInfo, ref int state) - { - // Reads each token in a source line and performs syntax coloring. It will continue to - // be called for the source until false is returned. - Token token = parser.Scanner.VsReadToken(ref state); - - // !EOL and !EOF - if (token != null && token.Terminal != Grammar.CurrentGrammar.Eof && token.Category != TokenCategory.Error) - { - tokenInfo.StartIndex = token.Location.Position; - tokenInfo.EndIndex = tokenInfo.StartIndex + token.Length - 1; - if (token.EditorInfo != null) { - tokenInfo.Color = (Microsoft.VisualStudio.Package.TokenColor)token.EditorInfo.Color; - tokenInfo.Type = (Microsoft.VisualStudio.Package.TokenType)token.EditorInfo.Type; - } - - if (token.KeyTerm != null && token.KeyTerm.EditorInfo != null) - { - tokenInfo.Trigger = - (Microsoft.VisualStudio.Package.TokenTriggers)token.KeyTerm.EditorInfo.Triggers; - } - else - { - if (token.EditorInfo != null) { - tokenInfo.Trigger = - (Microsoft.VisualStudio.Package.TokenTriggers)token.EditorInfo.Triggers; - } - } - - return true; - } - - return false; - } - - public void SetSource(string source, int offset) - { - // Stores line of source to be used by ScanTokenAndProvideInfoAboutIt. - parser.Scanner.VsSetSource(source, offset); - } - } -} diff --git a/Util/VS2010/Dafny/DafnyLanguageService/Integration/Method.cs b/Util/VS2010/Dafny/DafnyLanguageService/Integration/Method.cs deleted file mode 100644 index c5071612..00000000 --- a/Util/VS2010/Dafny/DafnyLanguageService/Integration/Method.cs +++ /dev/null @@ -1,20 +0,0 @@ -using System; -using System.Collections.Generic; - -namespace Demo -{ - public struct Method - { - public string Name; - public string Description; - public string Type; - public IList Parameters; - } - - public struct Parameter - { - public string Name; - public string Display; - public string Description; - } -} \ No newline at end of file diff --git a/Util/VS2010/Dafny/DafnyLanguageService/Integration/Methods.cs b/Util/VS2010/Dafny/DafnyLanguageService/Integration/Methods.cs deleted file mode 100644 index 1d7c124f..00000000 --- a/Util/VS2010/Dafny/DafnyLanguageService/Integration/Methods.cs +++ /dev/null @@ -1,50 +0,0 @@ -using System; -using System.Collections.Generic; -using System.Text; -using Microsoft.VisualStudio.TextManager.Interop; -using Microsoft.VisualStudio.Package; - -namespace Demo -{ - public class Methods : Microsoft.VisualStudio.Package.Methods - { - IList methods; - public Methods(IList methods) - { - this.methods = methods; - } - - public override int GetCount() - { - return methods.Count; - } - - public override string GetName(int index) - { - return methods[index].Name; - } - - public override string GetDescription(int index) - { - return methods[index].Description; - } - - public override string GetType(int index) - { - return methods[index].Type; - } - - public override int GetParameterCount(int index) - { - return (methods[index].Parameters == null) ? 0 : methods[index].Parameters.Count; - } - - public override void GetParameterInfo(int index, int paramIndex, out string name, out string display, out string description) - { - Parameter parameter = methods[index].Parameters[paramIndex]; - name = parameter.Name; - display = parameter.Display; - description = parameter.Description; - } - } -} \ No newline at end of file diff --git a/Util/VS2010/Dafny/DafnyLanguageService/Integration/Package.cs b/Util/VS2010/Dafny/DafnyLanguageService/Integration/Package.cs deleted file mode 100644 index dc1244d6..00000000 --- a/Util/VS2010/Dafny/DafnyLanguageService/Integration/Package.cs +++ /dev/null @@ -1,130 +0,0 @@ -using System; -using System.Collections.Generic; -using System.Text; -using System.Runtime.InteropServices; -using Microsoft.VisualStudio.OLE.Interop; -using MPF = Microsoft.VisualStudio.Package; -using System.ComponentModel.Design; - -namespace Demo -{ - public class IronyPackage : Microsoft.VisualStudio.Shell.Package, IOleComponent - { - uint componentID = 0; - public IronyPackage() - { - ServiceCreatorCallback callback = new ServiceCreatorCallback( - delegate(IServiceContainer container, Type serviceType) - { - if (typeof(IronyLanguageService) == serviceType) - { - IronyLanguageService language = new IronyLanguageService(); - language.SetSite(this); - - // register for idle time callbacks - IOleComponentManager mgr = GetService(typeof(SOleComponentManager)) as IOleComponentManager; - if (componentID == 0 && mgr != null) - { - OLECRINFO[] crinfo = new OLECRINFO[1]; - crinfo[0].cbSize = (uint)Marshal.SizeOf(typeof(OLECRINFO)); - crinfo[0].grfcrf = (uint)_OLECRF.olecrfNeedIdleTime | - (uint)_OLECRF.olecrfNeedPeriodicIdleTime; - crinfo[0].grfcadvf = (uint)_OLECADVF.olecadvfModal | - (uint)_OLECADVF.olecadvfRedrawOff | - (uint)_OLECADVF.olecadvfWarningsOff; - crinfo[0].uIdleTimeInterval = 300; - int hr = mgr.FRegisterComponent(this, crinfo, out componentID); - } - - return language; - } - else - { - return null; - } - }); - - // proffer the LanguageService - (this as IServiceContainer).AddService(typeof(IronyLanguageService), callback, true); - } - - protected override void Dispose(bool disposing) - { - try - { - if (componentID != 0) - { - IOleComponentManager mgr = GetService(typeof(SOleComponentManager)) as IOleComponentManager; - if (mgr != null) - { - mgr.FRevokeComponent(componentID); - } - componentID = 0; - } - } - finally - { - base.Dispose(disposing); - } - } - - #region IOleComponent Members - public int FContinueMessageLoop(uint uReason, IntPtr pvLoopData, MSG[] pMsgPeeked) - { - return 1; - } - - public int FDoIdle(uint grfidlef) - { - IronyLanguageService ls = GetService(typeof(IronyLanguageService)) as IronyLanguageService; - - if (ls != null) - { - ls.OnIdle((grfidlef & (uint)_OLEIDLEF.oleidlefPeriodic) != 0); - } - - return 0; - } - - public int FPreTranslateMessage(MSG[] pMsg) - { - return 0; - } - - public int FQueryTerminate(int fPromptUser) - { - return 1; - } - - public int FReserved1(uint dwReserved, uint message, IntPtr wParam, IntPtr lParam) - { - return 1; - } - - public IntPtr HwndGetWindow(uint dwWhich, uint dwReserved) - { - return IntPtr.Zero; - } - - public void OnActivationChange(IOleComponent pic, int fSameComponent, OLECRINFO[] pcrinfo, int fHostIsActivating, OLECHOSTINFO[] pchostinfo, uint dwReserved) - { - } - - public void OnAppActivate(int fActive, uint dwOtherThreadID) - { - } - - public void OnEnterState(uint uStateID, int fEnter) - { - } - - public void OnLoseActivation() - { - } - - public void Terminate() - { - } - #endregion - } -} \ No newline at end of file diff --git a/Util/VS2010/Dafny/DafnyLanguageService/Integration/Resolver.cs b/Util/VS2010/Dafny/DafnyLanguageService/Integration/Resolver.cs deleted file mode 100644 index 9f6ddeba..00000000 --- a/Util/VS2010/Dafny/DafnyLanguageService/Integration/Resolver.cs +++ /dev/null @@ -1,50 +0,0 @@ -using System; -using System.Collections.Generic; -using System.Text; -using Irony.Parsing; - -namespace Demo -{ - public class Resolver : Demo.IASTResolver - { - #region IASTResolver Members - - - public IList FindCompletions(object result, int line, int col) - { - // Used for intellisense. - List declarations = new List(); - - // Add keywords defined by grammar - foreach (KeyTerm key in Configuration.Grammar.KeyTerms.Values) - { - if(key.OptionIsSet(TermOptions.IsKeyword)) - { - declarations.Add(new Declaration("", key.Name, 206, key.Name)); - } - } - - declarations.Sort(); - return declarations; - } - - public IList FindMembers(object result, int line, int col) - { - List members = new List(); - - return members; - } - - public string FindQuickInfo(object result, int line, int col) - { - return "unknown"; - } - - public IList FindMethods(object result, int line, int col, string name) - { - return new List(); - } - - #endregion - } -} diff --git a/Util/VS2010/Dafny/DafnyLanguageService/Integration/Source.cs b/Util/VS2010/Dafny/DafnyLanguageService/Integration/Source.cs deleted file mode 100644 index 418bec01..00000000 --- a/Util/VS2010/Dafny/DafnyLanguageService/Integration/Source.cs +++ /dev/null @@ -1,41 +0,0 @@ -/*************************************************************************** - -Copyright (c) Microsoft Corporation. All rights reserved. -This code is licensed under the Visual Studio SDK license terms. -THIS CODE IS PROVIDED *AS IS* WITHOUT WARRANTY OF -ANY KIND, EITHER EXPRESS OR IMPLIED, INCLUDING ANY -IMPLIED WARRANTIES OF FITNESS FOR A PARTICULAR -PURPOSE, MERCHANTABILITY, OR NON-INFRINGEMENT. - -***************************************************************************/ - -using System; -using System.Collections.Generic; -using System.Text; -using Microsoft.VisualStudio.TextManager.Interop; -using Microsoft.VisualStudio.Package; - -namespace Demo -{ - public class Source : Microsoft.VisualStudio.Package.Source - { - public Source(LanguageService service, IVsTextLines textLines, Colorizer colorizer) - : base(service, textLines, colorizer) - { - } - - private object parseResult; - public object ParseResult - { - get { return parseResult; } - set { parseResult = value; } - } - - private IList braces; - public IList Braces - { - get { return braces; } - set { braces = value; } - } - } -} \ No newline at end of file diff --git a/Util/VS2010/Dafny/DafnyLanguageService/IronyLanguageServicePackage.cs b/Util/VS2010/Dafny/DafnyLanguageService/IronyLanguageServicePackage.cs deleted file mode 100644 index 29371f91..00000000 --- a/Util/VS2010/Dafny/DafnyLanguageService/IronyLanguageServicePackage.cs +++ /dev/null @@ -1,90 +0,0 @@ -// VsPkg.cs : Implementation of IronyLanguageService -// - -using System; -using System.Diagnostics; -using System.Globalization; -using System.Runtime.InteropServices; -using System.ComponentModel.Design; -using Microsoft.Win32; -using Microsoft.VisualStudio.Shell.Interop; -using Microsoft.VisualStudio.OLE.Interop; -using Microsoft.VisualStudio.Shell; - -namespace Demo -{ - /// - /// This is the class that implements the package exposed by this assembly. - /// - /// The minimum requirement for a class to be considered a valid package for Visual Studio - /// is to implement the IVsPackage interface and register itself with the shell. - /// This package uses the helper classes defined inside the Managed Package Framework (MPF) - /// to do it: it derives from the Package class that provides the implementation of the - /// IVsPackage interface and uses the registration attributes defined in the framework to - /// register itself and its components with the shell. - /// - // This attribute tells the registration utility (regpkg.exe) that this class needs - // to be registered as package. - [PackageRegistration(UseManagedResourcesOnly = true)] - // A Visual Studio component can be registered under different regitry roots; for instance - // when you debug your package you want to register it in the experimental hive. This - // attribute specifies the registry root to use if no one is provided to regpkg.exe with - // the /root switch. - [DefaultRegistryRoot("Software\\Microsoft\\VisualStudio\\10.0Exp")] - // This attribute is used to register the informations needed to show the this package - // in the Help/About dialog of Visual Studio. - [InstalledProductRegistration(/*false,*/ "#110", "#112", "1.0", IconResourceID = 400)] - // This attribute will make your language service accessible by other packages installed. - [ProvideService(typeof(IronyLanguageService))] - // This attribute(s) associates file extensions with your language service. - [ProvideLanguageExtension(typeof(IronyLanguageService), ".dfy")] - - // This attributes informs Visual Studio that this package provides a langauge service and - // which features are implemented. - [ProvideLanguageService(typeof(IronyLanguageService), Configuration.Name, 0, - CodeSense = true, - EnableCommenting = true, - MatchBraces = true, - MatchBracesAtCaret = true, - ShowMatchingBrace = true, - AutoOutlining = true)] - // In order be loaded inside Visual Studio in a machine that has not the VS SDK installed, - // package needs to have a valid load key (it can be requested at - // http://msdn.microsoft.com/vstudio/extend/). This attributes tells the shell that this - // package has a load key embedded in its resources. - [ProvideLoadKey("Standard", "1.0", "Dafny", "Demo", 104)] - [Guid(GuidList.guidIronyLanguageServicePkgString)] - public sealed class DafnyLanguageService : IronyPackage - { - /// - /// Default constructor of the package. - /// Inside this method you can place any initialization code that does not require - /// any Visual Studio service because at this point the package object is created but - /// not sited yet inside Visual Studio environment. The place to do all the other - /// initialization is the Initialize method. - /// - public DafnyLanguageService() - { - Trace.WriteLine(string.Format(CultureInfo.CurrentCulture, "Entering constructor for: {0}", this.ToString())); - } - - - - ///////////////////////////////////////////////////////////////////////////// - // Overriden Package Implementation - #region Package Members - - /// - /// Initialization of the package; this method is called right after the package is sited, so this is the place - /// where you can put all the initilaization code that rely on services provided by VisualStudio. - /// - protected override void Initialize() - { - Trace.WriteLine(string.Format(CultureInfo.CurrentCulture, "Entering Initialize() of: {0}", this.ToString())); - base.Initialize(); - - } - #endregion - - } -} diff --git a/Util/VS2010/Dafny/DafnyLanguageService/Key.snk b/Util/VS2010/Dafny/DafnyLanguageService/Key.snk deleted file mode 100644 index f80a4ceb..00000000 Binary files a/Util/VS2010/Dafny/DafnyLanguageService/Key.snk and /dev/null differ diff --git a/Util/VS2010/Dafny/DafnyLanguageService/Properties/AssemblyInfo.cs b/Util/VS2010/Dafny/DafnyLanguageService/Properties/AssemblyInfo.cs deleted file mode 100644 index 118d4488..00000000 --- a/Util/VS2010/Dafny/DafnyLanguageService/Properties/AssemblyInfo.cs +++ /dev/null @@ -1,36 +0,0 @@ -using System; -using System.Reflection; -using System.Resources; -using System.Runtime.CompilerServices; -using System.Runtime.InteropServices; - -// General Information about an assembly is controlled through the following -// set of attributes. Change these attribute values to modify the information -// associated with an assembly. -[assembly: AssemblyTitle("Package Name")] -[assembly: AssemblyDescription("")] -[assembly: AssemblyConfiguration("")] -[assembly: AssemblyCompany("Company")] -[assembly: AssemblyProduct("Package Name")] -[assembly: AssemblyCopyright("")] -[assembly: AssemblyTrademark("")] -[assembly: AssemblyCulture("")] -[assembly: ComVisible(false)] -[assembly: CLSCompliant(false)] -[assembly: NeutralResourcesLanguage("en-US")] - -// Version information for an assembly consists of the following four values: -// -// Major Version -// Minor Version -// Build Number -// Revision -// -// You can specify all the values or you can default the Revision and Build Numbers -// by using the '*' as shown below: - -[assembly: AssemblyVersion("1.0.0.0")] -[assembly: AssemblyFileVersion("1.0.0.0")] - - - diff --git a/Util/VS2010/Dafny/DafnyLanguageService/Resources.Designer.cs b/Util/VS2010/Dafny/DafnyLanguageService/Resources.Designer.cs deleted file mode 100644 index 0ca81303..00000000 --- a/Util/VS2010/Dafny/DafnyLanguageService/Resources.Designer.cs +++ /dev/null @@ -1,63 +0,0 @@ -//------------------------------------------------------------------------------ -// -// This code was generated by a tool. -// Runtime Version:4.0.21006.1 -// -// Changes to this file may cause incorrect behavior and will be lost if -// the code is regenerated. -// -//------------------------------------------------------------------------------ - -namespace Demo { - using System; - - - /// - /// A strongly-typed resource class, for looking up localized strings, etc. - /// - // This class was auto-generated by the StronglyTypedResourceBuilder - // class via a tool like ResGen or Visual Studio. - // To add or remove a member, edit your .ResX file then rerun ResGen - // with the /str option, or rebuild your VS project. - [global::System.CodeDom.Compiler.GeneratedCodeAttribute("System.Resources.Tools.StronglyTypedResourceBuilder", "4.0.0.0")] - [global::System.Diagnostics.DebuggerNonUserCodeAttribute()] - [global::System.Runtime.CompilerServices.CompilerGeneratedAttribute()] - internal class Resources { - - private static global::System.Resources.ResourceManager resourceMan; - - private static global::System.Globalization.CultureInfo resourceCulture; - - [global::System.Diagnostics.CodeAnalysis.SuppressMessageAttribute("Microsoft.Performance", "CA1811:AvoidUncalledPrivateCode")] - internal Resources() { - } - - /// - /// Returns the cached ResourceManager instance used by this class. - /// - [global::System.ComponentModel.EditorBrowsableAttribute(global::System.ComponentModel.EditorBrowsableState.Advanced)] - internal static global::System.Resources.ResourceManager ResourceManager { - get { - if (object.ReferenceEquals(resourceMan, null)) { - global::System.Resources.ResourceManager temp = new global::System.Resources.ResourceManager("Demo.DafnyLanguageService.Resources", typeof(Resources).Assembly); - resourceMan = temp; - } - return resourceMan; - } - } - - /// - /// Overrides the current thread's CurrentUICulture property for all - /// resource lookups using this strongly typed resource class. - /// - [global::System.ComponentModel.EditorBrowsableAttribute(global::System.ComponentModel.EditorBrowsableState.Advanced)] - internal static global::System.Globalization.CultureInfo Culture { - get { - return resourceCulture; - } - set { - resourceCulture = value; - } - } - } -} diff --git a/Util/VS2010/Dafny/DafnyLanguageService/Resources.resx b/Util/VS2010/Dafny/DafnyLanguageService/Resources.resx deleted file mode 100644 index 03fef612..00000000 --- a/Util/VS2010/Dafny/DafnyLanguageService/Resources.resx +++ /dev/null @@ -1,130 +0,0 @@ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - text/microsoft-resx - - - 2.0 - - - System.Resources.ResXResourceReader, System.Windows.Forms, Version=2.0.0.0, Culture=neutral, PublicKeyToken=b77a5c561934e089 - - - System.Resources.ResXResourceWriter, System.Windows.Forms, Version=2.0.0.0, Culture=neutral, PublicKeyToken=b77a5c561934e089 - - - \ No newline at end of file diff --git a/Util/VS2010/Dafny/DafnyLanguageService/Resources/Irony.dll b/Util/VS2010/Dafny/DafnyLanguageService/Resources/Irony.dll deleted file mode 100644 index e2021a72..00000000 Binary files a/Util/VS2010/Dafny/DafnyLanguageService/Resources/Irony.dll and /dev/null differ diff --git a/Util/VS2010/Dafny/DafnyLanguageService/VSPackage.resx b/Util/VS2010/Dafny/DafnyLanguageService/VSPackage.resx deleted file mode 100644 index 68782536..00000000 --- a/Util/VS2010/Dafny/DafnyLanguageService/VSPackage.resx +++ /dev/null @@ -1,129 +0,0 @@ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - text/microsoft-resx - - - 2.0 - - - System.Resources.ResXResourceReader, System.Windows.Forms, Version=2.0.0.0, Culture=neutral, PublicKeyToken=b77a5c561934e089 - - - System.Resources.ResXResourceWriter, System.Windows.Forms, Version=2.0.0.0, Culture=neutral, PublicKeyToken=b77a5c561934e089 - - - Paste PLK Here - - - Dafny - - - Dafny Programming Language - - \ No newline at end of file diff --git a/Util/VS2010/Dafny/DafnyLanguageService/source.extension.vsixmanifest b/Util/VS2010/Dafny/DafnyLanguageService/source.extension.vsixmanifest deleted file mode 100644 index 58e160cd..00000000 --- a/Util/VS2010/Dafny/DafnyLanguageService/source.extension.vsixmanifest +++ /dev/null @@ -1,27 +0,0 @@ - - - - - DafnyService - Microsoft Research - 1.0 - Information about my package - 1033 - - - - Pro - VST_All - - - - - - - - - - DafnyService.pkgdef - - - diff --git a/Util/VS2010/Dafny/StartDafny.bat b/Util/VS2010/Dafny/StartDafny.bat deleted file mode 100644 index 71dc149a..00000000 --- a/Util/VS2010/Dafny/StartDafny.bat +++ /dev/null @@ -1,10 +0,0 @@ -@echo off -echo ---------- Starting ------------ < nul >> c:\tmp\doo.out -time < nul >> c:\tmp\doo.out -echo. < nul >> c:\tmp\doo.out - -"c:\boogie\Binaries\Dafny.exe" -nologo stdin.dfy -compile:0 -timeLimit:10 %* 2>> c:\tmp\doo.out - -time < nul >> c:\tmp\doo.out -echo. < nul >> c:\tmp\doo.out -echo ---------- Done ------------ < nul >> c:\tmp\doo.out diff --git a/Util/VS2010/DafnyExtension/DafnyExtension.sln b/Util/VS2010/DafnyExtension/DafnyExtension.sln deleted file mode 100644 index fd450cc8..00000000 --- a/Util/VS2010/DafnyExtension/DafnyExtension.sln +++ /dev/null @@ -1,20 +0,0 @@ - -Microsoft Visual Studio Solution File, Format Version 12.00 -# Visual Studio 2012 -Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "DafnyExtension", "DafnyExtension\DafnyExtension.csproj", "{6E9A5E14-0763-471C-A129-80A879D9E7BA}" -EndProject -Global - GlobalSection(SolutionConfigurationPlatforms) = preSolution - Debug|Any CPU = Debug|Any CPU - Release|Any CPU = Release|Any CPU - EndGlobalSection - GlobalSection(ProjectConfigurationPlatforms) = postSolution - {6E9A5E14-0763-471C-A129-80A879D9E7BA}.Debug|Any CPU.ActiveCfg = Debug|Any CPU - {6E9A5E14-0763-471C-A129-80A879D9E7BA}.Debug|Any CPU.Build.0 = Debug|Any CPU - {6E9A5E14-0763-471C-A129-80A879D9E7BA}.Release|Any CPU.ActiveCfg = Release|Any CPU - {6E9A5E14-0763-471C-A129-80A879D9E7BA}.Release|Any CPU.Build.0 = Release|Any CPU - EndGlobalSection - GlobalSection(SolutionProperties) = preSolution - HideSolutionNode = FALSE - EndGlobalSection -EndGlobal diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/BraceMatching.cs b/Util/VS2010/DafnyExtension/DafnyExtension/BraceMatching.cs deleted file mode 100644 index 44b1affe..00000000 --- a/Util/VS2010/DafnyExtension/DafnyExtension/BraceMatching.cs +++ /dev/null @@ -1,253 +0,0 @@ -using System; -using System.Linq; -using System.Collections.Generic; -using System.ComponentModel.Composition; -using Microsoft.VisualStudio.Text; -using Microsoft.VisualStudio.Text.Editor; -using Microsoft.VisualStudio.Text.Tagging; -using Microsoft.VisualStudio.Utilities; - -namespace DafnyLanguage -{ - [Export(typeof(IViewTaggerProvider))] - [ContentType("dafny")] - [TagType(typeof(TextMarkerTag))] - internal class BraceMatchingTaggerProvider : IViewTaggerProvider - { - [Import] - internal IBufferTagAggregatorFactoryService AggregatorFactory = null; - - public ITagger CreateTagger(ITextView textView, ITextBuffer buffer) where T : ITag { - if (textView == null) - return null; - - //provide highlighting only on the top-level buffer - if (textView.TextBuffer != buffer) - return null; - - ITagAggregator tagAggregator = AggregatorFactory.CreateTagAggregator(buffer); - return new BraceMatchingTagger(textView, buffer, tagAggregator) as ITagger; - } - } - - internal abstract class TokenBasedTagger - { - ITagAggregator _aggregator; - - internal TokenBasedTagger(ITagAggregator tagAggregator) { - _aggregator = tagAggregator; - } - - public bool InsideComment(SnapshotPoint pt) { - SnapshotSpan span = new SnapshotSpan(pt, 1); - foreach (var tagSpan in this._aggregator.GetTags(span)) { - switch (tagSpan.Tag.Kind) { - case DafnyTokenKinds.Comment: - case DafnyTokenKinds.String: - foreach (var s in tagSpan.Span.GetSpans(pt.Snapshot)) { - if (s.Contains(span)) - return true; - } - break; - default: - break; - } - } - return false; - } - } - - internal class BraceMatchingTagger : TokenBasedTagger, ITagger - { - ITextView View { get; set; } - ITextBuffer SourceBuffer { get; set; } - SnapshotPoint? CurrentChar { get; set; } - private char[] openBraces; - private char[] closeBraces; - - static TextMarkerTag Blue = new TextMarkerTag("blue"); - - internal BraceMatchingTagger(ITextView view, ITextBuffer sourceBuffer, ITagAggregator tagAggregator) - : base(tagAggregator) - { - //here the keys are the open braces, and the values are the close braces - openBraces = new char[] { '(', '{', '[' }; - closeBraces = new char[] { ')', '}', ']' }; - this.View = view; - this.SourceBuffer = sourceBuffer; - this.CurrentChar = null; - - this.View.Caret.PositionChanged += CaretPositionChanged; - this.View.LayoutChanged += ViewLayoutChanged; - } - - public event EventHandler TagsChanged; - - void ViewLayoutChanged(object sender, TextViewLayoutChangedEventArgs e) { - if (e.NewSnapshot != e.OldSnapshot) //make sure that there has really been a change - { - UpdateAtCaretPosition(View.Caret.Position); - } - } - - void CaretPositionChanged(object sender, CaretPositionChangedEventArgs e) { - UpdateAtCaretPosition(e.NewPosition); - } - - void UpdateAtCaretPosition(CaretPosition caretPosition) { - CurrentChar = caretPosition.Point.GetPoint(SourceBuffer, caretPosition.Affinity); - - if (!CurrentChar.HasValue) - return; - - var chngd = TagsChanged; - if (chngd != null) - chngd(this, new SnapshotSpanEventArgs(new SnapshotSpan(SourceBuffer.CurrentSnapshot, 0, SourceBuffer.CurrentSnapshot.Length))); - } - - public IEnumerable> GetTags(NormalizedSnapshotSpanCollection spans) { - if (spans.Count == 0) //there is no content in the buffer - yield break; - - //don't do anything if the current SnapshotPoint is not initialized - if (!CurrentChar.HasValue) - yield break; - - //hold on to a snapshot of the current character - SnapshotPoint currentChar = CurrentChar.Value; - - //if the requested snapshot isn't the same as the one the brace is on, translate our spans to the expected snapshot - if (spans[0].Snapshot != currentChar.Snapshot) { - currentChar = currentChar.TranslateTo(spans[0].Snapshot, PointTrackingMode.Positive); - } - - if (currentChar.Position < spans[0].Snapshot.Length) { - // Check if the current character is an open brace - char ch = currentChar.GetChar(); - char closeCh; - if (MatchBrace(currentChar, ch, true, out closeCh)) { - SnapshotSpan pairSpan; - if (FindMatchingCloseChar(currentChar, ch, closeCh, View.TextViewLines.Count, out pairSpan)) { - yield return new TagSpan(new SnapshotSpan(currentChar, 1), Blue); - yield return new TagSpan(pairSpan, Blue); - } - } - } - - if (0 < currentChar.Position) { - // Check if the previous character is a close brace (note, caret may be between a close brace and an open brace, in which case we'll tag two pairs) - SnapshotPoint prevChar = currentChar - 1; - char ch = prevChar.GetChar(); - char openCh; - if (MatchBrace(prevChar, ch, false, out openCh)) { - SnapshotSpan pairSpan; - if (FindMatchingOpenChar(prevChar, openCh, ch, View.TextViewLines.Count, out pairSpan)) { - yield return new TagSpan(new SnapshotSpan(prevChar, 1), Blue); - yield return new TagSpan(pairSpan, Blue); - } - } - } - } - - private bool MatchBrace(SnapshotPoint pt, char query, bool sourceIsOpen, out char match) { - if (!InsideComment(pt)) { - char[] source = sourceIsOpen ? openBraces : closeBraces; - int i = 0; - foreach (char ch in source) { - if (ch == query) { - char[] dest = sourceIsOpen ? closeBraces : openBraces; - match = dest[i]; - return true; - } - i++; - } - } - match = query; // satisfy compiler - return false; - } - - private bool FindMatchingCloseChar(SnapshotPoint startPoint, char open, char close, int linesViewed, out SnapshotSpan pairSpan) { - ITextSnapshotLine line = startPoint.GetContainingLine(); - int lineNumber = line.LineNumber; - int offset = startPoint.Position - line.Start.Position + 1; - - int lineNumberLimit = Math.Min(startPoint.Snapshot.LineCount, lineNumber + linesViewed); - - int openCount = 0; - while (true) { - string lineText = line.GetText(); - - //walk the entire line - for (; offset < line.Length; offset++) { - char currentChar = lineText[offset]; - if (currentChar == open || currentChar == close) { - if (!InsideComment(new SnapshotPoint(line.Snapshot, line.Start.Position + offset))) { - if (currentChar == open) { - openCount++; - } else if (0 < openCount) { - openCount--; - } else { - //found the matching close - pairSpan = new SnapshotSpan(startPoint.Snapshot, line.Start + offset, 1); - return true; - } - } - } - } - - //move on to the next line - lineNumber++; - if (lineNumberLimit <= lineNumber) - break; - - line = line.Snapshot.GetLineFromLineNumber(lineNumber); - offset = 0; - } - - pairSpan = new SnapshotSpan(startPoint, startPoint); // satisfy the compiler - return false; - } - - private bool FindMatchingOpenChar(SnapshotPoint startPoint, char open, char close, int linesViewed, out SnapshotSpan pairSpan) { - ITextSnapshotLine line = startPoint.GetContainingLine(); - int lineNumber = line.LineNumber; - int offset = startPoint.Position - line.Start.Position - 1; //move the offset to the character before this one - - int lineNumberLimit = Math.Max(0, lineNumber - linesViewed); - - int closeCount = 0; - while (true) { - string lineText = line.GetText(); - - //walk the entire line - for (; 0 <= offset; offset--) { - char currentChar = lineText[offset]; - if (currentChar == open || currentChar == close) { - if (!InsideComment(new SnapshotPoint(line.Snapshot, line.Start.Position + offset))) { - if (currentChar == close) { - closeCount++; - } else if (0 < closeCount) { - closeCount--; - } else { - // We've found the open character - pairSpan = new SnapshotSpan(line.Start + offset, 1); //we just want the character itself - return true; - } - } - } - } - - // Move to the previous line - lineNumber--; - if (lineNumber < lineNumberLimit) - break; - - line = line.Snapshot.GetLineFromLineNumber(lineNumber); - offset = line.Length - 1; - } - - pairSpan = new SnapshotSpan(startPoint, startPoint); // satisfy the compiler - return false; - } - } -} diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/BufferIdleEventUtil.cs b/Util/VS2010/DafnyExtension/DafnyExtension/BufferIdleEventUtil.cs deleted file mode 100644 index 1aea1385..00000000 --- a/Util/VS2010/DafnyExtension/DafnyExtension/BufferIdleEventUtil.cs +++ /dev/null @@ -1,155 +0,0 @@ -//*************************************************************************** -// Copyright © 2010 Microsoft Corporation. All Rights Reserved. -// This code released under the terms of the -// Microsoft Public License (MS-PL, http://opensource.org/licenses/ms-pl.html.) -//*************************************************************************** -using System; -using System.Collections.Generic; -using System.Linq; -using System.Text; -using Microsoft.VisualStudio.Text; -using System.Windows.Threading; - -namespace DafnyLanguage -{ - /// - /// Handy reusable utility to listen for change events on the associated buffer, but - /// only pass these along to a set of listeners when the user stops typing for a half second - /// - static class BufferIdleEventUtil - { - static object bufferListenersKey = new object(); - static object bufferTimerKey = new object(); - - #region Public interface - - public static bool AddBufferIdleEventListener(ITextBuffer buffer, EventHandler handler) - { - HashSet listenersForBuffer; - if (!TryGetBufferListeners(buffer, out listenersForBuffer)) - listenersForBuffer = ConnectToBuffer(buffer); - - if (listenersForBuffer.Contains(handler)) - return false; - - listenersForBuffer.Add(handler); - - return true; - } - - public static bool RemoveBufferIdleEventListener(ITextBuffer buffer, EventHandler handler) - { - HashSet listenersForBuffer; - if (!TryGetBufferListeners(buffer, out listenersForBuffer)) - return false; - - if (!listenersForBuffer.Contains(handler)) - return false; - - listenersForBuffer.Remove(handler); - - if (listenersForBuffer.Count == 0) - DisconnectFromBuffer(buffer); - - return true; - } - - #endregion - - #region Helpers - - static bool TryGetBufferListeners(ITextBuffer buffer, out HashSet listeners) - { - return buffer.Properties.TryGetProperty(bufferListenersKey, out listeners); - } - - static void ClearBufferListeners(ITextBuffer buffer) - { - buffer.Properties.RemoveProperty(bufferListenersKey); - } - - static bool TryGetBufferTimer(ITextBuffer buffer, out DispatcherTimer timer) - { - return buffer.Properties.TryGetProperty(bufferTimerKey, out timer); - } - - static void ClearBufferTimer(ITextBuffer buffer) - { - DispatcherTimer timer; - if (TryGetBufferTimer(buffer, out timer)) - { - if (timer != null) - timer.Stop(); - buffer.Properties.RemoveProperty(bufferTimerKey); - } - } - - static void DisconnectFromBuffer(ITextBuffer buffer) - { - buffer.Changed -= BufferChanged; - - ClearBufferListeners(buffer); - ClearBufferTimer(buffer); - - buffer.Properties.RemoveProperty(bufferListenersKey); - } - - static HashSet ConnectToBuffer(ITextBuffer buffer) - { - buffer.Changed += BufferChanged; - - RestartTimerForBuffer(buffer); - - HashSet listenersForBuffer = new HashSet(); - buffer.Properties[bufferListenersKey] = listenersForBuffer; - - return listenersForBuffer; - } - - static void RestartTimerForBuffer(ITextBuffer buffer) - { - DispatcherTimer timer; - - if (TryGetBufferTimer(buffer, out timer)) - { - timer.Stop(); - } - else - { - timer = new DispatcherTimer(DispatcherPriority.ApplicationIdle) - { - Interval = TimeSpan.FromMilliseconds(500) - }; - - timer.Tick += (s, e) => - { - ClearBufferTimer(buffer); - - HashSet handlers; - if (TryGetBufferListeners(buffer, out handlers)) - { - foreach (var handler in handlers) - { - handler(buffer, new EventArgs()); - } - } - }; - - buffer.Properties[bufferTimerKey] = timer; - } - - timer.Start(); - } - - static void BufferChanged(object sender, TextContentChangedEventArgs e) - { - ITextBuffer buffer = sender as ITextBuffer; - if (buffer == null) - return; - - RestartTimerForBuffer(buffer); - } - - #endregion - } -} diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/ClassificationTagger.cs b/Util/VS2010/DafnyExtension/DafnyExtension/ClassificationTagger.cs deleted file mode 100644 index 09835ac9..00000000 --- a/Util/VS2010/DafnyExtension/DafnyExtension/ClassificationTagger.cs +++ /dev/null @@ -1,107 +0,0 @@ -using System; -using System.Collections.Generic; -using System.ComponentModel.Composition; -using System.Windows.Media; -using Microsoft.VisualStudio.Text; -using Microsoft.VisualStudio.Text.Classification; -using Microsoft.VisualStudio.Text.Editor; -using Microsoft.VisualStudio.Text.Tagging; -using Microsoft.VisualStudio.Utilities; - - -namespace DafnyLanguage -{ - [Export(typeof(ITaggerProvider))] - [ContentType("dafny")] - [TagType(typeof(ClassificationTag))] - internal sealed class DafnyClassifierProvider : ITaggerProvider - { - [Import] - internal IBufferTagAggregatorFactoryService AggregatorFactory = null; - - [Import] - internal IClassificationTypeRegistryService ClassificationTypeRegistry = null; - - [Import] - internal Microsoft.VisualStudio.Language.StandardClassification.IStandardClassificationService Standards = null; - - public ITagger CreateTagger(ITextBuffer buffer) where T : ITag { - ITagAggregator tagAggregator = AggregatorFactory.CreateTagAggregator(buffer); - return new DafnyClassifier(buffer, tagAggregator, ClassificationTypeRegistry, Standards) as ITagger; - } - } - - internal sealed class DafnyClassifier : ITagger - { - ITextBuffer _buffer; - ITagAggregator _aggregator; - IDictionary _typeMap; - - internal DafnyClassifier(ITextBuffer buffer, - ITagAggregator tagAggregator, - IClassificationTypeRegistryService typeService, Microsoft.VisualStudio.Language.StandardClassification.IStandardClassificationService standards) { - _buffer = buffer; - _aggregator = tagAggregator; - _aggregator.TagsChanged += new EventHandler(_aggregator_TagsChanged); - // use built-in classification types: - _typeMap = new Dictionary(); - _typeMap[DafnyTokenKinds.Keyword] = standards.Keyword; - _typeMap[DafnyTokenKinds.Number] = standards.NumberLiteral; - _typeMap[DafnyTokenKinds.String] = standards.StringLiteral; - _typeMap[DafnyTokenKinds.Comment] = standards.Comment; - _typeMap[DafnyTokenKinds.VariableIdentifier] = standards.Identifier; - _typeMap[DafnyTokenKinds.VariableIdentifierDefinition] = typeService.GetClassificationType("Dafny identifier"); - } - - public event EventHandler TagsChanged; - - public IEnumerable> GetTags(NormalizedSnapshotSpanCollection spans) { - if (spans.Count == 0) yield break; - var snapshot = spans[0].Snapshot; - foreach (var tagSpan in this._aggregator.GetTags(spans)) { - IClassificationType t = _typeMap[tagSpan.Tag.Kind]; - foreach (SnapshotSpan s in tagSpan.Span.GetSpans(snapshot)) { - yield return new TagSpan(s, new ClassificationTag(t)); - } - } - } - - void _aggregator_TagsChanged(object sender, TagsChangedEventArgs e) { - var chng = TagsChanged; - if (chng != null) { - NormalizedSnapshotSpanCollection spans = e.Span.GetSpans(_buffer.CurrentSnapshot); - if (spans.Count > 0) { - SnapshotSpan span = new SnapshotSpan(spans[0].Start, spans[spans.Count - 1].End); - chng(this, new SnapshotSpanEventArgs(span)); - } - } - } - } - - /// - /// Defines an editor format for user-defined type. - /// - [Export(typeof(EditorFormatDefinition))] - [ClassificationType(ClassificationTypeNames = "Dafny identifier")] - [Name("Dafny identifier")] - [UserVisible(true)] - //set the priority to be after the default classifiers - [Order(Before = Priority.Default)] - internal sealed class DafnyTypeFormat : ClassificationFormatDefinition - { - public DafnyTypeFormat() { - this.DisplayName = "Dafny identifier"; //human readable version of the name - this.ForegroundColor = Colors.CornflowerBlue; - } - } - - internal static class ClassificationDefinition - { - /// - /// Defines the "ordinary" classification type. - /// - [Export(typeof(ClassificationTypeDefinition))] - [Name("Dafny identifier")] - internal static ClassificationTypeDefinition UserType = null; - } -} diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/ContentType.cs b/Util/VS2010/DafnyExtension/DafnyExtension/ContentType.cs deleted file mode 100644 index d8487f74..00000000 --- a/Util/VS2010/DafnyExtension/DafnyExtension/ContentType.cs +++ /dev/null @@ -1,18 +0,0 @@ -using System.ComponentModel.Composition; -using Microsoft.VisualStudio.Utilities; - -namespace DafnyLanguage -{ - class DafnyContentType - { - [Export] - [Name("dafny")] - [BaseDefinition("code")] - internal static ContentTypeDefinition ContentType = null; - - [Export] - [FileExtension(".dfy")] - [ContentType("dafny")] - internal static FileExtensionToContentTypeDefinition FileType = null; - } -} diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/DafnyDriver.cs b/Util/VS2010/DafnyExtension/DafnyExtension/DafnyDriver.cs deleted file mode 100644 index 39829bb0..00000000 --- a/Util/VS2010/DafnyExtension/DafnyExtension/DafnyDriver.cs +++ /dev/null @@ -1,419 +0,0 @@ -using System; -using System.Collections.Generic; -using System.Linq; -using System.Text; -using System.IO; -using System.Diagnostics; -using System.Diagnostics.Contracts; -// Here come the Dafny/Boogie specific imports -//using PureCollections; -using Bpl = Microsoft.Boogie; -using Dafny = Microsoft.Dafny; -using Microsoft.Boogie.AbstractInterpretation; -using VC; -// using AI = Microsoft.AbstractInterpretationFramework; - - -namespace DafnyLanguage -{ - class DafnyDriver - { - readonly string _programText; - readonly string _filename; - Dafny.Program _program; - List _errors = new List(); - public List Errors { get { return _errors; } } - - public DafnyDriver(string programText, string filename) { - _programText = programText; - _filename = filename; - } - - void RecordError(int line, int col, ErrorCategory cat, string msg) { - _errors.Add(new DafnyError(line, col, cat, msg)); - } - - static DafnyDriver() { - Initialize(); - } - - static void Initialize() { - if (Dafny.DafnyOptions.O == null) { - var options = new Dafny.DafnyOptions(); - options.ProverKillTime = 10; - options.ErrorTrace = 0; - Dafny.DafnyOptions.Install(options); - options.ApplyDefaultOptions(); - } - } - - public Dafny.Program ProcessResolution() { - if (!ParseAndTypeCheck()) { - return null; - } - return _program; - } - - bool ParseAndTypeCheck() { - Dafny.ModuleDecl module = new Dafny.LiteralModuleDecl(new Dafny.DefaultModuleDecl(), null); - Dafny.BuiltIns builtIns = new Dafny.BuiltIns(); - int errorCount = Dafny.Parser.Parse(_programText, _filename, module, builtIns, new VSErrors(this)); - if (errorCount != 0) - return false; - Dafny.Program program = new Dafny.Program(_filename, module, builtIns); - - Dafny.Resolver r = new VSResolver(program, this); - r.ResolveProgram(program); - if (r.ErrorCount != 0) - return false; - - _program = program; - return true; // success - } - - class VSErrors : Dafny.Errors - { - DafnyDriver dd; - public VSErrors(DafnyDriver dd) { - this.dd = dd; - } - public override void SynErr(string filename, int line, int col, string msg) { - dd.RecordError(line - 1, col - 1, ErrorCategory.ParseError, msg); - count++; - } - public override void SemErr(string filename, int line, int col, string msg) { - dd.RecordError(line - 1, col - 1, ErrorCategory.ResolveError, msg); - count++; - } - public override void Warning(string filename, int line, int col, string msg) { - dd.RecordError(line - 1, col - 1, ErrorCategory.ParseWarning, msg); - } - } - - class VSResolver : Dafny.Resolver - { - DafnyDriver dd; - public VSResolver(Dafny.Program program, DafnyDriver dd) - : base(program) { - this.dd = dd; - } - public override void Error(Bpl.IToken tok, string msg, params object[] args) { - string s = string.Format(msg, args); - dd.RecordError(tok.line - 1, tok.col - 1, ErrorCategory.ResolveError, s); - ErrorCount++; - } - } - - public static bool Verify(Dafny.Program dafnyProgram, ErrorReporterDelegate er) { - Dafny.Translator translator = new Dafny.Translator(); - Bpl.Program boogieProgram = translator.Translate(dafnyProgram); - - PipelineOutcome oc = BoogiePipeline(boogieProgram, er); - switch (oc) { - case PipelineOutcome.Done: - case PipelineOutcome.VerificationCompleted: - // TODO: This would be the place to proceed to compile the program, if desired - return true; - case PipelineOutcome.FatalError: - default: - return false; - } - } - - enum PipelineOutcome { Done, ResolutionError, TypeCheckingError, ResolvedAndTypeChecked, FatalError, VerificationCompleted } - - /// - /// Resolve, type check, infer invariants for, and verify the given Boogie program. - /// The intention is that this Boogie program has been produced by translation from something - /// else. Hence, any resolution errors and type checking errors are due to errors in - /// the translation. - /// - static PipelineOutcome BoogiePipeline(Bpl.Program/*!*/ program, ErrorReporterDelegate er) { - Contract.Requires(program != null); - - PipelineOutcome oc = BoogieResolveAndTypecheck(program); - if (oc == PipelineOutcome.ResolvedAndTypeChecked) { - EliminateDeadVariablesAndInline(program); - return BoogieInferAndVerify(program, er); - } - return oc; - } - - static void EliminateDeadVariablesAndInline(Bpl.Program program) { - Contract.Requires(program != null); - // Eliminate dead variables - Microsoft.Boogie.UnusedVarEliminator.Eliminate(program); - - // Collect mod sets - if (Bpl.CommandLineOptions.Clo.DoModSetAnalysis) { - Microsoft.Boogie.ModSetCollector.DoModSetAnalysis(program); - } - - // Coalesce blocks - if (Bpl.CommandLineOptions.Clo.CoalesceBlocks) { - Microsoft.Boogie.BlockCoalescer.CoalesceBlocks(program); - } - - // Inline - var TopLevelDeclarations = program.TopLevelDeclarations; - - if (Bpl.CommandLineOptions.Clo.ProcedureInlining != Bpl.CommandLineOptions.Inlining.None) { - bool inline = false; - foreach (var d in TopLevelDeclarations) { - if (d.FindExprAttribute("inline") != null) { - inline = true; - } - } - if (inline && Bpl.CommandLineOptions.Clo.StratifiedInlining == 0) { - foreach (var d in TopLevelDeclarations) { - var impl = d as Bpl.Implementation; - if (impl != null) { - impl.OriginalBlocks = impl.Blocks; - impl.OriginalLocVars = impl.LocVars; - } - } - foreach (var d in TopLevelDeclarations) { - var impl = d as Bpl.Implementation; - if (impl != null && !impl.SkipVerification) { - Bpl.Inliner.ProcessImplementation(program, impl); - } - } - foreach (var d in TopLevelDeclarations) { - var impl = d as Bpl.Implementation; - if (impl != null) { - impl.OriginalBlocks = null; - impl.OriginalLocVars = null; - } - } - } - } - } - - /// - /// Resolves and type checks the given Boogie program. - /// Returns: - /// - Done if no errors occurred, and command line specified no resolution or no type checking. - /// - ResolutionError if a resolution error occurred - /// - TypeCheckingError if a type checking error occurred - /// - ResolvedAndTypeChecked if both resolution and type checking succeeded - /// - static PipelineOutcome BoogieResolveAndTypecheck(Bpl.Program program) { - Contract.Requires(program != null); - // ---------- Resolve ------------------------------------------------------------ - int errorCount = program.Resolve(); - if (errorCount != 0) { - return PipelineOutcome.ResolutionError; - } - - // ---------- Type check ------------------------------------------------------------ - errorCount = program.Typecheck(); - if (errorCount != 0) { - return PipelineOutcome.TypeCheckingError; - } - - return PipelineOutcome.ResolvedAndTypeChecked; - } - - /// - /// Given a resolved and type checked Boogie program, infers invariants for the program - /// and then attempts to verify it. Returns: - /// - Done if command line specified no verification - /// - FatalError if a fatal error occurred - /// - VerificationCompleted if inference and verification completed, in which the out - /// parameters contain meaningful values - /// - static PipelineOutcome BoogieInferAndVerify(Bpl.Program program, ErrorReporterDelegate er) { - Contract.Requires(program != null); - - // ---------- Infer invariants -------------------------------------------------------- - - // Abstract interpretation -> Always use (at least) intervals, if not specified otherwise (e.g. with the "/noinfer" switch) - if (Bpl.CommandLineOptions.Clo.UseAbstractInterpretation) { - if (Bpl.CommandLineOptions.Clo.Ai.J_Intervals || Bpl.CommandLineOptions.Clo.Ai.J_Trivial) { - Microsoft.Boogie.AbstractInterpretation.NativeAbstractInterpretation.RunAbstractInterpretation(program); - } else { - // use /infer:j as the default - Bpl.CommandLineOptions.Clo.Ai.J_Intervals = true; - Microsoft.Boogie.AbstractInterpretation.NativeAbstractInterpretation.RunAbstractInterpretation(program); - } - } - - if (Bpl.CommandLineOptions.Clo.LoopUnrollCount != -1) { - program.UnrollLoops(Bpl.CommandLineOptions.Clo.LoopUnrollCount); - } - - if (Bpl.CommandLineOptions.Clo.ExpandLambdas) { - Bpl.LambdaHelper.ExpandLambdas(program); - //PrintBplFile ("-", program, true); - } - - // ---------- Verify ------------------------------------------------------------ - - if (!Bpl.CommandLineOptions.Clo.Verify) { return PipelineOutcome.Done; } - - #region Verify each implementation - - ConditionGeneration vcgen = null; - try { - vcgen = new VCGen(program, Bpl.CommandLineOptions.Clo.SimplifyLogFilePath, Bpl.CommandLineOptions.Clo.SimplifyLogFileAppend); - } catch (Bpl.ProverException) { - return PipelineOutcome.FatalError; - } - - var decls = program.TopLevelDeclarations.ToArray(); - foreach (var decl in decls) { - Contract.Assert(decl != null); - Bpl.Implementation impl = decl as Bpl.Implementation; - if (impl != null && Bpl.CommandLineOptions.Clo.UserWantsToCheckRoutine(impl.Name) && !impl.SkipVerification) { - List/*?*/ errors; - - ConditionGeneration.Outcome outcome; - int prevAssertionCount = vcgen.CumulativeAssertionCount; - try { - outcome = vcgen.VerifyImplementation(impl, out errors); - } catch (VCGenException) { - errors = null; - outcome = VCGen.Outcome.Inconclusive; - } catch (Bpl.UnexpectedProverOutputException) { - errors = null; - outcome = VCGen.Outcome.Inconclusive; - } - - switch (outcome) { - default: - Contract.Assert(false); throw new Exception(); // unexpected outcome - case VCGen.Outcome.Correct: - break; - case VCGen.Outcome.TimedOut: - er(new DafnyErrorInformation(impl.tok, "Verification timed out (" + impl.Name + ")")); - break; - case VCGen.Outcome.OutOfMemory: - er(new DafnyErrorInformation(impl.tok, "Verification out of memory (" + impl.Name + ")")); - break; - case VCGen.Outcome.Inconclusive: - er(new DafnyErrorInformation(impl.tok, "Verification inconclusive (" + impl.Name + ")")); - break; - case VCGen.Outcome.Errors: - Contract.Assert(errors != null); // guaranteed by postcondition of VerifyImplementation - - errors.Sort(new Bpl.CounterexampleComparer()); - foreach (var error in errors) { - DafnyErrorInformation errorInfo; - - if (error is Bpl.CallCounterexample) { - var err = (Bpl.CallCounterexample)error; - errorInfo = new DafnyErrorInformation(err.FailingCall.tok, err.FailingCall.ErrorData as string ?? "A precondition for this call might not hold."); - errorInfo.AddAuxInfo(err.FailingRequires.tok, err.FailingRequires.ErrorData as string ?? "Related location: This is the precondition that might not hold."); - - } else if (error is Bpl.ReturnCounterexample) { - var err = (Bpl.ReturnCounterexample)error; - errorInfo = new DafnyErrorInformation(err.FailingReturn.tok, "A postcondition might not hold on this return path."); - errorInfo.AddAuxInfo(err.FailingEnsures.tok, err.FailingEnsures.ErrorData as string ?? "Related location: This is the postcondition that might not hold."); - errorInfo.AddAuxInfo(err.FailingEnsures.Attributes); - - } else { // error is AssertCounterexample - var err = (Bpl.AssertCounterexample)error; - if (err.FailingAssert is Bpl.LoopInitAssertCmd) { - errorInfo = new DafnyErrorInformation(err.FailingAssert.tok, "This loop invariant might not hold on entry."); - } else if (err.FailingAssert is Bpl.LoopInvMaintainedAssertCmd) { - // this assertion is a loop invariant which is not maintained - errorInfo = new DafnyErrorInformation(err.FailingAssert.tok, "This loop invariant might not be maintained by the loop."); - } else { - string msg = err.FailingAssert.ErrorData as string; - if (msg == null) { - msg = "This assertion might not hold."; - } - errorInfo = new DafnyErrorInformation(err.FailingAssert.tok, msg); - errorInfo.AddAuxInfo(err.FailingAssert.Attributes); - } - } - if (Bpl.CommandLineOptions.Clo.ErrorTrace > 0) { - foreach (Bpl.Block b in error.Trace) { - // for ErrorTrace == 1 restrict the output; - // do not print tokens with -17:-4 as their location because they have been - // introduced in the translation and do not give any useful feedback to the user - if (!(Bpl.CommandLineOptions.Clo.ErrorTrace == 1 && b.tok.line == -17 && b.tok.col == -4) && - b.tok.line != 0 && b.tok.col != 0) { - errorInfo.AddAuxInfo(b.tok, "Execution trace: " + b.Label); - } - } - } - // if (Bpl.CommandLineOptions.Clo.ModelViewFile != null) { - // error.PrintModel(); - // } - er(errorInfo); - } - break; - } - } - } - vcgen.Close(); - Bpl.CommandLineOptions.Clo.TheProverFactory.Close(); - - #endregion - - return PipelineOutcome.VerificationCompleted; - } - - public delegate void ErrorReporterDelegate(DafnyErrorInformation errInfo); - - public class DafnyErrorInformation - { - public readonly Bpl.IToken Tok; - public readonly string Msg; - public readonly List Aux = new List(); - - public class DafnyErrorAuxInfo - { - public readonly Bpl.IToken Tok; - public readonly string Msg; - public DafnyErrorAuxInfo(Bpl.IToken tok, string msg) { - Tok = tok; - Msg = CleanUp(msg); - } - } - - public DafnyErrorInformation(Bpl.IToken tok, string msg) { - Contract.Requires(tok != null); - Contract.Requires(1 <= tok.line && 1 <= tok.col); - Contract.Requires(msg != null); - Tok = tok; - Msg = CleanUp(msg); - AddNestingsAsAux(tok); - } - public void AddAuxInfo(Bpl.IToken tok, string msg) { - Contract.Requires(tok != null); - Contract.Requires(1 <= tok.line && 1 <= tok.col); - Contract.Requires(msg != null); - Aux.Add(new DafnyErrorAuxInfo(tok, msg)); - AddNestingsAsAux(tok); - } - void AddNestingsAsAux(Bpl.IToken tok) { - while (tok is Dafny.NestedToken) { - var nt = (Dafny.NestedToken)tok; - tok = nt.Inner; - Aux.Add(new DafnyErrorAuxInfo(tok, "Related location")); - } - } - public void AddAuxInfo(Bpl.QKeyValue attr) { - while (attr != null) { - if (attr.Key == "msg" && attr.Params.Count == 1 && attr.tok.line != 0 && attr.tok.col != 0) { - var str = attr.Params[0] as string; - if (str != null) { - AddAuxInfo(attr.tok, str); - } - } - attr = attr.Next; - } - } - - public static string CleanUp(string msg) { - if (msg.ToLower().StartsWith("error: ")) { - return msg.Substring(7); - } else { - return msg; - } - } - } - } -} diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/DafnyExtension.csproj b/Util/VS2010/DafnyExtension/DafnyExtension/DafnyExtension.csproj deleted file mode 100644 index 2580c396..00000000 --- a/Util/VS2010/DafnyExtension/DafnyExtension/DafnyExtension.csproj +++ /dev/null @@ -1,191 +0,0 @@ - - - - - Debug - AnyCPU - 10.0.20305 - 2.0 - {82b43b9b-a64c-4715-b499-d71e9ca2bd60};{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC} - {6E9A5E14-0763-471C-A129-80A879D9E7BA} - Library - Properties - DafnyLanguage - DafnyLanguageService - v4.0 - 512 - false - 11.0 - - - - - 4.0 - - - true - full - false - bin\Debug\ - DEBUG;TRACE - prompt - 4 - - - pdbonly - true - bin\Release\ - TRACE - prompt - 4 - - - - False - ..\..\..\..\Binaries\AbsInt.dll - - - False - ..\..\..\..\Binaries\AIFramework.dll - - - False - ..\..\..\..\Binaries\Basetypes.dll - - - False - ..\..\..\..\Binaries\CodeContractsExtender.dll - - - False - ..\..\..\..\Binaries\Core.dll - - - False - ..\..\..\..\Binaries\DafnyPipeline.dll - - - ..\..\..\..\Binaries\Graph.dll - - - ..\..\..\..\Binaries\Houdini.dll - - - ..\..\..\..\Binaries\Model.dll - - - ..\..\..\..\Binaries\ParserHelper.dll - - - ..\..\..\..\Binaries\Provers.Z3.dll - - - ..\..\..\..\Binaries\Provers.SMTLib.dll - - - ..\..\..\..\Binaries\VCExpr.dll - - - False - ..\..\..\..\Binaries\VCGeneration.dll - - - False - - - False - - - - - - - False - - - - - True - - - - False - - - False - - - False - - - False - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - true - Always - - - Designer - - - true - Always - - - - - - - 10.0 - $(MSBuildExtensionsPath32)\Microsoft\VisualStudio\v$(VisualStudioVersion) - - - - - - cd - - - - - copy ..\..\..\..\..\..\Binaries\DafnyPrelude.bpl $(ProjectDir) -copy ..\..\..\..\..\..\Binaries\UnivBackPred2.smt2 $(ProjectDir) - - - \ No newline at end of file diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/ErrorTagger.cs b/Util/VS2010/DafnyExtension/DafnyExtension/ErrorTagger.cs deleted file mode 100644 index efd755d8..00000000 --- a/Util/VS2010/DafnyExtension/DafnyExtension/ErrorTagger.cs +++ /dev/null @@ -1,85 +0,0 @@ -//*************************************************************************** -// Copyright © 2010 Microsoft Corporation. All Rights Reserved. -// This code released under the terms of the -// Microsoft Public License (MS-PL, http://opensource.org/licenses/ms-pl.html.) -//*************************************************************************** -using EnvDTE; -using System; -using System.Collections.Generic; -using System.Linq; -using System.Text; -using System.ComponentModel.Composition; -using System.Windows.Threading; -using Microsoft.VisualStudio.Shell; -using Microsoft.VisualStudio.Shell.Interop; -using Microsoft.VisualStudio.Text; -using Microsoft.VisualStudio.Text.Classification; -using Microsoft.VisualStudio.Text.Editor; -using Microsoft.VisualStudio.Text.Tagging; -using Microsoft.VisualStudio.Text.Projection; -using Microsoft.VisualStudio.Utilities; - -namespace DafnyLanguage -{ - [Export(typeof(ITaggerProvider))] - [ContentType("dafny")] - [TagType(typeof(ErrorTag))] - internal sealed class ErrorTaggerProvider : ITaggerProvider - { - [Import] - internal IBufferTagAggregatorFactoryService AggregatorFactory = null; - - public ITagger CreateTagger(ITextBuffer buffer) where T : ITag { - ITagAggregator tagAggregator = AggregatorFactory.CreateTagAggregator(buffer); - // create a single tagger for each buffer. - Func> sc = delegate() { return new ErrorTagger(buffer, tagAggregator) as ITagger; }; - return buffer.Properties.GetOrCreateSingletonProperty>(sc); - } - } - - /// - /// Translate PkgDefTokenTags into ErrorTags and Error List items - /// - internal sealed class ErrorTagger : ITagger - { - ITextBuffer _buffer; - ITagAggregator _aggregator; - - internal ErrorTagger(ITextBuffer buffer, ITagAggregator tagAggregator) { - _buffer = buffer; - _aggregator = tagAggregator; - _aggregator.TagsChanged += new EventHandler(_aggregator_TagsChanged); - } - - /// - /// Find the Error tokens in the set of all tokens and create an ErrorTag for each - /// - public IEnumerable> GetTags(NormalizedSnapshotSpanCollection spans) { - if (spans.Count == 0) yield break; - var snapshot = spans[0].Snapshot; - foreach (var tagSpan in this._aggregator.GetTags(spans)) { - DafnyResolverTag t = tagSpan.Tag; - DafnyErrorResolverTag et = t as DafnyErrorResolverTag; - if (et != null) { - foreach (SnapshotSpan s in tagSpan.Span.GetSpans(snapshot)) { - yield return new TagSpan(s, new ErrorTag(et.Typ, et.Msg)); - } - } - } - } - - // the Classifier tagger is translating buffer change events into TagsChanged events, so we don't have to - public event EventHandler TagsChanged; - - void _aggregator_TagsChanged(object sender, TagsChangedEventArgs e) { - var chng = TagsChanged; - if (chng != null) { - NormalizedSnapshotSpanCollection spans = e.Span.GetSpans(_buffer.CurrentSnapshot); - if (spans.Count > 0) { - SnapshotSpan span = new SnapshotSpan(spans[0].Start, spans[spans.Count - 1].End); - chng(this, new SnapshotSpanEventArgs(span)); - } - } - } - } -} diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/HoverText.cs b/Util/VS2010/DafnyExtension/DafnyExtension/HoverText.cs deleted file mode 100644 index be806f5b..00000000 --- a/Util/VS2010/DafnyExtension/DafnyExtension/HoverText.cs +++ /dev/null @@ -1,126 +0,0 @@ -using System; -using System.Collections.Generic; -using System.Linq; -using System.Text; -using System.Windows.Input; -using Microsoft.VisualStudio.Language.Intellisense; -using System.Collections.ObjectModel; -using Microsoft.VisualStudio.Text; -using Microsoft.VisualStudio.Text.Editor; -using Microsoft.VisualStudio.Text.Tagging; -using System.ComponentModel.Composition; -using Microsoft.VisualStudio.Utilities; -using System.Diagnostics.Contracts; - - -namespace DafnyLanguage -{ - [Export(typeof(IQuickInfoSourceProvider))] - [ContentType("dafny")] - [Name("Dafny QuickInfo")] - class OokQuickInfoSourceProvider : IQuickInfoSourceProvider - { - [Import] - IBufferTagAggregatorFactoryService aggService = null; - - public IQuickInfoSource TryCreateQuickInfoSource(ITextBuffer textBuffer) { - return new DafnyQuickInfoSource(textBuffer, aggService.CreateTagAggregator(textBuffer)); - } - } - - class DafnyQuickInfoSource : IQuickInfoSource - { - private ITagAggregator _aggregator; - private ITextBuffer _buffer; - - public DafnyQuickInfoSource(ITextBuffer buffer, ITagAggregator aggregator) { - _aggregator = aggregator; - _buffer = buffer; - } - - public void AugmentQuickInfoSession(IQuickInfoSession session, IList quickInfoContent, out ITrackingSpan applicableToSpan) { - applicableToSpan = null; - - var triggerPoint = (SnapshotPoint)session.GetTriggerPoint(_buffer.CurrentSnapshot); - if (triggerPoint == null) - return; - - foreach (IMappingTagSpan curTag in _aggregator.GetTags(new SnapshotSpan(triggerPoint, triggerPoint))) { - var s = curTag.Tag.HoverText; - if (s != null) { - var tagSpan = curTag.Span.GetSpans(_buffer).First(); - applicableToSpan = _buffer.CurrentSnapshot.CreateTrackingSpan(tagSpan, SpanTrackingMode.EdgeExclusive); - quickInfoContent.Add(s); - } - } - } - public void Dispose() { - } - } - // --------------------------------- QuickInfo controller ------------------------------------------ - - [Export(typeof(IIntellisenseControllerProvider))] - [Name("Dafny QuickInfo controller")] - [ContentType("dafny")] - class DafnyQuickInfoControllerProvider : IIntellisenseControllerProvider - { - [Import] - internal IQuickInfoBroker QuickInfoBroker { get; set; } - - public IIntellisenseController TryCreateIntellisenseController(ITextView textView, IList subjectBuffers) { - return new DafnyQuickInfoController(textView, subjectBuffers, this); - } - } - - class DafnyQuickInfoController : IIntellisenseController - { - private ITextView _textView; - private IList _subjectBuffers; - private DafnyQuickInfoControllerProvider _componentContext; - - private IQuickInfoSession _session; - - internal DafnyQuickInfoController(ITextView textView, IList subjectBuffers, DafnyQuickInfoControllerProvider componentContext) { - _textView = textView; - _subjectBuffers = subjectBuffers; - _componentContext = componentContext; - - _textView.MouseHover += this.OnTextViewMouseHover; - } - - public void ConnectSubjectBuffer(ITextBuffer subjectBuffer) { - } - - public void DisconnectSubjectBuffer(ITextBuffer subjectBuffer) { - } - - public void Detach(ITextView textView) { - if (_textView == textView) { - _textView.MouseHover -= OnTextViewMouseHover; - _textView = null; - } - } - - void OnTextViewMouseHover(object sender, MouseHoverEventArgs e) { - SnapshotPoint? point = GetMousePosition(new SnapshotPoint(_textView.TextSnapshot, e.Position)); - - if (point != null) { - ITrackingPoint triggerPoint = point.Value.Snapshot.CreateTrackingPoint(point.Value.Position, PointTrackingMode.Positive); - - // Find the broker for this buffer - if (!_componentContext.QuickInfoBroker.IsQuickInfoActive(_textView)) { - _session = _componentContext.QuickInfoBroker.CreateQuickInfoSession(_textView, triggerPoint, true); - _session.Start(); - } - } - } - - SnapshotPoint? GetMousePosition(SnapshotPoint topPosition) { - return _textView.BufferGraph.MapDownToFirstMatch( - topPosition, - PointTrackingMode.Positive, - snapshot => _subjectBuffers.Contains(snapshot.TextBuffer), - PositionAffinity.Predecessor); - } - } -} diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/IdentifierTagger.cs b/Util/VS2010/DafnyExtension/DafnyExtension/IdentifierTagger.cs deleted file mode 100644 index 5ecc8dc2..00000000 --- a/Util/VS2010/DafnyExtension/DafnyExtension/IdentifierTagger.cs +++ /dev/null @@ -1,344 +0,0 @@ -//*************************************************************************** -// Copyright © 2010 Microsoft Corporation. All Rights Reserved. -// This code released under the terms of the -// Microsoft Public License (MS-PL, http://opensource.org/licenses/ms-pl.html.) -//*************************************************************************** -using EnvDTE; -using System; -using System.Collections.Generic; -using System.Linq; -using System.Text; -using System.ComponentModel.Composition; -using System.Windows.Threading; -using Microsoft.VisualStudio.Shell; -using Microsoft.VisualStudio.Shell.Interop; -using Microsoft.VisualStudio.Text; -using Microsoft.VisualStudio.Text.Classification; -using Microsoft.VisualStudio.Text.Editor; -using Microsoft.VisualStudio.Text.Tagging; -using Microsoft.VisualStudio.Text.Projection; -using Microsoft.VisualStudio.Utilities; -using System.Diagnostics.Contracts; -using Bpl = Microsoft.Boogie; -using Microsoft.Dafny; - -namespace DafnyLanguage -{ - [Export(typeof(ITaggerProvider))] - [ContentType("dafny")] - [TagType(typeof(DafnyTokenTag))] - internal sealed class IdentifierTaggerProvider : ITaggerProvider - { - [Import] - internal IBufferTagAggregatorFactoryService AggregatorFactory = null; - - public ITagger CreateTagger(ITextBuffer buffer) where T : ITag { - ITagAggregator tagAggregator = AggregatorFactory.CreateTagAggregator(buffer); - // create a single tagger for each buffer. - Func> sc = delegate() { return new IdentifierTagger(buffer, tagAggregator) as ITagger; }; - return buffer.Properties.GetOrCreateSingletonProperty>(sc); - } - } - - /// - /// Translate DafnyResolverTag's into IOutliningRegionTag's - /// - internal sealed class IdentifierTagger : ITagger - { - ITextBuffer _buffer; - ITextSnapshot _snapshot; // the most recent snapshot of _buffer that we have been informed about - Microsoft.Dafny.Program _program; // the program parsed from _snapshot - List _regions = new List(); // the regions generated from _program - ITagAggregator _aggregator; - - internal IdentifierTagger(ITextBuffer buffer, ITagAggregator tagAggregator) { - _buffer = buffer; - _snapshot = _buffer.CurrentSnapshot; - _aggregator = tagAggregator; - _aggregator.TagsChanged += new EventHandler(_aggregator_TagsChanged); - } - - /// - /// Find the Error tokens in the set of all tokens and create an ErrorTag for each - /// - public IEnumerable> GetTags(NormalizedSnapshotSpanCollection spans) { - if (spans.Count == 0) yield break; - // (A NormalizedSnapshotSpanCollection contains spans that all come from the same snapshot.) - // The spans are ordered by the .Start component, and the collection contains no adjacent or abutting spans. - // Hence, to find a span that includes all the ones in "spans", we only need to look at the .Start for the - // first spand and the .End of the last span: - var startPoint = spans[0].Start; - var endPoint = spans[spans.Count - 1].End; - - // Note, (startPoint,endPoint) are points in the spans for which we're being asked to provide tags. We need to translate - // these back into the most recent snapshot that we've computed regions for, namely _snapshot. - var entire = new SnapshotSpan(startPoint, endPoint).TranslateTo(_snapshot, SpanTrackingMode.EdgeExclusive); - int start = entire.Start; - int end = entire.End; - foreach (var r in _regions) { - if (0 <= r.Length && r.Start <= end && start <= r.Start + r.Length) { - DafnyTokenKinds kind; - switch (r.Kind) { - case IdRegion.OccurrenceKind.Use: - kind = DafnyTokenKinds.VariableIdentifier; break; - case IdRegion.OccurrenceKind.Definition: - kind = DafnyTokenKinds.VariableIdentifierDefinition; break; - case IdRegion.OccurrenceKind.WildDefinition: - kind = DafnyTokenKinds.Keyword; break; - default: - Contract.Assert(false); // unexpected OccurrenceKind - goto case IdRegion.OccurrenceKind.Use; // to please compiler - } - yield return new TagSpan( - new SnapshotSpan(_snapshot, r.Start, r.Length), - new DafnyTokenTag(kind, r.HoverText)); - } - } - } - - // the Classifier tagger is translating buffer change events into TagsChanged events, so we don't have to - public event EventHandler TagsChanged; - - void _aggregator_TagsChanged(object sender, TagsChangedEventArgs e) { - var r = sender as ResolverTagger; - if (r != null) { - ITextSnapshot snap; - Microsoft.Dafny.Program prog; - lock (this) { - snap = r._snapshot; - prog = r._program; - } - if (prog != null) { - if (!ComputeIdentifierRegions(prog, snap)) - return; // no new regions - - var chng = TagsChanged; - if (chng != null) { - NormalizedSnapshotSpanCollection spans = e.Span.GetSpans(_buffer.CurrentSnapshot); - if (spans.Count > 0) { - SnapshotSpan span = new SnapshotSpan(spans[0].Start, spans[spans.Count - 1].End); - chng(this, new SnapshotSpanEventArgs(span)); - } - } - } - } - } - - bool ComputeIdentifierRegions(Microsoft.Dafny.Program program, ITextSnapshot snapshot) { - Contract.Requires(snapshot != null); - - if (program == _program) - return false; // no new regions - - List newRegions = new List(); - - foreach (var module in program.Modules) { - foreach (var d in module.TopLevelDecls) { - if (d is DatatypeDecl) { - var dt = (DatatypeDecl)d; - foreach (var ctor in dt.Ctors) { - foreach (var dtor in ctor.Destructors) { - if (dtor != null) { - IdRegion.Add(newRegions, dtor.tok, dtor, null, "destructor", true, module); - } - } - } - } else if (d is ClassDecl) { - var cl = (ClassDecl)d; - foreach (var member in cl.Members) { - if (member is Function) { - var f = (Function)member; - foreach (var p in f.Formals) { - IdRegion.Add(newRegions, p.tok, p, true, module); - } - f.Req.ForEach(e => ExprRegions(e, newRegions, module)); - f.Reads.ForEach(fe => FrameExprRegions(fe, newRegions, true, module)); - f.Ens.ForEach(e => ExprRegions(e, newRegions, module)); - f.Decreases.Expressions.ForEach(e => ExprRegions(e, newRegions, module)); - if (f.Body != null) { - ExprRegions(f.Body, newRegions, module); - } - } else if (member is Method) { - var m = (Method)member; - foreach (var p in m.Ins) { - IdRegion.Add(newRegions, p.tok, p, true, module); - } - foreach (var p in m.Outs) { - IdRegion.Add(newRegions, p.tok, p, true, module); - } - m.Req.ForEach(e => ExprRegions(e.E, newRegions, module)); - m.Mod.Expressions.ForEach(fe => FrameExprRegions(fe, newRegions, true, module)); - m.Ens.ForEach(e => ExprRegions(e.E, newRegions, module)); - m.Decreases.Expressions.ForEach(e => ExprRegions(e, newRegions, module)); - if (m.Body != null) { - StatementRegions(m.Body, newRegions, module); - } - } else if (member is Field) { - var fld = (Field)member; - IdRegion.Add(newRegions, fld.tok, fld, null, "field", true, module); - } - } - } - } - } - _snapshot = snapshot; - _regions = newRegions; - _program = program; - return true; - } - - static void FrameExprRegions(FrameExpression fe, List regions, bool descendIntoExpressions, ModuleDefinition module) { - Contract.Requires(fe != null); - Contract.Requires(regions != null); - if (descendIntoExpressions) { - ExprRegions(fe.E, regions, module); - } - if (fe.Field != null) { - 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); - } - } - - static void ExprRegions(Microsoft.Dafny.Expression expr, List regions, ModuleDefinition module) { - Contract.Requires(expr != null); - Contract.Requires(regions != null); - if (expr is IdentifierExpr) { - var e = (IdentifierExpr)expr; - 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, e.Type, "field", false, module); - } else if (expr is ComprehensionExpr) { - var e = (ComprehensionExpr)expr; - foreach (var bv in e.BoundVars) { - IdRegion.Add(regions, bv.tok, bv, true, module); - } - } else if (expr is MatchExpr) { - var e = (MatchExpr)expr; - foreach (var kase in e.Cases) { - kase.Arguments.ForEach(bv => IdRegion.Add(regions, bv.tok, bv, true, module)); - } - } else if (expr is ChainingExpression) { - var e = (ChainingExpression)expr; - // Do the subexpressions only once (that is, avoid the duplication that occurs in the desugared form of the ChainingExpression) - e.Operands.ForEach(ee => ExprRegions(ee, regions, module)); - return; // return here, so as to avoid doing the subexpressions below - } - foreach (var ee in expr.SubExpressions) { - ExprRegions(ee, regions, module); - } - } - - static void StatementRegions(Statement stmt, List regions, ModuleDefinition module) { - Contract.Requires(stmt != null); - Contract.Requires(regions != null); - if (stmt is VarDeclStmt) { - var s = (VarDeclStmt)stmt; - // Add the variables here, once, and then go directly to the RHS's (without letting the sub-statements re-do the LHS's) - foreach (var lhs in s.Lhss) { - IdRegion.Add(regions, lhs.Tok, lhs, true, module); - } - if (s.Update == null) { - // the VarDeclStmt has no associated assignment - } else if (s.Update is UpdateStmt) { - var upd = (UpdateStmt)s.Update; - foreach (var rhs in upd.Rhss) { - foreach (var ee in rhs.SubExpressions) { - ExprRegions(ee, regions, module); - } - } - } else { - var upd = (AssignSuchThatStmt)s.Update; - ExprRegions(upd.Expr, regions, module); - } - // we're done, so don't do the sub-statements/expressions again - return; - } else if (stmt is VarDecl) { - var s = (VarDecl)stmt; - IdRegion.Add(regions, s.Tok, s, true, module); - } else if (stmt is ParallelStmt) { - var s = (ParallelStmt)stmt; - s.BoundVars.ForEach(bv => IdRegion.Add(regions, bv.tok, bv, true, module)); - } else if (stmt is MatchStmt) { - var s = (MatchStmt)stmt; - foreach (var kase in s.Cases) { - kase.Arguments.ForEach(bv => IdRegion.Add(regions, bv.tok, bv, true, module)); - } - } else if (stmt is LoopStmt) { - var s = (LoopStmt)stmt; - if (s.Mod.Expressions != null) { - s.Mod.Expressions.ForEach(fe => FrameExprRegions(fe, regions, false, module)); - } - } - foreach (var ee in stmt.SubExpressions) { - ExprRegions(ee, regions, module); - } - foreach (var ss in stmt.SubStatements) { - StatementRegions(ss, regions, module); - } - } - - class IdRegion - { - public readonly int Start; - public readonly int Length; - public readonly string HoverText; - public enum OccurrenceKind { Use, Definition, WildDefinition } - public readonly OccurrenceKind Kind; - - static bool SurfaceSyntaxToken(Bpl.IToken tok) { - Contract.Requires(tok != null); - return !(tok is TokenWrapper); - } - - public static void Add(List regions, Bpl.IToken tok, IVariable v, bool isDefinition, ModuleDefinition context) { - Contract.Requires(regions != null); - Contract.Requires(tok != null); - Contract.Requires(v != null); - if (SurfaceSyntaxToken(tok)) { - regions.Add(new IdRegion(tok, v, isDefinition, context)); - } - } - public static void Add(List 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, showType, kind, isDefinition, context)); - } - } - - private IdRegion(Bpl.IToken tok, IVariable v, bool isDefinition, ModuleDefinition context) { - Contract.Requires(tok != null); - Contract.Requires(v != null); - Start = tok.pos; - Length = v.DisplayName.Length; - string kind; - if (v is VarDecl) { - kind = "local variable"; - } else if (v is BoundVar) { - kind = "bound variable"; - } else { - var formal = (Formal)v; - kind = formal.InParam ? "in-parameter" : "out-parameter"; - } - 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, 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), showType.TypeName(context), decl.IsGhost ? "ghost " : "", kind); - Kind = !isDefinition ? OccurrenceKind.Use : OccurrenceKind.Definition; - } - } - } - -} diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/OutliningTagger.cs b/Util/VS2010/DafnyExtension/DafnyExtension/OutliningTagger.cs deleted file mode 100644 index a47cdba7..00000000 --- a/Util/VS2010/DafnyExtension/DafnyExtension/OutliningTagger.cs +++ /dev/null @@ -1,185 +0,0 @@ -//*************************************************************************** -// Copyright © 2010 Microsoft Corporation. All Rights Reserved. -// This code released under the terms of the -// Microsoft Public License (MS-PL, http://opensource.org/licenses/ms-pl.html.) -//*************************************************************************** -using EnvDTE; -using System; -using System.Collections.Generic; -using System.Linq; -using System.Text; -using System.ComponentModel.Composition; -using System.Windows.Threading; -using Microsoft.VisualStudio.Shell; -using Microsoft.VisualStudio.Shell.Interop; -using Microsoft.VisualStudio.Text; -using Microsoft.VisualStudio.Text.Classification; -using Microsoft.VisualStudio.Text.Editor; -using Microsoft.VisualStudio.Text.Tagging; -using Microsoft.VisualStudio.Text.Projection; -using Microsoft.VisualStudio.Utilities; -using System.Diagnostics.Contracts; -using Bpl = Microsoft.Boogie; -using Dafny = Microsoft.Dafny; - -namespace DafnyLanguage -{ - [Export(typeof(ITaggerProvider))] - [ContentType("dafny")] - [TagType(typeof(IOutliningRegionTag))] - internal sealed class OutliningTaggerProvider : ITaggerProvider - { - [Import] - internal IBufferTagAggregatorFactoryService AggregatorFactory = null; - - public ITagger CreateTagger(ITextBuffer buffer) where T : ITag { - ITagAggregator tagAggregator = AggregatorFactory.CreateTagAggregator(buffer); - // create a single tagger for each buffer. - Func> sc = delegate() { return new OutliningTagger(buffer, tagAggregator) as ITagger; }; - return buffer.Properties.GetOrCreateSingletonProperty>(sc); - } - } - - /// - /// Translate DafnyResolverTag's into IOutliningRegionTag's - /// - internal sealed class OutliningTagger : ITagger - { - ITextBuffer _buffer; - ITextSnapshot _snapshot; // the most recent snapshot of _buffer that we have been informed about - Dafny.Program _program; // the program parsed from _snapshot - List _regions = new List(); // the regions generated from _program - ITagAggregator _aggregator; - - internal OutliningTagger(ITextBuffer buffer, ITagAggregator tagAggregator) { - _buffer = buffer; - _snapshot = _buffer.CurrentSnapshot; - _aggregator = tagAggregator; - _aggregator.TagsChanged += new EventHandler(_aggregator_TagsChanged); - } - - /// - /// Find the Error tokens in the set of all tokens and create an ErrorTag for each - /// - public IEnumerable> GetTags(NormalizedSnapshotSpanCollection spans) { - if (spans.Count == 0) yield break; - // (A NormalizedSnapshotSpanCollection contains spans that all come from the same snapshot.) - // The spans are ordered by the .Start component, and the collection contains no adjacent or abutting spans. - // Hence, to find a span that includes all the ones in "spans", we only need to look at the .Start for the - // first spand and the .End of the last span: - var startPoint = spans[0].Start; - var endPoint = spans[spans.Count - 1].End; - - // Note, (startPoint,endPoint) are points in the spans for which we're being asked to provide tags. We need to translate - // these back into the most recent snapshot that we've computed regions for, namely _snapshot. - var entire = new SnapshotSpan(startPoint, endPoint).TranslateTo(_snapshot, SpanTrackingMode.EdgeExclusive); - int start = entire.Start; - int end = entire.End; - if (start == end) yield break; - - foreach (var r in _regions) { - if (0 <= r.Length && r.Start <= end && start <= r.Start + r.Length) { - yield return new TagSpan( - new SnapshotSpan(_snapshot, r.Start, r.Length), - new OutliningRegionTag(false, false, "...", r.HoverText)); - } - } - } - - // the Classifier tagger is translating buffer change events into TagsChanged events, so we don't have to - public event EventHandler TagsChanged; - - void _aggregator_TagsChanged(object sender, TagsChangedEventArgs e) { - var r = sender as ResolverTagger; - if (r != null) { - ITextSnapshot snap; - Microsoft.Dafny.Program prog; - lock (this) { - snap = r._snapshot; - prog = r._program; - } - if (prog != null) { - if (!ComputeOutliningRegions(prog, snap)) - return; // no new regions - - var chng = TagsChanged; - if (chng != null) { - NormalizedSnapshotSpanCollection spans = e.Span.GetSpans(_buffer.CurrentSnapshot); - if (spans.Count > 0) { - SnapshotSpan span = new SnapshotSpan(spans[0].Start, spans[spans.Count - 1].End); - chng(this, new SnapshotSpanEventArgs(span)); - } - } - } - } - } - - bool ComputeOutliningRegions(Dafny.Program program, ITextSnapshot snapshot) { - Contract.Requires(snapshot != null); - - if (program == _program) - return false; // no new regions - - List newRegions = new List(); - - foreach (var module in program.Modules) { - if (!module.IsDefaultModule) { - newRegions.Add(new ORegion(module, "module")); - } - foreach (Dafny.TopLevelDecl d in module.TopLevelDecls) { - if (!HasBodyTokens(d) && !(d is Dafny.ClassDecl)) { - continue; - } - if (d is Dafny.ArbitraryTypeDecl) { - newRegions.Add(new ORegion(d, "type")); - } else if (d is Dafny.CoDatatypeDecl) { - newRegions.Add(new ORegion(d, "codatatype")); - } else if (d is Dafny.DatatypeDecl) { - newRegions.Add(new ORegion(d, "datatype")); - } else if (d is Dafny.ModuleDecl) { - // do nothing here, since the outer loop handles modules - } else { - Dafny.ClassDecl cl = (Dafny.ClassDecl)d; - if (!cl.IsDefaultClass) { - newRegions.Add(new ORegion(cl, "class")); - } - // do the class members (in particular, functions and methods) - foreach (Dafny.MemberDecl m in cl.Members) { - if (!HasBodyTokens(m)) { - continue; - } - if (m is Dafny.Function && ((Dafny.Function)m).Body != null) { - newRegions.Add(new ORegion(m, m is Dafny.CoPredicate ? "copredicate" : m is Dafny.Predicate ? "predicate" : "function")); - } else if (m is Dafny.Method && ((Dafny.Method)m).Body != null) { - newRegions.Add(new ORegion(m, m is Dafny.Constructor ? "constructor" : "method")); - } - } - } - } - } - _snapshot = snapshot; - _regions = newRegions; - _program = program; - return true; - } - - bool HasBodyTokens(Dafny.Declaration decl) { - Contract.Requires(decl != null); - return decl.BodyStartTok != Bpl.Token.NoToken && decl.BodyEndTok != Bpl.Token.NoToken; - } - - class ORegion - { - public readonly int Start; - public readonly int Length; - public readonly string HoverText; - public ORegion(Dafny.Declaration decl, string kind) { - int startPosition = decl.BodyStartTok.pos + 1; // skip the open-curly brace itself - int length = decl.BodyEndTok.pos - startPosition; - Start = startPosition; - Length = length; - HoverText = string.Format("body of {0} {1}", kind, decl.Name); - } - } - } -} diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/ProgressMargin.cs b/Util/VS2010/DafnyExtension/DafnyExtension/ProgressMargin.cs deleted file mode 100644 index 7fdf38a6..00000000 --- a/Util/VS2010/DafnyExtension/DafnyExtension/ProgressMargin.cs +++ /dev/null @@ -1,260 +0,0 @@ -using System; -using System.Collections.Generic; -using System.Threading; -using System.Windows.Threading; -using System.Windows; -using System.Windows.Shapes; -using System.Windows.Media; -using System.Windows.Controls; -using System.ComponentModel.Composition; -using Microsoft.VisualStudio.Text; -using Microsoft.VisualStudio.Text.Editor; -using Microsoft.VisualStudio.Text.Formatting; -using Microsoft.VisualStudio.Text.Tagging; -using Microsoft.VisualStudio.Text.Classification; -using Microsoft.VisualStudio.Shell; -using Microsoft.VisualStudio.Utilities; -using System.Diagnostics.Contracts; -using Dafny = Microsoft.Dafny; -using Bpl = Microsoft.Boogie; - - -namespace DafnyLanguage -{ - #region UI stuff - internal class ProgressMarginGlyphFactory : IGlyphFactory - { - public UIElement GenerateGlyph(IWpfTextViewLine line, IGlyphTag tag) { - var dtag = tag as ProgressGlyphTag; - if (dtag == null) { - return null; - } - - System.Windows.Shapes.Rectangle sh = new Rectangle() { - Fill = dtag.Val == 0 ? Brushes.Violet : Brushes.DarkOrange, - Height = 18.0, - Width = 3.0 - }; - return sh; - } - } - - [Export(typeof(IGlyphFactoryProvider))] - [Name("ProgressMarginGlyph")] - [Order(After = "TokenTagger")] - [ContentType("dafny")] - [TagType(typeof(ProgressGlyphTag))] - internal sealed class ProgressMarginGlyphFactoryProvider : IGlyphFactoryProvider - { - public IGlyphFactory GetGlyphFactory(IWpfTextView view, IWpfTextViewMargin margin) { - return new ProgressMarginGlyphFactory(); - } - } - - internal class ProgressGlyphTag : IGlyphTag - { - public readonly int Val; - public ProgressGlyphTag(int val) { - Val = val; - } - } - #endregion - - [Export(typeof(ITaggerProvider))] - [ContentType("dafny")] - [TagType(typeof(ProgressGlyphTag))] - class ProgressTaggerProvider : ITaggerProvider - { - [Import] - internal IBufferTagAggregatorFactoryService AggregatorFactory = null; - - [Import(typeof(Microsoft.VisualStudio.Shell.SVsServiceProvider))] - internal IServiceProvider _serviceProvider = null; - - public ITagger CreateTagger(ITextBuffer buffer) where T : ITag { - ITagAggregator tagAggregator = AggregatorFactory.CreateTagAggregator(buffer); - // create a single tagger for each buffer. - Func> sc = delegate() { return new ProgressTagger(buffer, _serviceProvider, tagAggregator) as ITagger; }; - return buffer.Properties.GetOrCreateSingletonProperty>(sc); - } - } - - internal class ProgressTagger : ITagger - { - ErrorListProvider _errorProvider; - ITextBuffer _buffer; - - readonly DispatcherTimer timer; - - public ProgressTagger(ITextBuffer buffer, IServiceProvider serviceProvider, ITagAggregator tagAggregator) { - _buffer = buffer; - _errorProvider = new ErrorListProvider(serviceProvider); - - timer = new DispatcherTimer(DispatcherPriority.ApplicationIdle); - timer.Interval = TimeSpan.FromMilliseconds(500); - timer.Tick += new EventHandler(UponIdle); - - tagAggregator.TagsChanged += new EventHandler(_aggregator_TagsChanged); - buffer.Changed += new EventHandler(buffer_Changed); - bufferChangesPostVerificationStart.Add(new SnapshotSpan(buffer.CurrentSnapshot, 0, buffer.CurrentSnapshot.Length)); - } - - public void Dispose() { - } - - // The following fields and the contents of the following two lists are protected by the lock "this". - List bufferChangesPreVerificationStart = new List(); // buffer changes after the last completed verification and before the currently running verification - List bufferChangesPostVerificationStart = new List(); // buffer changes since the start of the currently running verification - - void buffer_Changed(object sender, TextContentChangedEventArgs e) { - lock (this) { - foreach (var change in e.Changes) { - var startLine = e.After.GetLineFromPosition(change.NewPosition); - var endLine = e.After.GetLineFromPosition(change.NewEnd); - bufferChangesPostVerificationStart.Add(new SnapshotSpan(startLine.Start, endLine.End)); - } - } - } - - // The next field is protected by "this" - ResolverTagger resolver; - // Keep track of the most recent resolution results. - void _aggregator_TagsChanged(object sender, TagsChangedEventArgs e) { - var r = sender as ResolverTagger; - if (r != null) { - lock (this) { - resolver = r; - } - timer.Stop(); - timer.Start(); - } - } - - bool verificationInProgress; // this field is protected by "this". Invariant: !verificationInProgress ==> bufferChangesPreVerificationStart.Count == 0 - /// - /// This method is invoked when the user has been idle for a little while. - /// Note, "sender" and "args" are allowed to be passed in as null--they are not used by this method. - /// - public void UponIdle(object sender, EventArgs args) { - Dafny.Program prog; - ITextSnapshot snap; - ResolverTagger r; - lock (this) { - if (verificationInProgress) { - // This UponIdle message came at an inopportune time--we've already kicked off a verification. - // Just back off. - return; - } - - if (resolver == null) return; - lock (resolver) { - prog = resolver._program; - snap = resolver._snapshot; - } - r = resolver; - resolver = null; - if (prog == null) return; - // We have a successfully resolved program to verify - - var resolvedVersion = snap.Version.VersionNumber; - if (bufferChangesPostVerificationStart.Count == 0) { - // Nothing new to verify. No reason to start a new verification. - return; - } else if (!bufferChangesPostVerificationStart.TrueForAll(span => span.Snapshot.Version.VersionNumber <= resolvedVersion)) { - // There have been buffer changes since the program that was resolved. Do nothing here, - // and instead just await the next resolved program. - return; - } - - // at this time, we're committed to running the verifier - verificationInProgress = true; - - // Change orange progress markers into yellow ones - Contract.Assert(bufferChangesPreVerificationStart.Count == 0); // follows from monitor invariant - var empty = bufferChangesPreVerificationStart; - bufferChangesPreVerificationStart = bufferChangesPostVerificationStart; - bufferChangesPostVerificationStart = empty; - // Notify to-whom-it-may-concern about the changes we just made - var chng = TagsChanged; - if (chng != null) { - chng(this, new SnapshotSpanEventArgs(new SnapshotSpan(snap, 0, snap.Length))); - } - - } - new Thread(() => VerificationWorker(prog, snap, r)).Start(); - } - - /// - /// Thread entry point. - /// - void VerificationWorker(Dafny.Program program, ITextSnapshot snapshot, ResolverTagger errorListHolder) { - Contract.Requires(program != null); - Contract.Requires(snapshot != null); - Contract.Requires(errorListHolder != null); - - // Run the verifier - var newErrors = new List(); - try { - bool success = DafnyDriver.Verify(program, errorInfo => { - newErrors.Add(new DafnyError(errorInfo.Tok.line - 1, errorInfo.Tok.col - 1, ErrorCategory.VerificationError, errorInfo.Msg)); - foreach (var aux in errorInfo.Aux) { - newErrors.Add(new DafnyError(aux.Tok.line - 1, aux.Tok.col - 1, ErrorCategory.AuxInformation, aux.Msg)); - } - }); - if (!success) { - newErrors.Add(new DafnyError(0, 0, ErrorCategory.InternalError, "verification process error")); - } - } catch (Exception e) { - newErrors.Add(new DafnyError(0, 0, ErrorCategory.InternalError, "verification process error: " + e.Message)); - } - errorListHolder.PopulateErrorList(newErrors, true, snapshot); - - lock (this) { - bufferChangesPreVerificationStart.Clear(); - verificationInProgress = false; - } - // Notify to-whom-it-may-concern about the cleared pre-verification changes - var chng = TagsChanged; - if (chng != null) { - chng(this, new SnapshotSpanEventArgs(new SnapshotSpan(snapshot, 0, snapshot.Length))); - } - - // If new changes took place since we started the verification, we may need to kick off another verification - // immediately. - UponIdle(null, null); - } - - public event EventHandler TagsChanged; - IEnumerable> ITagger.GetTags(NormalizedSnapshotSpanCollection spans) { - if (spans.Count == 0) yield break; - var targetSnapshot = spans[0].Snapshot; - - List pre; - List post; - lock (this) { - pre = bufferChangesPreVerificationStart; - post = bufferChangesPostVerificationStart; - } - - // If the requested snapshot isn't the same as the one our words are on, translate our spans to the expected snapshot - NormalizedSnapshotSpanCollection chs; - chs = new NormalizedSnapshotSpanCollection(Map(pre, span => span.TranslateTo(targetSnapshot, SpanTrackingMode.EdgeExclusive))); - foreach (SnapshotSpan span in NormalizedSnapshotSpanCollection.Overlap(spans, chs)) { - yield return new TagSpan(span, new ProgressGlyphTag(0)); - } - chs = new NormalizedSnapshotSpanCollection(Map(post, span => span.TranslateTo(targetSnapshot, SpanTrackingMode.EdgeExclusive))); - foreach (SnapshotSpan span in NormalizedSnapshotSpanCollection.Overlap(spans, chs)) { - yield return new TagSpan(span, new ProgressGlyphTag(1)); - } - } - - /// - /// (Why the firetruck isn't an extension method like this already in the standard library?) - /// - public static IEnumerable Map(IEnumerable coll, System.Func fn) { - foreach (var e in coll) { - yield return fn(e); - } - } - } -} diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/Properties/AssemblyInfo.cs b/Util/VS2010/DafnyExtension/DafnyExtension/Properties/AssemblyInfo.cs deleted file mode 100644 index b73b8410..00000000 --- a/Util/VS2010/DafnyExtension/DafnyExtension/Properties/AssemblyInfo.cs +++ /dev/null @@ -1,33 +0,0 @@ -using System.Reflection; -using System.Runtime.CompilerServices; -using System.Runtime.InteropServices; - -// General Information about an assembly is controlled through the following -// set of attributes. Change these attribute values to modify the information -// associated with an assembly. -[assembly: AssemblyTitle("EditorClassifier1")] -[assembly: AssemblyDescription("")] -[assembly: AssemblyConfiguration("")] -[assembly: AssemblyCompany("")] -[assembly: AssemblyProduct("EditorClassifier1")] -[assembly: AssemblyCopyright("")] -[assembly: AssemblyTrademark("")] -[assembly: AssemblyCulture("")] - -// Setting ComVisible to false makes the types in this assembly not visible -// to COM components. If you need to access a type in this assembly from -// COM, set the ComVisible attribute to true on that type. -[assembly: ComVisible(false)] - -// Version information for an assembly consists of the following four values: -// -// Major Version -// Minor Version -// Build Number -// Revision -// -// You can specify all the values or you can default the Build and Revision Numbers -// by using the '*' as shown below: -// [assembly: AssemblyVersion("1.0.*")] -[assembly: AssemblyVersion("1.0.0.0")] -[assembly: AssemblyFileVersion("1.0.0.0")] diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/ResolverTagger.cs b/Util/VS2010/DafnyExtension/DafnyExtension/ResolverTagger.cs deleted file mode 100644 index d1af6878..00000000 --- a/Util/VS2010/DafnyExtension/DafnyExtension/ResolverTagger.cs +++ /dev/null @@ -1,321 +0,0 @@ -//*************************************************************************** -// Copyright © 2010 Microsoft Corporation. All Rights Reserved. -// This code released under the terms of the -// Microsoft Public License (MS-PL, http://opensource.org/licenses/ms-pl.html.) -//*************************************************************************** -using EnvDTE; -using System; -using System.Collections.Generic; -using System.Linq; -using System.Text; -using System.ComponentModel.Composition; -using System.Windows.Threading; -using Microsoft.VisualStudio; -using Microsoft.VisualStudio.Shell; -using Microsoft.VisualStudio.Shell.Interop; -using Microsoft.VisualStudio.Text; -using Microsoft.VisualStudio.Text.Classification; -using Microsoft.VisualStudio.Text.Editor; -using Microsoft.VisualStudio.Text.Tagging; -using Microsoft.VisualStudio.Text.Projection; -using Microsoft.VisualStudio.TextManager.Interop; -using Microsoft.VisualStudio.Utilities; -using System.Diagnostics.Contracts; -using Dafny = Microsoft.Dafny; - -namespace DafnyLanguage -{ - [Export(typeof(ITaggerProvider))] - [ContentType("dafny")] - [TagType(typeof(DafnyResolverTag))] - internal sealed class ResolverTaggerProvider : ITaggerProvider - { - [Import(typeof(Microsoft.VisualStudio.Shell.SVsServiceProvider))] - internal IServiceProvider _serviceProvider = null; - - [Import] - ITextDocumentFactoryService _textDocumentFactory = null; - - public ITagger CreateTagger(ITextBuffer buffer) where T : ITag { - // create a single tagger for each buffer. - Func> sc = delegate() { return new ResolverTagger(buffer, _serviceProvider, _textDocumentFactory) as ITagger; }; - return buffer.Properties.GetOrCreateSingletonProperty>(sc); - } - } - - public abstract class DafnyResolverTag : ITag - { - } - public class DafnyErrorResolverTag : DafnyResolverTag - { - public readonly string Typ; - public readonly string Msg; - public DafnyErrorResolverTag(string typ, string msg) { - Typ = typ; - Msg = msg; - } - } - public class DafnySuccessResolverTag : DafnyResolverTag - { - public readonly Dafny.Program Program; - public DafnySuccessResolverTag(Dafny.Program program) { - Program = program; - } - } - - /// - /// Translate PkgDefTokenTags into ErrorTags and Error List items - /// - internal sealed class ResolverTagger : ITagger, IDisposable - { - ITextBuffer _buffer; - ITextDocument _document; - // The _snapshot and _program fields should be updated and read together, so they are protected by "this" - public ITextSnapshot _snapshot; // may be null - public Dafny.Program _program; // non-null only if the snapshot contains a Dafny program that type checks - List _resolutionErrors = new List(); // if nonempty, then _snapshot is the snapshot from which the errors were produced - List _verificationErrors = new List(); - ErrorListProvider _errorProvider; - - internal ResolverTagger(ITextBuffer buffer, IServiceProvider serviceProvider, ITextDocumentFactoryService textDocumentFactory) { - _buffer = buffer; - if (!textDocumentFactory.TryGetTextDocument(_buffer, out _document)) - _document = null; - _snapshot = null; // this makes sure the next snapshot will look different - _errorProvider = new ErrorListProvider(serviceProvider); - - BufferIdleEventUtil.AddBufferIdleEventListener(_buffer, ResolveBuffer); - } - - public void Dispose() { - if (_errorProvider != null) { - try { - _errorProvider.Tasks.Clear(); - } catch (InvalidOperationException) { - // this may occur if the SVsServiceProvider somehow has been uninstalled before our Dispose method is called - } - _errorProvider.Dispose(); - } - BufferIdleEventUtil.RemoveBufferIdleEventListener(_buffer, ResolveBuffer); - } - - public IEnumerable AllErrors() { - foreach (var err in _resolutionErrors) { - yield return err; - } - if (_resolutionErrors.Count != 0) { - // we're done - yield break; - } - foreach (var err in _verificationErrors) { - yield return err; - } - } - - /// - /// Find the Error tokens in the set of all tokens and create an ErrorTag for each - /// - public IEnumerable> GetTags(NormalizedSnapshotSpanCollection spans) { - if (spans.Count == 0) yield break; - var currentSnapshot = spans[0].Snapshot; - foreach (var err in AllErrors()) { - if (err.Category != ErrorCategory.ProcessError) { - var span = err.Span().TranslateTo(currentSnapshot, SpanTrackingMode.EdgeExclusive); - string ty; // the COLORs below indicate what I see on my machine - switch (err.Category) { - default: // unexpected category - case ErrorCategory.ParseError: - case ErrorCategory.ParseWarning: - ty = "syntax error"; break; // COLOR: red - case ErrorCategory.ResolveError: - ty = "compiler error"; break; // COLOR: blue - case ErrorCategory.VerificationError: - ty = "error"; break; // COLOR: red - case ErrorCategory.AuxInformation: - ty = "other error"; break; // COLOR: purple red - case ErrorCategory.InternalError: - ty = "error"; break; // COLOR: red - } - yield return new TagSpan(span, new DafnyErrorResolverTag(ty, err.Message)); - } - } - - ITextSnapshot snap; - Dafny.Program prog; - lock (this) { - snap = _snapshot; - prog = _program; - } - if (prog != null) { - yield return new TagSpan(new SnapshotSpan(snap, 0, snap.Length), new DafnySuccessResolverTag(prog)); - } - } - - public event EventHandler TagsChanged; - - /// - /// Calls the Dafny parser/resolver/type checker on the contents of the buffer, updates the Error List accordingly. - /// - void ResolveBuffer(object sender, EventArgs args) { - ITextSnapshot snapshot = _buffer.CurrentSnapshot; - if (snapshot == _snapshot) - return; // we've already done this snapshot - NormalizedSnapshotSpanCollection spans = new NormalizedSnapshotSpanCollection(new SnapshotSpan(snapshot, 0, snapshot.Length)); - - var driver = new DafnyDriver(snapshot.GetText(), _document != null ? _document.FilePath : ""); - List newErrors; - Dafny.Program program; - try { - program = driver.ProcessResolution(); - newErrors = driver.Errors; - } catch (Exception e) { - newErrors = new List(); - newErrors.Add(new DafnyError(0, 0, ErrorCategory.InternalError, "internal Dafny error: " + e.Message)); - program = null; - } - - lock (this) { - _snapshot = snapshot; - _program = program; - } - PopulateErrorList(newErrors, false, snapshot); - } - - public void PopulateErrorList(List newErrors, bool verificationErrors, ITextSnapshot snapshot) { - Contract.Requires(newErrors != null); - foreach (var err in newErrors) { - err.FillInSnapshot(snapshot); - } - if (verificationErrors) { - _verificationErrors = newErrors; - } else { - _resolutionErrors = newErrors; - } - - _errorProvider.SuspendRefresh(); // reduce flickering - _errorProvider.Tasks.Clear(); - foreach (var err in AllErrors()) { - ErrorTask task = new ErrorTask() { - Category = TaskCategory.BuildCompile, - ErrorCategory = CategoryConversion(err.Category), - Text = err.Message, - Line = err.Line, - Column = err.Column - }; - if (_document != null) { - task.Document = _document.FilePath; - } - if (err.Category != ErrorCategory.ProcessError && err.Category != ErrorCategory.InternalError) { - task.Navigate += new EventHandler(NavigateHandler); - } - _errorProvider.Tasks.Add(task); - } - _errorProvider.ResumeRefresh(); - var chng = TagsChanged; - if (chng != null) - chng(this, new SnapshotSpanEventArgs(new SnapshotSpan(snapshot, 0, snapshot.Length))); - } - - TaskErrorCategory CategoryConversion(ErrorCategory cat) { - switch (cat) { - case ErrorCategory.ParseError: - case ErrorCategory.ResolveError: - case ErrorCategory.VerificationError: - case ErrorCategory.InternalError: - return TaskErrorCategory.Error; - case ErrorCategory.ParseWarning: - return TaskErrorCategory.Warning; - case ErrorCategory.AuxInformation: - return TaskErrorCategory.Message; - default: - Contract.Assert(false); // unexpected category - return TaskErrorCategory.Error; // please compiler - } - } - - void NavigateHandler(object sender, EventArgs arguments) { - var task = sender as ErrorTask; - if (task == null || task.Document == null) - return; - - // This would have been the simple way of doing things: - // _errorProvider.Navigate(error, new Guid(EnvDTE.Constants.vsViewKindCode)); - // Unfortunately, it doesn't work--it seems to ignore the column position. (Moreover, it wants 1-based - // line/column numbers, whereas the Error Task pane wants 0-based line/column numbers.) - // So, instead we do all the things that follow: - - var openDoc = Package.GetGlobalService(typeof(IVsUIShellOpenDocument)) as IVsUIShellOpenDocument; - if (openDoc == null) - return; - - IVsWindowFrame frame; - Microsoft.VisualStudio.OLE.Interop.IServiceProvider sp; - IVsUIHierarchy hier; - uint itemid; - Guid logicalView = VSConstants.LOGVIEWID_Code; - if (Microsoft.VisualStudio.ErrorHandler.Failed(openDoc.OpenDocumentViaProject(task.Document, ref logicalView, out sp, out hier, out itemid, out frame)) || frame == null) - return; - - object docData; - Microsoft.VisualStudio.ErrorHandler.ThrowOnFailure(frame.GetProperty((int)__VSFPROPID.VSFPROPID_DocData, out docData)); - - // Get the VsTextBuffer - VsTextBuffer buffer = docData as VsTextBuffer; - if (buffer == null) { - IVsTextBufferProvider bufferProvider = docData as IVsTextBufferProvider; - if (bufferProvider != null) { - IVsTextLines lines; - Microsoft.VisualStudio.ErrorHandler.ThrowOnFailure(bufferProvider.GetTextBuffer(out lines)); - buffer = lines as VsTextBuffer; - if (buffer == null) - return; - } - } - - VsTextManager textManager = Package.GetGlobalService(typeof(VsTextManagerClass)) as VsTextManager; - if (textManager == null) - return; - - // Finally, move the cursor - Microsoft.VisualStudio.ErrorHandler.ThrowOnFailure(textManager.NavigateToLineAndColumn(buffer, ref logicalView, task.Line, task.Column, task.Line, task.Column)); - } - - } - - public enum ErrorCategory - { - ProcessError, ParseWarning, ParseError, ResolveError, VerificationError, AuxInformation, InternalError - } - - internal class DafnyError - { - public readonly int Line; // 0 based - public readonly int Column; // 0 based - ITextSnapshot Snapshot; // filled in during the FillInSnapshot call - public readonly ErrorCategory Category; - public readonly string Message; - /// - /// "line" and "col" are expected to be 0-based - /// - public DafnyError(int line, int col, ErrorCategory cat, string msg) { - Contract.Requires(0 <= line); - Contract.Requires(0 <= col); - Line = line; - Column = col; - Category = cat; - Message = msg; - } - - public void FillInSnapshot(ITextSnapshot snapshot) { - Contract.Requires(snapshot != null); - Snapshot = snapshot; - } - public SnapshotSpan Span() { - Contract.Requires(Snapshot != null); // requires that Snapshot has been filled in - var line = Snapshot.GetLineFromLineNumber(Line); - Contract.Assume(Column <= line.Length); // this is really a precondition of the constructor + FillInSnapshot - var length = Math.Min(line.Length - Column, 5); - return new SnapshotSpan(line.Start + Column, length); - } - } -} diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs b/Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs deleted file mode 100644 index 2f295429..00000000 --- a/Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs +++ /dev/null @@ -1,342 +0,0 @@ -using System; -using System.Collections.Generic; -using System.Linq; -using System.ComponentModel.Composition; -using Microsoft.VisualStudio.Text; -using Microsoft.VisualStudio.Text.Classification; -using Microsoft.VisualStudio.Text.Editor; -using Microsoft.VisualStudio.Text.Tagging; -using Microsoft.VisualStudio.Utilities; -using Dafny = Microsoft.Dafny; - -namespace DafnyLanguage -{ - [Export(typeof(ITaggerProvider))] - [ContentType("dafny")] - [TagType(typeof(DafnyTokenTag))] - internal sealed class DafnyTokenTagProvider : ITaggerProvider - { - public ITagger CreateTagger(ITextBuffer buffer) where T : ITag { - return new DafnyTokenTagger(buffer) as ITagger; - } - } - - public enum DafnyTokenKinds - { - Keyword, Number, String, Comment, - VariableIdentifier, VariableIdentifierDefinition - } - - public class DafnyTokenTag : ITag - { - public DafnyTokenKinds Kind { get; private set; } - public string HoverText { get; private set; } - - public DafnyTokenTag(DafnyTokenKinds kind) { - this.Kind = kind; - } - - public DafnyTokenTag(DafnyTokenKinds kind, string hoverText) { - this.Kind = kind; - this.HoverText = hoverText; - } - } - - internal sealed class DafnyTokenTagger : ITagger - { - ITextBuffer _buffer; - ITextSnapshot _snapshot; - List _regions; - - internal DafnyTokenTagger(ITextBuffer buffer) { - _buffer = buffer; - _snapshot = buffer.CurrentSnapshot; - _regions = Rescan(_snapshot); - - _buffer.Changed += new EventHandler(ReparseFile); - } - - public event EventHandler TagsChanged; - - public IEnumerable> GetTags(NormalizedSnapshotSpanCollection spans) { - if (spans.Count == 0) - yield break; - - List currentRegions = _regions; - ITextSnapshot currentSnapshot = _snapshot; - - // create a new SnapshotSpan for the entire region encompassed by the span collection - SnapshotSpan entire = new SnapshotSpan(spans[0].Start, spans[spans.Count - 1].End).TranslateTo(currentSnapshot, SpanTrackingMode.EdgeExclusive); - - // return tags for any regions that fall within that span - // BUGBUG: depending on how GetTags gets called (e.g., once for each line in the buffer), this may produce quadratic behavior - foreach (var region in currentRegions) { - if (entire.IntersectsWith(region.Span)) { - yield return new TagSpan(new SnapshotSpan(region.Start, region.End), new DafnyTokenTag(region.Kind)); - } - } - } - - /// - /// Find all of the tag regions in the document (snapshot) and notify - /// listeners of any that changed - /// - void ReparseFile(object sender, TextContentChangedEventArgs args) { - ITextSnapshot snapshot = _buffer.CurrentSnapshot; - if (snapshot == _snapshot) - return; // we've already computed the regions for this snapshot - - // get all of the outline regions in the snapshot - List newRegions = Rescan(snapshot); - - // determine the changed span, and send a changed event with the new spans - List oldSpans = new List(_regions.Select(r => - r.Span.TranslateTo(snapshot, SpanTrackingMode.EdgeExclusive))); - - List newSpans = new List(newRegions.Select(r => r.Span)); - - NormalizedSnapshotSpanCollection oldSpanCollection = new NormalizedSnapshotSpanCollection(oldSpans); - NormalizedSnapshotSpanCollection newSpanCollection = new NormalizedSnapshotSpanCollection(newSpans); - - NormalizedSnapshotSpanCollection difference = SymmetricDifference(oldSpanCollection, newSpanCollection); - - // save the new baseline - _snapshot = snapshot; - _regions = newRegions; - - var chng = TagsChanged; - if (chng != null) { - foreach (var span in difference) { - chng(this, new SnapshotSpanEventArgs(span)); - } - } - } - - NormalizedSnapshotSpanCollection SymmetricDifference(NormalizedSnapshotSpanCollection first, NormalizedSnapshotSpanCollection second) { - return NormalizedSnapshotSpanCollection.Union( - NormalizedSnapshotSpanCollection.Difference(first, second), - NormalizedSnapshotSpanCollection.Difference(second, first)); - } - - private static List Rescan(ITextSnapshot newSnapshot) { - List newRegions = new List(); - - bool stillScanningLongComment = false; - SnapshotPoint commentStart = new SnapshotPoint(); // used only when stillScanningLongComment - SnapshotPoint commentEndAsWeKnowIt = new SnapshotPoint(); // used only when stillScanningLongComment - foreach (ITextSnapshotLine line in newSnapshot.Lines) { - string txt = line.GetText(); // the current line (without linebreak characters) - int N = txt.Length; // length of the current line - int cur = 0; // offset into the current line - - if (stillScanningLongComment) { - if (ScanForEndOfComment(txt, ref cur)) { - newRegions.Add(new DRegion(commentStart, new SnapshotPoint(newSnapshot, line.Start + cur), DafnyTokenKinds.Comment)); - stillScanningLongComment = false; - } else { - commentEndAsWeKnowIt = new SnapshotPoint(newSnapshot, line.Start + cur); - } - } - - // repeatedly get the remaining tokens from this line - int end; // offset into the current line - for (; ; cur = end) { - // advance to the first character of a keyword or token - DafnyTokenKinds ty = DafnyTokenKinds.Keyword; - for (; ; cur++) { - if (N <= cur) { - // we've looked at everything in this line - goto OUTER_CONTINUE; - } - char ch = txt[cur]; - if ('a' <= ch && ch <= 'z') break; - if ('A' <= ch && ch <= 'Z') break; - if ('0' <= ch && ch <= '9') { ty = DafnyTokenKinds.Number; break; } - if (ch == '"') { ty = DafnyTokenKinds.String; break; } - if (ch == '/') { ty = DafnyTokenKinds.Comment; break; } - if (ch == '\'' || ch == '_' || ch == '?' || ch == '\\') break; // parts of identifiers - } - - // advance to the end of the token - end = cur + 1; // offset into the current line - if (ty == DafnyTokenKinds.Number) { - // scan the rest of this number - for (; end < N; end++) { - char ch = txt[end]; - if ('0' <= ch && ch <= '9') { - } else break; - } - } else if (ty == DafnyTokenKinds.String) { - // scan the rest of this string, but not past the end-of-line - for (; end < N; end++) { - char ch = txt[end]; - if (ch == '"') { - end++; break; - } else if (ch == '\\') { - // escape sequence - end++; - if (end == N) { break; } - ch = txt[end]; - if (ch == 'u') { - end += 4; - if (N <= end) { end = N; break; } - } - } - } - } else if (ty == DafnyTokenKinds.Comment) { - if (end == N) continue; // this was not the start of a comment - char ch = txt[end]; - if (ch == '/') { - // a short comment - end = N; - } else if (ch == '*') { - // a long comment; find the matching "*/" - end++; - commentStart = new SnapshotPoint(newSnapshot, line.Start + cur); - if (ScanForEndOfComment(txt, ref end)) { - newRegions.Add(new DRegion(commentStart, new SnapshotPoint(newSnapshot, line.Start + end), DafnyTokenKinds.Comment)); - } else { - stillScanningLongComment = true; - commentEndAsWeKnowIt = new SnapshotPoint(newSnapshot, line.Start + end); - } - continue; - } else { - // not a comment - continue; - } - } else { - int trailingDigits = 0; - for (; end < N; end++) { - char ch = txt[end]; - if ('a' <= ch && ch <= 'z') { - trailingDigits = 0; - } else if ('A' <= ch && ch <= 'Z') { - trailingDigits = 0; - } else if ('0' <= ch && ch <= '9') { - trailingDigits++; - } else if (ch == '\'' || ch == '_' || ch == '?' || ch == '\\') { - trailingDigits = 0; - } else break; - } - // we have a keyword or an identifier - string s = txt.Substring(cur, end - cur); - if (0 < trailingDigits && s.Length == 5 + trailingDigits && s.StartsWith("array") && s[5] != '0' && (trailingDigits != 1 || s[5] != '1')) { - // this is a keyword (array2, array3, ...) - } else { - switch (s) { - #region keywords - case "allocated": - case "array": - case "as": - case "assert": - case "assume": - case "bool": - case "break": - case "calc": - case "case": - case "choose": - case "class": - case "codatatype": - case "constructor": - case "copredicate": - case "datatype": - case "decreases": - case "else": - case "ensures": - case "exists": - case "false": - case "forall": - case "free": - case "fresh": - case "function": - case "ghost": - case "if": - case "import": - case "in": - case "int": - case "invariant": - case "iterator": - case "label": - case "match": - case "method": - case "modifies": - case "module": - case "multiset": - case "nat": - case "new": - case "null": - case "object": - case "old": - case "opened": - case "parallel": - case "predicate": - case "print": - case "reads": - case "refines": - case "requires": - case "result": - case "return": - case "returns": - case "seq": - case "set": - case "static": - case "then": - case "this": - case "true": - case "type": - case "var": - case "while": - case "yield": - case "yields": - #endregion - break; - default: - continue; // it was an identifier - } - } - } - - newRegions.Add(new DRegion(new SnapshotPoint(newSnapshot, line.Start + cur), new SnapshotPoint(newSnapshot, line.Start + end), ty)); - } - OUTER_CONTINUE: ; - } - - if (stillScanningLongComment) { - newRegions.Add(new DRegion(commentStart, commentEndAsWeKnowIt, DafnyTokenKinds.Comment)); - } - - return newRegions; - } - - private static bool ScanForEndOfComment(string txt, ref int end) { - int N = txt.Length; - for (; end < N; end++) { - char ch = txt[end]; - if (ch == '*' && end + 1 < N) { - ch = txt[end + 1]; - if (ch == '/') { - end += 2; - return true; - } - } - } - return false; // hit end-of-line without finding end-of-comment - } - } - - internal class DRegion - { - public SnapshotPoint Start { get; private set; } - public SnapshotPoint End { get; private set; } - public SnapshotSpan Span { - get { return new SnapshotSpan(Start, End); } - } - public DafnyTokenKinds Kind { get; private set; } - - public DRegion(SnapshotPoint start, SnapshotPoint end, DafnyTokenKinds kind) { - Start = start; - End = end; - Kind = kind; - } - } -} diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/WordHighlighter.cs b/Util/VS2010/DafnyExtension/DafnyExtension/WordHighlighter.cs deleted file mode 100644 index 03456c85..00000000 --- a/Util/VS2010/DafnyExtension/DafnyExtension/WordHighlighter.cs +++ /dev/null @@ -1,211 +0,0 @@ -using System; -using System.Collections.Generic; -using System.ComponentModel.Composition; -using System.Linq; -using System.Threading; -using System.Windows.Media; -using Microsoft.VisualStudio.Text; -using Microsoft.VisualStudio.Text.Classification; -using Microsoft.VisualStudio.Text.Editor; -using Microsoft.VisualStudio.Text.Operations; -using Microsoft.VisualStudio.Text.Tagging; -using Microsoft.VisualStudio.Utilities; - -namespace DafnyLanguage -{ -#if LATER_MAYBE - #region // (the current annoying) word highligher - internal class HighlightWordTagger : ITagger - { - ITextView View { get; set; } - ITextBuffer SourceBuffer { get; set; } - ITextSearchService TextSearchService { get; set; } - ITextStructureNavigator TextStructureNavigator { get; set; } - NormalizedSnapshotSpanCollection WordSpans { get; set; } - SnapshotSpan? CurrentWord { get; set; } - SnapshotPoint RequestedPoint { get; set; } - object updateLock = new object(); - - public HighlightWordTagger(ITextView view, ITextBuffer sourceBuffer, ITextSearchService textSearchService, - ITextStructureNavigator textStructureNavigator) { - this.View = view; - this.SourceBuffer = sourceBuffer; - this.TextSearchService = textSearchService; - this.TextStructureNavigator = textStructureNavigator; - this.WordSpans = new NormalizedSnapshotSpanCollection(); - this.CurrentWord = null; - this.View.Caret.PositionChanged += CaretPositionChanged; - this.View.LayoutChanged += ViewLayoutChanged; - } - - void ViewLayoutChanged(object sender, TextViewLayoutChangedEventArgs e) { - // If a new snapshot wasn't generated, then skip this layout - if (e.NewSnapshot != e.OldSnapshot) { - UpdateAtCaretPosition(View.Caret.Position); - } - } - - void CaretPositionChanged(object sender, CaretPositionChangedEventArgs e) { - UpdateAtCaretPosition(e.NewPosition); - } - - public event EventHandler TagsChanged; - - void UpdateAtCaretPosition(CaretPosition caretPosition) { - SnapshotPoint? point = caretPosition.Point.GetPoint(SourceBuffer, caretPosition.Affinity); - - if (!point.HasValue) - return; - - // If the new caret position is still within the current word (and on the same snapshot), we don't need to check it - if (CurrentWord.HasValue - && CurrentWord.Value.Snapshot == View.TextSnapshot - && CurrentWord.Value.Start <= point.Value && point.Value <= CurrentWord.Value.End) { - return; - } - - RequestedPoint = point.Value; - UpdateWordAdornments(); - } - - void UpdateWordAdornments() { - SnapshotPoint currentRequest = RequestedPoint; - List wordSpans = new List(); - //Find all words in the buffer like the one the caret is on - TextExtent word = TextStructureNavigator.GetExtentOfWord(currentRequest); - bool foundWord = true; - //If we've selected something not worth highlighting, we might have missed a "word" by a little bit - if (!WordExtentIsValid(currentRequest, word)) { - //Before we retry, make sure it is worthwhile - if (word.Span.Start != currentRequest - || currentRequest == currentRequest.GetContainingLine().Start - || char.IsWhiteSpace((currentRequest - 1).GetChar())) { - foundWord = false; - } else { - // Try again, one character previous. - //If the caret is at the end of a word, pick up the word. - word = TextStructureNavigator.GetExtentOfWord(currentRequest - 1); - - //If the word still isn't valid, we're done - if (!WordExtentIsValid(currentRequest, word)) - foundWord = false; - } - } - - if (!foundWord) { - //If we couldn't find a word, clear out the existing markers - SynchronousUpdate(currentRequest, new NormalizedSnapshotSpanCollection(), null); - return; - } - - SnapshotSpan currentWord = word.Span; - //If this is the current word, and the caret moved within a word, we're done. - if (CurrentWord.HasValue && currentWord == CurrentWord) - return; - - //Find the new spans - FindData findData = new FindData(currentWord.GetText(), currentWord.Snapshot); - findData.FindOptions = FindOptions.WholeWord | FindOptions.MatchCase; - - wordSpans.AddRange(TextSearchService.FindAll(findData)); - - //If another change hasn't happened, do a real update - if (currentRequest == RequestedPoint) - SynchronousUpdate(currentRequest, new NormalizedSnapshotSpanCollection(wordSpans), currentWord); - } - - static bool WordExtentIsValid(SnapshotPoint currentRequest, TextExtent word) { - return word.IsSignificant - && currentRequest.Snapshot.GetText(word.Span).Any(c => char.IsLetter(c)); - } - - void SynchronousUpdate(SnapshotPoint currentRequest, NormalizedSnapshotSpanCollection newSpans, SnapshotSpan? newCurrentWord) { - lock (updateLock) { - if (currentRequest != RequestedPoint) - return; - - WordSpans = newSpans; - CurrentWord = newCurrentWord; - - var chngd = TagsChanged; - if (chngd != null) - chngd(this, new SnapshotSpanEventArgs(new SnapshotSpan(SourceBuffer.CurrentSnapshot, 0, SourceBuffer.CurrentSnapshot.Length))); - } - } - - public IEnumerable> GetTags(NormalizedSnapshotSpanCollection spans) { - if (CurrentWord == null) - yield break; - - // Hold on to a "snapshot" of the word spans and current word, so that we maintain the same - // collection throughout - SnapshotSpan currentWord = CurrentWord.Value; - NormalizedSnapshotSpanCollection wordSpans = WordSpans; - - if (spans.Count == 0 || WordSpans.Count == 0) - yield break; - - // If the requested snapshot isn't the same as the one our words are on, translate our spans to the expected snapshot - if (spans[0].Snapshot != wordSpans[0].Snapshot) { - wordSpans = new NormalizedSnapshotSpanCollection( - wordSpans.Select(span => span.TranslateTo(spans[0].Snapshot, SpanTrackingMode.EdgeExclusive))); - - currentWord = currentWord.TranslateTo(spans[0].Snapshot, SpanTrackingMode.EdgeExclusive); - } - - // First, yield back the word the cursor is under (if it overlaps) - // Note that we'll yield back the same word again in the wordspans collection; - // the duplication here is expected. - if (spans.OverlapsWith(new NormalizedSnapshotSpanCollection(currentWord))) - yield return new TagSpan(currentWord, new HighlightWordTag()); - - // Second, yield all the other words in the file - foreach (SnapshotSpan span in NormalizedSnapshotSpanCollection.Overlap(spans, wordSpans)) { - yield return new TagSpan(span, new HighlightWordTag()); - } - } - } - - internal class HighlightWordTag : TextMarkerTag - { - public HighlightWordTag() : base("MarkerFormatDefinition/HighlightWordFormatDefinition") { } - } - - [Export(typeof(EditorFormatDefinition))] - [Name("MarkerFormatDefinition/HighlightWordFormatDefinition")] - [UserVisible(true)] - internal class HighlightWordFormatDefinition : MarkerFormatDefinition - { - public HighlightWordFormatDefinition() { - this.BackgroundColor = Colors.LightBlue; - this.ForegroundColor = Colors.DarkBlue; - this.DisplayName = "Highlight Word"; - this.ZOrder = 5; - } - } - - [Export(typeof(IViewTaggerProvider))] - [ContentType("text")] - [TagType(typeof(TextMarkerTag))] - internal class HighlightWordTaggerProvider : IViewTaggerProvider - { - [Import] - internal ITextSearchService TextSearchService { get; set; } - - [Import] - internal ITextStructureNavigatorSelectorService TextStructureNavigatorSelector { get; set; } - - public ITagger CreateTagger(ITextView textView, ITextBuffer buffer) where T : ITag { - //provide highlighting only on the top buffer - if (textView.TextBuffer != buffer) - return null; - - ITextStructureNavigator textStructureNavigator = - TextStructureNavigatorSelector.GetTextStructureNavigator(buffer); - - return new HighlightWordTagger(textView, buffer, TextSearchService, textStructureNavigator) as ITagger; - } - } -#endregion -#endif -} diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/source.extension.vsixmanifest b/Util/VS2010/DafnyExtension/DafnyExtension/source.extension.vsixmanifest deleted file mode 100644 index ef5c1cf5..00000000 --- a/Util/VS2010/DafnyExtension/DafnyExtension/source.extension.vsixmanifest +++ /dev/null @@ -1,25 +0,0 @@ - - - - DafnyLanguageMode - Microsoft Research - 1.0 - This is a language mode for using the Dafny language inside Visual Studio. - 1033 - - - Pro - - - Pro - - - - - - - |%CurrentProject%| - DafnyPrelude.bpl - UnivBackPred2.smt2 - - diff --git a/Util/latex/chalice.sty b/Util/latex/chalice.sty deleted file mode 100644 index a04d6f23..00000000 --- a/Util/latex/chalice.sty +++ /dev/null @@ -1,63 +0,0 @@ -\usepackage{listings} -%\lstloadlanguages{C} -\lstdefinestyle{chalice}{% - numbers=none, - firstnumber=0, - numberstyle=\tiny, - stepnumber=5, -% basicstyle=\scriptsize\sffamily,% -% commentstyle=\itshape,% -% keywordstyle=\bfseries,% -% ndkeywordstyle=\bfseries,% -% language=[Sharp]C, - morekeywords={% - above,acc,acquire,and,assert,assigned,assume,% - below,between,bool,% - call,class,const,% - downgrade,% - else,ensures,eval,exists,% - false,fold,forall,fork,free,function,% - ghost,% - holds,% - if,in,int,invariant,ite,% - join,% - lock,lockbottom,lockchange,% - method,module,% - new,nil,null,% - old,% - predicate,% - rd,reorder,release,requires,result,returns,% - seq,share,string,% - this,token,true,% - unfold,unfolding,unshare,% - var,% - waitlevel,while}, - literate=% - {=}{{=~}}1% - {+=}{{+}{=}~}3% - {-=}{{-}{=}~}3% - {*=}{{*}{=}~}3% - {++}{{+}{+}}2% - {--}{{-}{-}}2% - {==}{==}2% - {<=}{<=}2% - {=>}{=>}2% - {==>}{==>}3 % - {<==>}{<==>}4 % -%% % {!}{$\lnot$}1% don't do this if ! is also used to indicate non-null types - {!=}{!=}2% -}% -\lstnewenvironment{chalice}[1][]{% - \lstset{style=chalice, - floatplacement={tbp},showstringspaces=false,captionpos=b, - frame=lines,xleftmargin=8pt,xrightmargin=8pt,basicstyle=\ttfamily,#1}}{}% -\lstnewenvironment{chaliceNoLines}[1][]{% - \lstset{style=chalice, - floatplacement={tbp},showstringspaces=false,captionpos=b, - xleftmargin=8pt,xrightmargin=8pt,basicstyle=\ttfamily,#1}}{}% -\def\S{% - \lstinline[style=chalice,basicstyle=\ttfamily,columns=fixed]} -\newcommand{\lstfile}[1]{ - \lstinputlisting[style=chalice,% - frame=lines,xleftmargin=8pt,xrightmargin=8pt,basicstyle=\ttfamily,columns=fixed]{#1} -} diff --git a/Util/latex/dafny.sty b/Util/latex/dafny.sty deleted file mode 100644 index 879b90cb..00000000 --- a/Util/latex/dafny.sty +++ /dev/null @@ -1,110 +0,0 @@ -% dafny.sty -% Dafny mode for the LaTeX listings package. -% Rustan Leino, 22 June 2008. - -\usepackage{listings} - -\lstdefinelanguage{dafny}{ - 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,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,yield, - parallel,where,calc - }, - literate=% - {:}{$\colon$}1 - {::}{$\bullet$}2 - {:=}{$:$$=$}2 - {!}{$\lnot$}1 - {!!}{$\not\cap$}1 - {==}{$=$}1 - {!=}{$\neq$}1 - {&&}{$\land$}1 - {||}{$\lor$}1 - {<=}{$\le$}1 - {>=}{$\ge$}1 - % the following isn't actually Dafny, but it gives the option to produce nicer latex - {|=>}{$\Rightarrow$}2 - {<=set}{$\subseteq$}1 - {+set}{$\cup$}1 - {*set}{$\cap$}1 - {==>}{$\Longrightarrow$}3 - {=>}{$\Rightarrow$}2 - {<==>}{$\Longleftrightarrow$}4 - {forall}{$\forall$}1 - {exists}{$\exists$}1 - {!in}{$\not\in$}1 - {\\in}{$\in$}1 - % the following isn't actually Dafny, but it gives the option to produce nicer latex - {<<}{$\langle$}1 - {>>}{$\rangle$}1 - {(==)}{${}^{(=)}$}2 - {...}{$\ldots$}1 - {\\alpha}{$\alpha$}1 - {\\beta}{$\beta$}1 - {\\gamma}{$\gamma$}1 - {\\delta}{$\delta$}1 - {\\epsilon}{$\epsilon$}1 - {\\zeta}{$\zeta$}1 - {\\eta}{$\eta$}1 - {\\theta}{$\theta$}1 - {\\iota}{$\iota$}1 - {\\kappa}{$\kappa$}1 - {\\lambda}{$\lambda$}1 - {\\mu}{$\mu$}1 - {\\nu}{$\nu$}1 - {\\xi}{$\xi$}1 - {\\pi}{$\pi$}1 - {\\rho}{$\rho$}1 - {\\sigma}{$\sigma$}1 - {\\tau}{$\tau$}1 - {\\upsilon}{$\upsilon$}1 - {\\phi}{$\phi$}1 - {\\chi}{$\chi$}1 - {\\psi}{$\psi$}1 - {\\omega}{$\omega$}1 - {\\Gamma}{$\Gamma$}1 - {\\Delta}{$\Delta$}1 - {\\Theta}{$\Theta$}1 - {\\Lambda}{$\Lambda$}1 - {\\Xi}{$\Xi$}1 - {\\Pi}{$\Pi$}1 - {\\Sigma}{$\Sigma$}1 - {\\Upsilon}{$\Upsilon$}1 - {\\Phi}{$\Phi$}1 - {\\Psi}{$\Psi$}1 - {\\Omega}{$\Omega$}1 - , - sensitive=true, % case sensitive - morecomment=[l]{//}, - morecomment=[s]{/*}{*/}, - morestring=[b]", - numbers=none, - firstnumber=0, - numberstyle=\tiny, - stepnumber=5, - basicstyle=\scriptsize\sffamily, - commentstyle=\itshape, - keywordstyle=\bfseries, - ndkeywordstyle=\bfseries, -} -\lstnewenvironment{dafny}[1][]{% - \lstset{language=dafny, - floatplacement={tbp},captionpos=b, - frame=lines,xleftmargin=8pt,xrightmargin=8pt,basicstyle=\ttfamily,#1}}{} -\lstnewenvironment{dafnyNoLines}[1][]{% - \lstset{language=dafny, - floatplacement={tbp},captionpos=b, - xleftmargin=8pt,xrightmargin=8pt,basicstyle=\ttfamily,#1}}{} -\def\inlinedafny{% - \lstinline[language=dafny,basicstyle=\ttfamily,columns=fixed]} -\newcommand{\lstfile}[1]{ - \lstinputlisting[language=dafny,% - frame=lines,xleftmargin=8pt,xrightmargin=8pt,basicstyle=\ttfamily,columns=fixed]{#1} -} diff --git a/Util/vim/syntax/chalice.vim b/Util/vim/syntax/chalice.vim deleted file mode 100644 index 86b65d74..00000000 --- a/Util/vim/syntax/chalice.vim +++ /dev/null @@ -1,44 +0,0 @@ -" Vim syntax file -" Language: Chalice -" Author: Kuat Yessenov -" Date: 7/14/2010 - -syntax clear -syntax case match -syntax keyword chaliceFunction function method predicate -syntax keyword chaliceTypeDef class channel module -syntax keyword chaliceConditional if then else -syntax keyword chaliceRepeat foreach while -syntax keyword chaliceStatement assert assume call reorder share unshare acquire release lock rd downgrade free fold unfold fork join wait signal send receive -syntax keyword chaliceKeyword external var ghost returns where const new between and above below waitlevel lockbottom this result holds refines replaces spec by transforms -syntax keyword chaliceType int bool string seq token -syntax keyword chaliceLogic invariant requires ensures lockchange -syntax keyword chaliceOperator forall exists old fresh old credit acc unfolding in eval ite rd -syntax keyword chaliceBoolean true false - -syntax region chaliceString start=/"/ skip=/\\"/ end=/"/ - -syntax match chaliceComment /\/\/.*/ -syntax region chaliceComment start="/\*" end="\*/" - -syntax match chaliceNumber /\d\+\>/ -syntax match chaliceIdentifier /\<\w\+\>/ - -syntax match chaliceOperator "==>" -syntax match chaliceOperator "<==>" -syntax match chaliceOperator ":=" -syntax match chaliceOperator "<<" - -highlight link chaliceFunction Function -highlight link chaliceTypeDef Typedef -highlight link chaliceConditional Conditional -highlight link chaliceRepeat Repeat -highlight link chaliceKeyword Keyword -highlight link chaliceType Type -highlight link chaliceLogic Debug -highlight link chaliceComment Comment -highlight link chaliceString String -highlight link chaliceNumber Number -highlight link chaliceOperator Operator -highlight link chaliceStatement Statement -highlight link chaliceBoolean Boolean diff --git a/Util/vim/syntax/dafny.vim b/Util/vim/syntax/dafny.vim deleted file mode 100644 index 45afbcf0..00000000 --- a/Util/vim/syntax/dafny.vim +++ /dev/null @@ -1,44 +0,0 @@ -" Vim syntax file -" Language: Dafny -" Author: Kuat Yessenov -" Date: 6/24/2010 - -syntax clear -syntax case match -syntax keyword dafnyFunction function predicate copredicate method constructor -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 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 -syntax keyword dafnyBoolean true false - -syntax region dafnyString start=/"/ skip=/\\"/ end=/"/ - -syntax match dafnyComment /\/\/.*/ -syntax region dafnyComment start="/\*" end="\*/" - -syntax match dafnyNumber /\d\+\>/ -syntax match dafnyIdentifier /\<\w\+\>/ - -syntax match dafnyOperator "==>" -syntax match dafnyOperator "<==>" -syntax match dafnyOperator "::" - -highlight link dafnyFunction Function -highlight link dafnyTypeDef Typedef -highlight link dafnyConditional Conditional -highlight link dafnyRepeat Repeat -highlight link dafnyKeyword Keyword -highlight link dafnyType Type -highlight link dafnyLogic Debug -highlight link dafnyComment Comment -highlight link dafnyString String -highlight link dafnyNumber Number -highlight link dafnyOperator Operator -highlight link dafnyStatement Statement -highlight link dafnyBoolean Boolean -- cgit v1.2.3