Commit d1b5042e authored by Martin Clochard's avatar Martin Clochard

byso: by/so in keyword lists

parent 6509617d
......@@ -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")) . font-lock-keyword-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" "by" "so")) . font-lock-keyword-face)
)
"Minimal highlighting for Why3 mode")
......
......@@ -158,6 +158,7 @@ on linking described in file LICENSE.
<context id="keywords" style-ref="meta-keyword">
<keyword>abstract</keyword>
<keyword>axiom</keyword>
<keyword>by</keyword>
<keyword>clone</keyword>
<keyword>coinductive</keyword>
<keyword>constant</keyword>
......@@ -175,6 +176,7 @@ on linking described in file LICENSE.
<keyword>namespace</keyword>
<keyword>predicate</keyword>
<keyword>private</keyword>
<keyword>so</keyword>
<keyword>theory</keyword>
<keyword>type</keyword>
<keyword>use</keyword>
......
......@@ -9,7 +9,7 @@ morekeywords=[1]{predicate,constant,function,goal,type,use,%
import,theory,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,%
rec,clone,if,then,else,result,old,ghost,by,so%
axiom,lemma,export,forall,exists,match,with,try,not,inductive,coinductive},%
%keywordstyle=[1]{\color{red}},%
morekeywords=[2]{true,false},%
......
......@@ -83,12 +83,12 @@ syn keyword whyModuleKeyword contained module
syn region whyNone matchgroup=whyKeyword start="\<\(axiom\|lemma\|goal\|prop\)\>" matchgroup=whyNone end="\<\w\(\w\|'\)*\>" contains=@whyAllErrs,whyComment
syn keyword whyKeyword as constant
syn keyword whyKeyword as by constant
syn keyword whyKeyword else epsilon exists
syn keyword whyKeyword forall function
syn keyword whyKeyword if in inductive coinductive
syn keyword whyKeyword let meta
syn keyword whyKeyword not predicate
syn keyword whyKeyword not predicate so
syn keyword whyKeyword then type with
syn keyword whyKeyword any
......
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