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