Commit 58d66dfe authored by Guillaume Melquiond's avatar Guillaume Melquiond

Fix keywords for trywhy3.

parent 1c97f58f
......@@ -7,13 +7,22 @@ var TextHighlightRules = require("./text_highlight_rules").TextHighlightRules;
var Why3HighlightRules = function() {
var keywords = (
"abstract|axiom|by|clone|coinductive|constant|end|exception|" +
"export|function|goal|ghost|import|inductive|lemma|meta|mutable|" +
"module|namespace|predicate|private|so|theory|type|use|val|with|" +
"begin|do|done|downto|else|exists|for|forall|if|in|let|loop|match|" +
"raise|rec|then|to|try|while|absurd|assert|assume|diverges|ensures|" +
"check|invariant|raises|reads|requires|result|returns|self|variant|" +
"writes"
"as|axiom|by|clone|coinductive|constant|" +
"else|end|epsilon|exists|export|" +
"false|float|forall|function|" +
"goal|if|import|in|inductive|" +
"lemma|let|match|meta|not|predicate|" +
"range|scope|so|then|theory|true|type|use|with|" +
// programs
"abstract|any|at|" +
"begin|break|continue|do|done|downto|exception|" +
"for|fun|ghost|label|module|mutable|" +
"old|private|pure|raise|rec|return|" +
"to|try|val|while|" +
// specification
"absurd|alias|assert|assume|" +
"check|diverges|ensures|invariant|" +
"raises|reads|requires|returns|variant|writes"
);
var builtinConstants = ("true|false");
......@@ -78,10 +87,6 @@ var Why3HighlightRules = function() {
regex : '"',
next : "qstring"
},
{
token : "constant.numeric", // imaginary
regex : "(?:" + floatNumber + "|\\d+)[jJ]\\b"
},
{
token : "constant.numeric", // float
regex : floatNumber
......
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