Merge pull request #2 from lordqwerty/master

Renaming, updating and snippets

.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

Commands/Default.sublime-commands

@@ -8,7 +8,7 @@
         "command": "tamarin_prove_interactive"
     },
     {
-        "caption": "Tamarin: Typecheck",
+        "caption": "Tamarin: Check",
         "command": "tamarin_check"
     }
 ]

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"
                             },

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

Snippets/hide-lemma.sublime-snippet

@@ -0,0 +1,6 @@
+<snippet>
+    <content><![CDATA[hide_lemma=]]></content>
+    <tabTrigger>hide_lemma</tabTrigger>
+    <description>Tamarin - Hide Lemma</description>
+    <scope>source.spthy</scope>
+</snippet>

Snippets/left.sublime-snippet

@@ -0,0 +1,6 @@
+<snippet>
+    <content><![CDATA[left]]></content>
+    <tabTrigger>left</tabTrigger>
+    <description>Tamarin - Left</description>
+    <scope>source.spthy</scope>
+</snippet>

Snippets/lemma.sublime-snippet

@@ -1,9 +1,9 @@
 <snippet>
     <content><![CDATA[
 lemma $1:
-  "
-
-  "
+"
+    
+"
 ]]></content>
     <tabTrigger>lemma</tabTrigger>
     <description>Tamarin - Skeleton Lemma</description>

Snippets/restriction.sublime-snippet

@@ -1,9 +1,9 @@
 <snippet>
     <content><![CDATA[
 restriction $1:
-  "
-
-  "
+"
+    
+"
 ]]></content>
     <tabTrigger>restriction</tabTrigger>
     <description>Tamarin - Skeleton restriction</description>

Snippets/reuse.sublime-snippet

@@ -0,0 +1,6 @@
+<snippet>
+    <content><![CDATA[reuse]]></content>
+    <tabTrigger>reuse</tabTrigger>
+    <description>Tamarin - Reuse</description>
+    <scope>source.spthy</scope>
+</snippet>

Snippets/right.sublime-snippet

@@ -0,0 +1,6 @@
+<snippet>
+    <content><![CDATA[right]]></content>
+    <tabTrigger>right</tabTrigger>
+    <description>Tamarin - Right</description>
+    <scope>source.spthy</scope>
+</snippet>

Snippets/rule.sublime-snippet

@@ -2,7 +2,7 @@
     <content><![CDATA[
 rule $1:
   let
-
+    
   in
     [  ]
   --[  ]->

Syntaxes/spthy.sublime-syntax

@@ -35,15 +35,15 @@ 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
 
     - match: "\\b(in|let|begin|end)\\b"
       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
 
 

info.plist

@@ -3,13 +3,13 @@
 <plist version="1.0">
 <dict>
     <key>contactEmailRot13</key>
-    <string>[email protected].uk</string>
+    <string>[email protected].uk</string>
     <key>contactName</key>
     <string>Jorden Whitefield</string>
     <key>description</key>
     <string>Bundle that adds support for the Tamarin Prover.</string>
     <key>name</key>
-    <string>TamarinAssist</string>
+    <string>TamarinProver</string>
     <key>uuid</key>
     <string>A6B019CB-75BF-4D9A-AAB1-703F6B6D143B</string>
 </dict>

tamarin_assist.py → 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', {

upgrade.py

@@ -1,7 +1,7 @@
 import sys
 
 
-package_name = 'TamarinAssist'
+package_name = 'TamarinProver'
 
 
 def plugin_loaded():