diff options
| -rw-r--r-- | isabelle.sublime-syntax | 47 |
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 |