Syntax Highlighting for Java+JML

javajml.sublime-syntax

%YAML 1.2
---

name: JavaJml
file_extensions:
  - java
  - jml
scope: source.java

contexts:
  main:
    - match: ""
      push: "Packages/Java.sublime-syntax"
      with_prototype:
        - match: '//@'
          push: jmlSingle
        - match: '/\*@'
          push: jmlMulti
  jmlMulti:
    - meta_scope: comment
    - match: '\*/'
      pop: true
    - include: jml
      
  jmlSingle:
    - match: '$'
      pop: true
    - include: jml

  jml:
    - match: '\b(boolean|byte|int|long|short|void)\b'
      scope: storage.type.primitive.java

      #modifiers
    - match: '\b(public|private|protected|pure|nullable|null_by_default|ghost|model|helper|non_null|nullable|\\bigint|\\real)\b'
      scope: keyword.modifier

    - match: '\b(false|true)\b'
      scope: literal.boolean

    - match: '\b(instanceof|new|null|super|this)\b'
      scope: keyword

    #clauses
    - match: '\b(accessible|assignable|breaks|continues|decreases|depends|ensures|ensures_free|loop_determines|represents|requires|requires_free|signals|signals_only|loop_invariant)\b'
      scope: keyword.control

    - match: '\((\\(forall|exists|num_of|sum|bsum|infinite_union))'
      captures:
        1: keyword
      
    - match: '\b(\\duration|\\elemtype|\\empty|\\everything|\\exception|\\exists|\\forall|\\fresh|\\index|\\into|\\invariant_for|\\is_initialized|\\lblneg||\\lblpos|\\lockset|\\max|\\measured_by|\\min|\\nonnullelements|\\nothing|\\not_assigned|\\not_modified|\\not_specified|\\num_of|\\old|\\permission|\\pre|\product|\\reach|\\result|\\same|\\space|\\subset|\\such_that|\\sum|\\TYPE|\\typeof|\\type|\\values|\\working_space)\b'
      scope: keyword
      

    - match: '\b(\\all_fields \\all_objects|\\backup|\\bsum|\\by|\\declassifies|\\disjoint| \\domain_implies_created|determines|model_method_axiom|\\erases|\\free|\\seq_indexOf|\\intersect|\\inv|\\in_domain|\\is_finite|\\itself|\\locset|\\map|\\map_empty|\\map_get|\\map_override|\\map_remove|\\map_singleton|\\map_size|\\map_update|\\new_elems_fresh|\\new_objects|\\reachLocs|\\seq|\\seq_2_map|\\seq_concat|\\seq_def|\\seq_empty|\\seq_get|\\seq_put|\\seq_reverse|\\seq_singleton|\\seq_sub|\\set_minus|\\singleton|\\static_invariant_for|\\strictly_nothing|\\string_equal|returns|join_proc|separates|\\set_union|\\infinite_union|\\transactionUpdated|\\transient)\b'
      scope: keyword

    - match: '\b(\\dl_\w+)\b'
      scope: keyword.entity.name.key