emacs/latex: added keywords

parent 9ef61cea
......@@ -29,7 +29,7 @@
'("(\\*\\([^*)]\\([^*]\\|\\*[^)]\\)*\\)?\\*)" . font-lock-comment-face)
; '("{}\\|{[^|]\\([^}]*\\)}" . font-lock-type-face)
`(,(why3-regexp-opt '("invariant" "variant" "diverges" "requires" "ensures" "returns" "raises" "reads" "writes" "assert" "assume" "check")) . font-lock-type-face)
`(,(why3-regexp-opt '("use" "clone" "namespace" "import" "export" "coinductive" "inductive" "external" "constant" "function" "predicate" "val" "exception" "axiom" "lemma" "goal" "type" "mutable" "model" "abstract" "private" "any" "match" "let" "rec" "in" "if" "then" "else" "begin" "end" "while" "for" "to" "downto" "do" "done" "loop" "absurd" "ghost" "raise" "try" "with" "theory" "uses" "module" "converter" "fun" "at" "old" "true" "false" "forall" "exists" "label")) . font-lock-keyword-face)
`(,(why3-regexp-opt '("use" "clone" "scope" "import" "export" "coinductive" "inductive" "external" "constant" "function" "predicate" "val" "exception" "axiom" "lemma" "goal" "type" "mutable" "model" "abstract" "private" "any" "match" "let" "rec" "in" "if" "then" "else" "begin" "end" "while" "for" "to" "downto" "do" "done" "loop" "absurd" "ghost" "raise" "try" "with" "theory" "uses" "module" "converter" "fun" "at" "old" "true" "false" "forall" "exists" "label")) . font-lock-keyword-face)
)
"Minimal highlighting for Why3 mode")
......
......@@ -5,8 +5,8 @@
\lstdefinelanguage{why3}
{
basicstyle=\ttfamily,
morekeywords=[1]{predicate,constant,function,goal,type,use,%
import,theory,end,in,%
morekeywords=[1]{predicate,constant,fun,function,goal,type,use,%
import,theory,scope,end,in,%
mutable,invariant,model,requires,ensures,raises,returns,reads,writes,diverges,%
variant,let,val,while,for,loop,abstract,private,any,assert,assume,check,%
rec,clone,if,then,else,result,old,ghost,%
......
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