max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix: identifiers highlighting and literals

Browse source
This commit is contained in:
Leonardo de Moura 2020-11-23 18:32:39 -08:00
parent 0fc0bf0593
commit a44e51ce2e
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
doc/highlight.js
View file

@ -1136,14 +1136,14 @@ hljs.registerLanguage("lean", function(hljs) {
'have replace at suffices show from ' +
'congr congr_n congr_arg norm_num ring ',
literal:
'tt ff',
'true false',
meta:
'noncomputable|10 private protected mutual',
strong:
'sorry admit',
};
var LEAN_IDENT_RE = /[A-Za-z_][\\w\u207F-\u209C\u1D62-\u1D6A\u2079\']*/;
var LEAN_IDENT_RE = /[A-Za-z_][\\w\u207F-\u209C\u1D62-\u1D6A\u2079\'0-9]*/;
var DASH_COMMENT = hljs.COMMENT('--', '$');
var MULTI_LINE_COMMENT = hljs.COMMENT('/-[^-]', '-/');