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

syntax highlighting in Emacs and GTKsourceview

parent 0053e3da
...@@ -29,8 +29,8 @@ ...@@ -29,8 +29,8 @@
;; Note: comment font-lock is guaranteed by suitable syntax entries ;; Note: comment font-lock is guaranteed by suitable syntax entries
;; '("(\\*\\([^*)]\\([^*]\\|\\*[^)]\\)*\\)?\\*)" . font-lock-comment-face) ;; '("(\\*\\([^*)]\\([^*]\\|\\*[^)]\\)*\\)?\\*)" . font-lock-comment-face)
'("{}\\|{[^|]\\([^}]*\\)}" . font-lock-type-face) '("{}\\|{[^|]\\([^}]*\\)}" . font-lock-type-face)
`(,(why-regexp-opt '("use" "clone" "namespace" "import" "export" "inductive" "external" "logic" "parameter" "exception" "axiom" "lemma" "goal" "type" "mutable" "model" "abstract")) . font-lock-builtin-face) `(,(why-regexp-opt '("use" "clone" "namespace" "import" "export" "inductive" "external" "function" "predicate" "parameter" "exception" "axiom" "lemma" "goal" "type" "mutable" "model" "abstract")) . font-lock-builtin-face)
`(,(why-regexp-opt '("and" "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 '("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) ; `(,(why-regexp-opt '("unit" "bool" "int" "float" "prop" "array")) . font-lock-type-face)
) )
"Minimal highlighting for Why mode") "Minimal highlighting for Why mode")
......
...@@ -152,7 +152,8 @@ MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. ...@@ -152,7 +152,8 @@ MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.
<keyword>import</keyword> <keyword>import</keyword>
<keyword>export</keyword> <keyword>export</keyword>
<keyword>inductive</keyword> <keyword>inductive</keyword>
<keyword>logic</keyword> <keyword>function</keyword>
<keyword>predicate</keyword>
<keyword>axiom</keyword> <keyword>axiom</keyword>
<keyword>lemma</keyword> <keyword>lemma</keyword>
<keyword>goal</keyword> <keyword>goal</keyword>
...@@ -165,6 +166,7 @@ MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. ...@@ -165,6 +166,7 @@ MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.
<context id="meta-words" style-ref="keyword"> <context id="meta-words" style-ref="keyword">
<keyword>match</keyword> <keyword>match</keyword>
<keyword>let</keyword> <keyword>let</keyword>
<keyword>rec</keyword>
<keyword>in</keyword> <keyword>in</keyword>
<keyword>if</keyword> <keyword>if</keyword>
<keyword>then</keyword> <keyword>then</keyword>
......
module MutualRec
use import int.Int
let rec f (x1 x2: int) : int variant { x1+x2 } =
{ x1 >= 0 && x2 >= 0 } if x1 <= 1 then 0 else g (x1-1) x2 { result = 0 }
with g (y1: int) variant { y1 } =
{ y1 >= 0 }
f (y1-1)
{ 0 = 0 }
end
module PoorArrays module PoorArrays
use import int.Int use import int.Int
...@@ -14,7 +28,7 @@ module PoorArrays ...@@ -14,7 +28,7 @@ module PoorArrays
parameter set (a: array 'a) (i: int) (v: 'a) : parameter set (a: array 'a) (i: int) (v: 'a) :
{ 0 <= i < length !a } { 0 <= i < length !a }
unit writes a unit writes a
{ !a.length = !(old a).length and !a.elts = M.set !(old a).elts i v } { !a.length = !(old a).length && !a.elts = M.set !(old a).elts i v }
end end
......
Supports Markdown
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