Skip to content

Instantly share code, notes, and snippets.

@maxvonhippel
Created December 7, 2020 21:53
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
Star You must be signed in to star a gist
Save maxvonhippel/fde4e129ef5b1baf1653c34e81c652e2 to your computer and use it in GitHub Desktop.
Practical Verification System (PVS) Sublime Text Syntax Highlighting
%YAML 1.2
---
# See http://www.sublimetext.com/docs/3/syntax.html
file_extensions:
- pvs
scope: source.pvs
contexts:
# The prototype context is prepended to all contexts but those setting
# meta_include_prototype: false.
prototype:
- include: comments
- include: match-operators
main:
# The main context is the initial starting point of our syntax.
# Include other contexts from here (or specify them directly).
- include: keywords
- include: numbers
- include: strings
keywords:
# http://pvs.csl.sri.com/doc/pvs-language-reference.pdf
- match: '\b(CODATATYPE|ENDTABLE|JUDGEMENT|SUBLEMMA|CLOSURE|ENDIF|INDUCTIVE|RECURSIVE|CHALLENGE|ENDCASES|IMPORTING|POSTULATE|CLAIM|ENDCOND|IN|PROPOSITION|BY|END|IFF|OR|WITH|CASES|ENDASSUMING|IMPLIES|ORELSE|XOR|BEGIN|ELSE|HAS_TYPE|OBLIGATION|WHEN|BUT|ELSIF|IF|OF|WHERE|AUTO_REWRITE\-|COROLLARY|FUNCTION|NOT|TYPE\+|AXIOM|DATATYPE|GHOST|O|VAR|AUTO_REWRITE\+|CORECURSIVE|FROM|NONEMPTY_TYPE|TYPE|AUTO_REWRITE|CONVERSION\-|FORMULA|MEASURE|TRUE|ASSUMPTION|CONVERSION\+|FORALL|MACRO|THEORY|ASSUMING|CONVERSION|FALSE|LIBRARY|THEOREM|AS|CONTAINING|FACT|LET|THEN|LAW|SUBTYPE_OF|ARRAY|EXPRESSION|LEMMA|TABLEANDTHEN|COND|EXPORTING|CONJECTURE|AND|COINDUCTIVE|EXISTS|LAMBDA|SUBTYPES)\b'
scope: keyword.control.pvs
match-operators: [
{match: '=', scope: keyword.operator.pvs},
{match: '->', scope: keyword.operator.pvs},
{match: ':', scope: keyword.operator.pvs}]
numbers:
- match: '\b(-)?[0-9.]+\b'
scope: constant.numeric.pvs
strings:
# Strings begin and end with quotes, and use backslashes as an escape
# character.
- match: '"'
scope: punctuation.definition.string.begin.pvs
push: inside_string
inside_string:
- meta_include_prototype: false
- meta_scope: string.quoted.double.pvs
- match: '\.'
scope: constant.character.escape.pvs
- match: '"'
scope: punctuation.definition.string.end.pvs
pop: true
comments:
- match: '%'
scope: punctuation.definition.comment.pvs
push:
# This is an anonymous context push for brevity.
- meta_scope: comment.line.double-slash.pvs
- match: $\n?
pop: true
@maxvonhippel
Copy link
Author

I don't know anything about making Sublime text syntax definitions so this is kind of garbage, but it makes the code at least a bit readable.

Any improvements welcome!

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment