more ketwords & snippets

Author: linwe2012

.gitignore

@@ -1,2 +1,4 @@
 *.visx
-*.vsix
+*.vsix
+*.aes
+*.spthy

README.md

@@ -2,4 +2,6 @@
 
 An extension for highlighting tamarin-prover.
 
+Also include some snippets to smooth developing
+
 see http://tamarin-prover.github.io/

package.json

@@ -1,6 +1,6 @@
 {
     "name": "tamarin",
-    "version": "0.0.4",
+    "version": "0.0.5",
     "engines": {
         "vscode": ">=0.9.0-pre.1"
     },

snippets.json

@@ -22,7 +22,7 @@
         ],
         "description": "Generate full rule wit let in"
     },
-    "thoery": {
+    "theory": {
         "prefix": "theory",
         "body": [
             "theory $1",
@@ -61,7 +61,7 @@
         "description": "Create a fresh nounce"
     },
     "pair": {
-        "prefix": "<",
+        "prefix": "pair",
         "body":[
             "< $1, $2 >"
         ],
@@ -88,6 +88,38 @@
             "\t[ $2 ]\n\t--[\n\t\t\n\t]->\n\t[ $3 ]"
         ],
         "description": "Create an init rule"
+    },
+    "let in": {
+        "prefix": "let",
+        "body":[
+            "\tlet",
+            "\t\t$1",
+            "in"
+        ]
+    },
+    "all-traces": {
+        "prefix": "all",
+        "body": [
+            "all-traces"
+        ],
+        "description": "Tamarin - All Traces"
+    },
+    "exists-trace": {
+        "prefix": "exist",
+        "body":[
+            "exists-trace"
+        ],
+        "description": "Lemma proven once a trace is found"
+    },
+    "restrition": {
+        "prefix": "restriction",
+        "body":[
+            "restriction $1:",
+            "\"",
+            "\t$2",
+            "\""
+        ],
+        "description": "restriction skeleton"
     }
 
 }

syntaxes/tamarin.YAML-tmLanguage

@@ -0,0 +1,87 @@
+name: Tamarin
+file_extensions:
+  - spthy
+scope: source.spthy
+fileTypes: [YAML-tmLanguage]
+scopeName: source.yaml-tmlanguage
+uuid: a6b019cb-75bf-4d9a-aab1-703f6b6d143b
+
+foldingStartMarker: "(?x)\n\t\t /\\*\\*(?!\\*)\n\t\t|^(?![^{]*?//|[^{]*?/\\*(?!.*?\\*/.*?\\{)).*?\\{\\s*($|//|/\\*(?!.*?\\*/.*\\S))\n\t"
+foldingStopMarker: "(?<!\\*)\\*\\*/|^\\s*\\}"
+
+contexts:
+  main:
+    - include: comments
+    - include: comments-inline
+
+    - match: '"'
+      scope: punctuation.definition.string.begin.spthy
+
+    - match: \b(equations|functions|builtins|protocol|property|theory|begin|end|subsection|section|text|rule|pb|lts|exists-trace|all-traces|enable|assertions|modulo|default_rules|anb-proto|in|let|Fresh|fresh|Public|public)\b
+      scope: keyword.function.spthy
+
+    - match: '{\||\|}|{|}|\.\.|:|@|#|<-|<->|\!=|<=|>=|--\[|\]->|\[|\]|-->'
+      scope: keyword.operator.spthy
+
+
+    # Numbers
+    - match: '\b(-)?[0-9.]+\b'
+      scope: constant.numeric.spthy
+
+    # Brackets
+    - match: \(
+      push: brackets
+    - match: \)
+      scope: invalid.illegal.stray-bracket-end
+
+    - 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|sources|use_induction|reuse|hide_lemma|left|right|builtins|protocol|property|subsection|section|text|theory)\\b"
+      scope: keyword.control.spthy
+
+
+    - match: "(\\b(F|T|All|Ex|not|)\\b|&|\\||==>|=|==|<|>)"
+      scope: constant.language.spthy
+      comment: Tamarin logical operations
+
+    - match: "'"
+      captures:
+        0: punctuation.definition.string.begin.spthy
+      push:
+        - meta_scope: string.quoted.single.spthy
+        - match: "'"
+          captures:
+            0: punctuation.definition.string.end.spthy
+          pop: true
+
+    - match: \w+\s*(?=\()
+      scope: support.function.spthy
+
+
+  comments:
+    - match: /\*\*/
+      scope: comment.block.empty.spthy punctuation.definition.comment.spthy
+    - include: comments-inline
+  comments-inline:
+    - match: /\*
+      scope: punctuation.definition.comment.spthy
+      push:
+        - meta_scope: comment.block.spthy
+        - match: \*/
+          scope: punctuation.definition.comment.spthy
+          pop: true
+    - match: \s*((//).*$\n?)
+      captures:
+        1: comment.line.double-slash.spthy
+        2: punctuation.definition.comment.spthy
+
+  brackets:
+    - match: \)
+      pop: true
+    - include: main

syntaxes/tamarin.tmLanguage

@@ -33,11 +33,17 @@
       <!-- key words -->
       <dict>
          <key>match</key>
-         <string>\b(axiom|lemma|equations|functions|builtins|protocol|property|theory|begin|end|subsection|section|text|rule|pb|lts|exists-trace|all-traces|enable|assertions|modulo|default_rules|anb-proto|in|let|Fresh|fresh|Public|public)\b</string>
+         <string>\b(equations|functions|builtins|protocol|property|theory|begin|end|subsection|section|text|rule|pb|lts|exists-trace|all-traces|enable|assertions|modulo|default_rules|anb-proto|in|let|Fresh|fresh|Public|public)\b</string>
          <key>name</key>
          <string>keyword.control</string>
       </dict>
 
+      <dict>
+         <key>match</key>
+         <string>\b(axiom|restriction|lemma|sources|use_induction|reuse|hide_lemma|left|right|builtins|protocol|property|subsection|section|text)\b</string>
+         <key>name</key>
+         <string>keyword.control</string>
+      </dict>
 
 
       <dict>