Unnamed repository; edit this file 'description' to name the repository.
Diffstat (limited to 'runtime/queries/proverif/highlights.scm')
| -rw-r--r-- | runtime/queries/proverif/highlights.scm | 203 |
1 files changed, 203 insertions, 0 deletions
diff --git a/runtime/queries/proverif/highlights.scm b/runtime/queries/proverif/highlights.scm new file mode 100644 index 00000000..abafe833 --- /dev/null +++ b/runtime/queries/proverif/highlights.scm @@ -0,0 +1,203 @@ +;; fallback for identifiers +(ident) @variable + +;; Comments + +(comment) @comment + +; CryptoVerif-only opaque blocks +(proof) @comment.unused +(def) @comment.unused + +;; Types +(type_def + name: (ident) @type) + +(typeid) @type +(typeid + (ident) @type) + +(decl_table + name: (ident) @type) + +;; Function & Macro Definitions + +(function_def + name: (ident) @function) + +(function_macro_def + name: (ident) @function.macro) + +(decl_pred + name: (ident) @function) + +(decl_event + name: (ident) @function) + +;; Function Calls + +(term_function_call + name: (ident) @function) +(term_function_call + (term (ident) @variable.parameter)) + +(pterm_function_call + name: (ident) @function) +(pterm_function_call + (pterm (ident) @variable.parameter)) + +(decl_process_macro + name: (ident) @function) +(decl_process_macro + (typedecl (ident) @variable.parameter)) + +(gterm_function_call + name: (ident) @function) +(gterm_function_call + (gterm (ident) @variable.parameter)) + +(gformat_function_call + name: (ident) @function) +(gformat_function_call + (gformat (ident) @variable.parameter)) + +(process_function_call + name: (ident) @function) +(process_function_call + (pterm (ident) @variable.parameter)) + +(process_input "in" @function.builtin) +(process_input + (pterm (ident) @variable.parameter)) +(process_input + (pattern (ident) @variable.parameter)) +(process_input + (pattern (pattern (ident) @variable.parameter))) + +(process_output "out" @function.builtin) +(process_output + (pterm (ident) @variable.parameter)) +(process_output + (pterm (pterm (ident) @variable.parameter))) + +;; Literals + +(nat) @constant.numeric +(int) @constant.numeric +(string) @string + +[ + "true" + "false" +] @constant.builtin.boolean + +"fail" @constant.builtin + +(process_final_item + "0" @constant.builtin) + +;; Keywords + +[ + "among" + "axiom" + "choice" + "clauses" + "const" + "def" + "elimtrue" + "else" + "equation" + "equivalence" + "event" + "expand" + "fail" + "forall" + "foreach" + "free" + "fun" + "get" + "if" + "inj-event" + "insert" + "lemma" + "let" + "letfun" + "letproba" + "new" + "noninterf" + "noselect" + "not" + "nounif" + "otherwise" + "param" + "phase" + "pred" + "proba" + "process" + "proof" + "public_vars" + "putbegin" + "query" + "reduc" + "restriction" + "secret" + "select" + "set" + "suchthat" + "sync" + "table" + "then" + "type" + "weaksecret" + "yield" +] @keyword + +(decl_channel "channel" @keyword) ; "channel" can also be used as type, hence the restriction +(process_let "in" @keyword) ; "in" can is keyword in "let ... in", but builtin function otherwise + +;; Operators + +[ + "=" + "<>" + "<=" + ">=" + "<" + ">" + "+" + "-" + "==>" + "<-" + "<-R" + "->" + "<->" + "<=>" + "||" + "&&" + "|" + "!" +] @keyword.operator + +;; Punctuation + +[ + "." + "," + ";" + ":" +] @punctuation.delimiter + +[ + "(" + ")" + "[" + "]" + "{" + "}" +] @punctuation.bracket + +;; Options + +(option) @attribute +(nounifoption) @attribute |