Commit 01715ba0 authored by Jean-Christophe Filliâtre's avatar Jean-Christophe Filliâtre
Browse files

syntax highlighting for reads/writes/raises

parent a8dcbbe1
......@@ -29,7 +29,7 @@
;; Note: comment font-lock is guaranteed by suitable syntax entries
;; '("(\\*\\([^*)]\\([^*]\\|\\*[^)]\\)*\\)?\\*)" . font-lock-comment-face)
'("{}\\|{[^|]\\([^}]*\\)}" . font-lock-type-face)
`(,(why-regexp-opt '("use" "clone" "namespace" "import" "export" "inductive" "external" "function" "predicate" "val" "exception" "axiom" "lemma" "goal" "type" "mutable" "model" "abstract")) . font-lock-builtin-face)
`(,(why-regexp-opt '("use" "clone" "namespace" "import" "export" "inductive" "external" "function" "predicate" "val" "exception" "axiom" "lemma" "goal" "type" "mutable" "model" "abstract" "reads" "writes" "raises")) . font-lock-builtin-face)
`(,(why-regexp-opt '("any" "match" "let" "rec" "in" "if" "then" "else" "begin" "end" "while" "invariant" "variant" "for" "to" "downto" "do" "done" "label" "loop" "assert" "absurd" "assume" "check" "ghost" "try" "with" "theory" "uses" "module")) . font-lock-keyword-face)
; `(,(why-regexp-opt '("unit" "bool" "int" "float" "prop" "array")) . font-lock-type-face)
)
......
......@@ -183,6 +183,9 @@ MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.
<keyword>variant</keyword>
<keyword>assert</keyword>
<keyword>while</keyword>
<keyword>reads</keyword>
<keyword>writes</keyword>
<keyword>raises</keyword>
<keyword>-&gt;</keyword>
</context>
<context id="types" style-ref="type">
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment