%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