From 0f16602bbc3a43cfcc240575143be083b01e923c Mon Sep 17 00:00:00 2001 From: Jorden Whitefield Date: Thu, 4 Oct 2018 09:23:50 +0100 Subject: [PATCH] Renaming, updating grammar and snippets --- .github/PULL_REQUEST_TEMPLATE.md | 2 +- Commands/Default.sublime-commands | 2 +- Main.sublime-menu | 6 ++-- README.md | 36 ++++++++++++++++--- Snippets/hide-lemma.sublime-snippet | 6 ++++ Snippets/left.sublime-snippet | 6 ++++ Snippets/lemma.sublime-snippet | 6 ++-- Snippets/restriction.sublime-snippet | 6 ++-- Snippets/reuse.sublime-snippet | 6 ++++ Snippets/right.sublime-snippet | 6 ++++ Snippets/rule.sublime-snippet | 2 +- Syntaxes/spthy.sublime-syntax | 4 +-- ...e-project => TamarinProver.sublime-project | 0 ...settings => TamarinProver.sublime-settings | 0 info.plist | 4 +-- tamarin_assist.py => tamarin_prover.py | 8 ++--- upgrade.py | 2 +- 17 files changed, 76 insertions(+), 26 deletions(-) create mode 100644 Snippets/hide-lemma.sublime-snippet create mode 100644 Snippets/left.sublime-snippet create mode 100644 Snippets/reuse.sublime-snippet create mode 100644 Snippets/right.sublime-snippet rename TamarinAssist.sublime-project => TamarinProver.sublime-project (100%) rename TamarinAssist.sublime-settings => TamarinProver.sublime-settings (100%) rename tamarin_assist.py => tamarin_prover.py (97%) diff --git a/.github/PULL_REQUEST_TEMPLATE.md b/.github/PULL_REQUEST_TEMPLATE.md index 8fad9af..a4f2277 100644 --- a/.github/PULL_REQUEST_TEMPLATE.md +++ b/.github/PULL_REQUEST_TEMPLATE.md @@ -2,7 +2,7 @@ - [ ] Followed the guidelines in our [CONTRIBUTING](CONTRIBUTING.md) document? - [ ] Followed the Google Python [Style Guide](https://google.github.io/styleguide/pyguide.html) document? -- [ ] Checked to ensure there aren't other open [Pull Requests](https://github.com/lordqwerty/TamarinAssist/pulls) for the same update/change? +- [ ] Checked to ensure there aren't other open [Pull Requests](https://github.com/tamarin-prover/editor-sublime/pulls) for the same update/change? - [ ] Checked to ensure the plugin compiles and works as expected? ### New Feature diff --git a/Commands/Default.sublime-commands b/Commands/Default.sublime-commands index d685168..b166d03 100644 --- a/Commands/Default.sublime-commands +++ b/Commands/Default.sublime-commands @@ -8,7 +8,7 @@ "command": "tamarin_prove_interactive" }, { - "caption": "Tamarin: Typecheck", + "caption": "Tamarin: Check", "command": "tamarin_check" } ] \ No newline at end of file diff --git a/Main.sublime-menu b/Main.sublime-menu index 5ffa696..f989095 100644 --- a/Main.sublime-menu +++ b/Main.sublime-menu @@ -12,20 +12,20 @@ "children": [ { - "caption": "TamarinAssist", + "caption": "editor-sublime", "children": [ { "command": "open_file", "args": { - "file": "${packages}/TamarinAssist/Tamarin.sublime-settings" + "file": "${packages}/editor-sublime/TamarinProver.sublime-settings" }, "caption": "Settings – Default" }, { "command": "open_file", "args": { - "file": "${packages}/User/TamarinAssist.sublime-settings" + "file": "${packages}/User/TamarinProver.sublime-settings" }, "caption": "Settings – User" }, diff --git a/README.md b/README.md index 87fab6b..5022846 100644 --- a/README.md +++ b/README.md @@ -26,19 +26,45 @@ type "*Tamarin*" to see the options available. - [X] Basic Syntaxes - [X] Run Tamarin within Sublime -- [X] Snippets for Theory, Rule, Axiom and Lemma -- [X] Add package to [PackageControl.io] +- [X] Snippets for Theory, Rule, Restriction and Lemma - [X] Configure `SAPIC` path ## Under Development +- [ ] Add package to [PackageControl.io] - [ ] Highlight Script errors in Editor - [ ] Highlight Restriction / Lemma Guardedness issues in Editor -## Package Control +## Installation -[PackageControl.io](https://packagecontrol.io/packages/) can now be installed via the sublime package manager. See the -[install](https://packagecontrol.io/installation) and [usage](https://packagecontrol.io/docs/usage) documentation. +### Manual + +### OS X + +```bash +$ git clone https://github.com/tamarin-prover/editor-sublime.git +$ ln -s `pwd`/editor-sublime ~/Library/Application\ Support/Sublime\ Text\ 3/Packages/ +``` + +### Linux + +```bash +$ git clone https://github.com/tamarin-prover/editor-sublime.git +$ ln -s `pwd`/editor-sublime ~/.config/sublime-text-3/Packages/ +``` + +### Windows + +On Windows, you can use directory junctions instead of symlinks (symlinks require administrative rights; directory junctions don't): +```powershell +# Using PowerShell +PS> git clone https://github.com/tamarin-prover/editor-sublime.git +PS> cmd /c mklink /J "$env:APPDATA/Sublime Text 3/Packages/editor-sublime" (convert-path ./editor-sublime) +``` + +### Package Control + +[PackageControl.io](https://packagecontrol.io/packages/) currently in development and hope to bring this installation method back very soon. [Tamarin]:https://tamarin-prover.github.io/ [Tamarin GitHub]:https://github.com/tamarin-prover/tamarin-prover diff --git a/Snippets/hide-lemma.sublime-snippet b/Snippets/hide-lemma.sublime-snippet new file mode 100644 index 0000000..bbc366f --- /dev/null +++ b/Snippets/hide-lemma.sublime-snippet @@ -0,0 +1,6 @@ + + + hide_lemma + Tamarin - Hide Lemma + source.spthy + diff --git a/Snippets/left.sublime-snippet b/Snippets/left.sublime-snippet new file mode 100644 index 0000000..e559c4c --- /dev/null +++ b/Snippets/left.sublime-snippet @@ -0,0 +1,6 @@ + + + left + Tamarin - Left + source.spthy + diff --git a/Snippets/lemma.sublime-snippet b/Snippets/lemma.sublime-snippet index 4a34f3f..c61033b 100644 --- a/Snippets/lemma.sublime-snippet +++ b/Snippets/lemma.sublime-snippet @@ -1,9 +1,9 @@ lemma Tamarin - Skeleton Lemma diff --git a/Snippets/restriction.sublime-snippet b/Snippets/restriction.sublime-snippet index 4140d9a..f9d130b 100644 --- a/Snippets/restriction.sublime-snippet +++ b/Snippets/restriction.sublime-snippet @@ -1,9 +1,9 @@ restriction Tamarin - Skeleton restriction diff --git a/Snippets/reuse.sublime-snippet b/Snippets/reuse.sublime-snippet new file mode 100644 index 0000000..ff112b3 --- /dev/null +++ b/Snippets/reuse.sublime-snippet @@ -0,0 +1,6 @@ + + + reuse + Tamarin - Reuse + source.spthy + diff --git a/Snippets/right.sublime-snippet b/Snippets/right.sublime-snippet new file mode 100644 index 0000000..d471a1d --- /dev/null +++ b/Snippets/right.sublime-snippet @@ -0,0 +1,6 @@ + + + right + Tamarin - Right + source.spthy + diff --git a/Snippets/rule.sublime-snippet b/Snippets/rule.sublime-snippet index 482dfe0..91ec417 100644 --- a/Snippets/rule.sublime-snippet +++ b/Snippets/rule.sublime-snippet @@ -2,7 +2,7 @@ diff --git a/Syntaxes/spthy.sublime-syntax b/Syntaxes/spthy.sublime-syntax index 2989da6..eae9b25 100644 --- a/Syntaxes/spthy.sublime-syntax +++ b/Syntaxes/spthy.sublime-syntax @@ -35,7 +35,7 @@ contexts: - match: \) scope: invalid.illegal.stray-bracket-end - - match: "\\b(aenc|sdec|senc|sdec|sign|verify|Eq|eq|hashing|signing|diffie-hellman|symmetric-encryption|asymmetric-encryption|multiset|bilinear-pairing|h|H|sk|pk|Fr|In|Out|fr|in|out)\\b" + - match: "\\b(aenc|adec|senc|sdec|sign|verify|Eq|eq|hashing|signing|revealing-signing|diffie-hellman|symmetric-encryption|asymmetric-encryption|multiset|bilinear-pairing|h|H|sk|pk|Fr|In|Out|IN|OUT)\\b" scope: variable.language.spthy comment: Tamarin constr keywords @@ -43,7 +43,7 @@ contexts: scope: constant.language.spthy comment: Tamarin decl keywords - - match: "\\b(axiom|restriction|lemma|source|builtins|protocol|property|subsection|section|text|theory)\\b" + - match: "\\b(axiom|restriction|lemma|sources|use_induction|reuse|hide_lemma|left|right|builtins|protocol|property|subsection|section|text|theory)\\b" scope: keyword.control.spthy diff --git a/TamarinAssist.sublime-project b/TamarinProver.sublime-project similarity index 100% rename from TamarinAssist.sublime-project rename to TamarinProver.sublime-project diff --git a/TamarinAssist.sublime-settings b/TamarinProver.sublime-settings similarity index 100% rename from TamarinAssist.sublime-settings rename to TamarinProver.sublime-settings diff --git a/info.plist b/info.plist index e267dd6..a29b1c4 100644 --- a/info.plist +++ b/info.plist @@ -3,13 +3,13 @@ contactEmailRot13 - j.whitefield@surrey.ac.uk + jorden@jwhitefield.co.uk contactName Jorden Whitefield description Bundle that adds support for the Tamarin Prover. name - TamarinAssist + TamarinProver uuid A6B019CB-75BF-4D9A-AAB1-703F6B6D143B diff --git a/tamarin_assist.py b/tamarin_prover.py similarity index 97% rename from tamarin_assist.py rename to tamarin_prover.py index 7886398..0f27602 100644 --- a/tamarin_assist.py +++ b/tamarin_prover.py @@ -13,7 +13,7 @@ LOCAL = '/usr/local/bin:/usr/local/sbin' -SYNTAX_FILE = 'Packages/TamarinAssist/Syntaxes/spthy.sublime-syntax' +SYNTAX_FILE = 'Packages/editor-sublime/Syntaxes/spthy.sublime-syntax' VERSION = "0.0.1" os.environ['PATH'] += ':' @@ -30,7 +30,7 @@ def stream_watcher(identifier, stream): def settings_get(name, default=None): - plugin_settings = sublime.load_settings('TamarinAssist.sublime-settings') + plugin_settings = sublime.load_settings('TamarinProver.sublime-settings') project_settings = None if sublime.active_window() and sublime.active_window().active_view(): project_settings = sublime.active_window().active_view().settings() @@ -156,7 +156,7 @@ def run(self): if view is None: return self.output_view = self.window.new_file() - self.output_view.set_name("Tamarin Typecheck") + self.output_view.set_name("Tamarin Check") self.output_view.set_scratch(True) self.output_view.set_read_only(True) self._runner(get_spthy_file(view)) @@ -212,7 +212,7 @@ def printer(proc): def print_sublime_tamarin(self): - MESSAGE = "TamarinAssist v" + VERSION + MESSAGE = "TamarinProver v" + VERSION self.output_view.set_read_only(False) self.output_view.run_command('tamarin_insert_text', { diff --git a/upgrade.py b/upgrade.py index 382442f..cc82465 100644 --- a/upgrade.py +++ b/upgrade.py @@ -1,7 +1,7 @@ import sys -package_name = 'TamarinAssist' +package_name = 'TamarinProver' def plugin_loaded():