summaryrefslogtreecommitdiff
path: root/isabelle.sublime-syntax
diff options
context:
space:
mode:
authorstuebinm2021-09-04 14:52:56 +0200
committerstuebinm2021-09-04 14:52:56 +0200
commit69d6d0b95a232d47b0e3eca06e5b8da6d0d7c64c (patch)
treee77a13669140d725abaa304f61e6a16467f3cae9 /isabelle.sublime-syntax
parentb469f8b1e360f1169e9a2d4e6de382c63502c72b (diff)
basic sublime text highlighter syntax (for bat)
This is mostly based on the syntax generated by `isabelle vscode_grammar` for the list of keywords; choice of scopes is heavily biased by my understanding of the subset of isabelle syntax I actually know about. For now, it makes no attempt to actually understand anything of what is going on in a file (except for strings/comments) and simply matches keywords. Note that scope selection does not make sense, and is mostly based on looking into which scopes are assigned useful colours by common highlighter themes (mostly bat's default theme and TwoDark for now)
Diffstat (limited to 'isabelle.sublime-syntax')
-rw-r--r--isabelle.sublime-syntax47
1 files changed, 47 insertions, 0 deletions
diff --git a/isabelle.sublime-syntax b/isabelle.sublime-syntax
new file mode 100644
index 0000000..f7beb6e
--- /dev/null
+++ b/isabelle.sublime-syntax
@@ -0,0 +1,47 @@
+%YAML 1.2
+---
+
+name: Isabelle
+file_extensions:
+ - thy
+scope: source.isabelle
+
+contexts:
+ main:
+ - match: \b(theory|imports|begin|end|ML|ML_command|ML_export|ML_file|ML_file_debug|ML_prf|ML_val|Roots_file|SML_export|alias|attribute_setup|back|bibtex_file|bnf|bundle|class|class_deps|codatatype|code_datatype|code_deps|code_identifier|code_monad|code_pred|code_printing|code_reflect|code_reserved|code_thms|coinductive|coinductive_set|compile_generated_files|consts|context|copy_bnf|declaration|declare|default_sort|defer|experiment|export_code|export_generated_files|external_file|extract|extract_type|find_consts|find_theorems|find_unused_assms|free_constructors|full_prf|fun_cases|generate_file|guess|help|hide_class|hide_const|hide_fact|hide_type|include|including|inductive|inductive_cases|inductive_set|inductive_simps|lift_bnf|lift_definition|lifting_forget|lifting_update|local_setup|locale_deps|method_setup|named_theorems|nitpick|nitpick_params|no_notation|no_syntax|no_translations|no_type_notation|nonterminal|notation|notepad|nunchaku|nunchaku_params|old_rep_datatype|oops|oracle|overloading|parse_ast_translation|parse_translation|prefer|prf|primcorec|primcorecursive|primrec|print_ML_antiquotations|print_abbrevs|print_antiquotations|print_ast_translation|print_attributes|print_bnfs|print_bundles|print_case_translations|print_cases|print_claset|print_classes|print_codeproc|print_codesetup|print_coercions|print_commands|print_context|print_definitions|print_defn_rules|print_facts|print_induct_rules|print_inductives|print_interps|print_locale|print_locales|print_methods|print_options|print_orders|print_quot_maps|print_quotconsts|print_quotients|print_quotientsQ3|print_quotmapsQ3|print_record|print_rules|print_simpset|print_state|print_statement|print_syntax|print_term_bindings|print_theorems|print_theory|print_trans_rules|print_translation|quickcheck|quickcheck_generator|quickcheck_params|quotient_definition|quotient_type|realizability|realizers|record|schematic_goal|session|setup|setup_lifting|simproc_setup|sledgehammer|sledgehammer_params|smt_status|solve_direct|sorry|specification|subclass|subgoal|supply|syntax|syntax_declaration|thm|thm_deps|thm_oracles|thy_deps|translations|try|try0|txt|typ|type_alias|type_notation|type_synonym|typed_print_translation|unbundle|unused_thms|value|values|welcome|write|abbrevs|begin|binder|checking|class_instance|class_relation|code_module|constant|constrains|datatypes|description|directories|document_files|document_theories|export_files|export_prefix|external_files|file|file_prefix|functions|global|includes|infix|infixl|infixr|keywords|module_name|monos|morphisms|notes|open|opening|options|output|overloaded|parametric|pervasive|premises|private|qualified|rewrites|sessions|structure|theories|type_class|type_constructor|unchecked|when|where)\b
+ scope: entity.name.class.isabelle
+ comment: things that don't easily fit elsewhere (taken from the vscode grammar)
+ - match: \b(chapter|note|paragraph|section|subparagraph|subsection|subsubsection|text|text_raw)\b
+ # TODO: better scope for this, TwoDark prints this the same as keyword.source
+ scope: keyword.name.struct.isabelle
+ - match: \b(lemma|definition|theorem|corollary|abbreviation|assumes|shows|and|fixes|obtains|also|axiomatization|judgement|lemmas|proposition|prop|term|termination|is|obtains)\b
+ scope: keyword.source.isabelle
+ comment: reserved words used to structure theorems, statements, etc.
+ - match: \b(proof|qed|then|thus|have|hence|moreover|finally|ultimately|using|unfolding|by|apply|apply_end|done|assume|with|show|fix|from|obtain|next|case|consider|define|presume)\b
+ scope: entity.name.tag.isabelle
+ comment: reserved words used in proofs
+ - match: \b(fun|function|functor|datatype|datatype_compat|global_interpretation|instance|instantiation|interpret|interpretation|let|locale|partial_function|sublocale|typedec|typedef|if|in)\b
+ scope: support.function.isabelle
+ comment: reserved words used in isabelle's functional language
+ - match: '\b[0-9]+\b'
+ scope: constant.numeric.isabelle
+ comment: numeric constants
+ - match: '"(\\"|[^"])*"'
+ scope: string.isabelle
+ comment: normal strings enclosed by quotes
+ - match: \(\*
+ comment: block comments
+ push:
+ - meta_scope: comment.block.isabelle
+ - match: "(\bTODO|(.)+:)"
+ scope: constant.numeric.isabelle
+ comment: useful for e.g. the top info comment of AFP entries
+ - match: \*\)
+ pop: true
+ # TODO: assign this a different colour
+ - match: "\\\\<open>|‹"
+ comment: Cartouches, i.e. strings enclosed in ‹›
+ push:
+ - meta_scope: string.quoted.other.multiline.isabelle
+ - match: "\\\\<close>|›"
+ pop: true