From f6943d9c130db7a0145124af2db54fe2698762bf Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Fri, 20 Nov 2020 16:58:48 +0100 Subject: [PATCH] doc: fix highlighting of `#eval` etc. --- doc/highlight.js | 1 + 1 file changed, 1 insertion(+) diff --git a/doc/highlight.js b/doc/highlight.js index 583f2d065a..fcd4a66384 100644 --- a/doc/highlight.js +++ b/doc/highlight.js @@ -1104,6 +1104,7 @@ contains:b}}}()); // original from https://github.com/leanprover-community/highlightjs-lean/blob/master/src/lean.js, BSD 3, (c) 2020 Patrick Massot hljs.registerLanguage("lean", function(hljs) { var LEAN_KEYWORDS = { + $pattern: /#?\w+/, keyword: 'theorem|10 lemma|10 definition def class structure instance ' + 'example inductive coinductive ' +