Add syntax highlighting for juvix code blocks in docs (#1971)

This PR adds initial syntax highlighting for juvix code blocks and REPL
sessions in Markdown files rendered by mdbook. After this PR, only two
themes would be supported to ease maintenance: Light and Dark (Ayu).

The implementation is a specifically tailored version of

- https://github.com/anoma/highlightjs-juvix (plugin for
HighlightJS,v11.7).

to be compatible with the infamous HighlightJS 10.1.1, to be used just
for MdBook.

The output can be seen here (make sure the CI finished to check the last
version, otherwise run the website locally):

- https://jonaprieto.github.io/juvix/tutorials/learn.html

.gitignore

@@ -88,3 +88,4 @@ examples/milestone/HelloWorld/HelloWorld
 hie.yaml
 /.shake/
 /.benchmark-results/
+docs/assets/**

Makefile

@@ -74,6 +74,7 @@ demo-example:
 .PHONY: docs
 docs:
 	@cp $(METAFILES) docs/
+	@cp -r assets/ docs/
 	@mdbook build
 
 .PHONY: serve-docs

book.toml

@@ -28,8 +28,8 @@ macros = "theme/latex-macros.txt"
 default-theme = "light"
 preferred-dark-theme = "Ayu"
 copy-fonts = true
-additional-css = ["theme/pagetoc.css"]
-additional-js = ["theme/pagetoc.js","assets/images/tara-magicien.png", "assets/images/tara-seating.svg", "assets/images/tara-smiling.png", "assets/images/tara-smiling.svg", "assets/images/tara-teaching.png", "assets/images/tara-teaching.svg", "assets/js/highlight.js", "assets/js/tex-chtml.js" ]
+additional-css = ["theme/pagetoc.css", "theme/juvix.css"]
+additional-js = ["theme/pagetoc.js", "theme/juvix.js", "theme/pascal.js"]
 no-section-label = false
 git-repository-url = "https://github.com/anoma/juvix"
 git-repository-icon = "fa-github"

docs/reference/language/axioms.md

@@ -5,11 +5,12 @@ example, let us imagine one wants to write a program that assumes _A_ is
 a type, and there exists a term _x_ that inhabits _A_. Then the program
 would look like the following.
 
-    -- Example.juvix
+```juvix
     module Example;
      axiom A : Type;
      axiom x : A;
     end;
+```
 
 Terms introduced by the `axiom` keyword lack any computational content.
 Programs containing axioms not marked as builtins cannot be compiled to

docs/reference/language/comments.md

@@ -5,15 +5,14 @@ Juvix has no support for nested comments.
 
 - Inline Comment
 
-<!-- -->
-
+```juvix
     -- This is a comment!
+```
 
 - Region comment
 
-<!-- -->
-
+```juvix
     {-
         This is a comment!
-
     -}
+```

docs/reference/language/modules.md

@@ -60,6 +60,7 @@ module B;
     open A;
     x : Nat;
     x := zero;
+end;
 ```
 
 However, opening modules may create name collisions if you already have

docs/tutorials/learn.md

@@ -27,7 +27,7 @@ juvix repl
 
 The response should be similar to:
 
-```juvix
+```jrepl
 Juvix REPL version 0.3: https://juvix.org. Run :help for help
 OK loaded: ./.juvix-build/stdlib/Stdlib/Prelude.juvix
 Stdlib.Prelude>
@@ -41,7 +41,7 @@ commands type `:help`.
 
 You can try evaluating simple arithmetic expressions in the REPL:
 
-```juvix
+```jrepl
 Stdlib.Prelude> 3 + 4
 7
 Stdlib.Prelude> 1 + 3 * 7
@@ -62,7 +62,7 @@ natural number from a smaller one yields `0`.
 
 You can also try boolean expressions
 
-```juvix
+```jrepl
 Stdlib.Prelude> true
 true
 Stdlib.Prelude> not true
@@ -77,7 +77,7 @@ Stdlib.Prelude> if true 1 0
 
 and strings, pairs and lists:
 
-```juvix
+```jrepl
 Stdlib.Prelude> "Hello world!"
 "Hello world!"
 Stdlib.Prelude> (1, 2)
@@ -91,7 +91,7 @@ In fact, you can use all functions and types from the
 module of the [standard library](https://anoma.github.io/juvix-stdlib),
 which is preloaded by default.
 
-```juvix
+```jrepl
 Stdlib.Prelude> length (1 :: 2 :: nil)
 3
 Stdlib.Prelude> null (1 :: 2 :: nil)
@@ -136,7 +136,7 @@ evaluating `main`.
 
 To see the type of an expression, use the `:type` REPL command:
 
-```juvix
+```jrepl
 Stdlib.Prelude> :type 1
 Nat
 Stdlib.Prelude> :type true
@@ -300,7 +300,7 @@ It is not necessary to define a separate function to perform pattern
 matching. One can use the `case` syntax to pattern match an expression
 directly.
 
-```juvix
+```jrepl
 Stdlib.Prelude> case (1, 2) | (suc _, zero) := 0 | (suc _, suc x) := x | _ := 19
 1
 ```
@@ -365,7 +365,7 @@ even :=
     odd' zero := false;
     odd' (suc n) := even' n;
   in
-  even'
+  even';
 ```
 
 The functions `even'` and `odd'` are not visible outside `even`.
@@ -569,13 +569,16 @@ This is not acceptable if you care about performance. In an imperative
 language, one would use a simple loop going over the list without any
 memory allocation. In pseudocode:
 
-```juvix
-var sum : Nat := 0;
-while (lst /= nnil) {
+```pascal
+sum : Nat := 0;
+
+while (lst /= nil) do
+begin
   sum := sum + head lst;
   lst := tail lst;
-};
-return sum;
+end;
+
+result := sum;
 ```
 
 Fortunately, it is possible to rewrite this function to use _tail
@@ -613,16 +616,19 @@ imperative pseudocode for computing the nth Fibonacci number in linear
 time. The variables `cur` and `next` hold the last two computed
 Fibonacci numbers.
 
-```juvix
-var cur : Nat := 0;
-var next : Nat := 1;
-while (n /= 0) {
-  var tmp := next;
+```pascal
+cur : Nat := 0;
+next : Nat := 1;
+
+while (n /= 0) do
+begin
+  tmp := next;
   next := cur + next;
   cur := tmp;
   n := n - 1;
-};
-return cur;
+end;
+
+result := cur;
 ```
 
 An equivalent functional program is:
@@ -776,7 +782,7 @@ and the [Juvix program examples](../reference/examples.md).
     Analogously to the `map` function for lists, define a function
 
     ```juvix
-    tmap : (Nat -> Nat) -> Tree -> Tree
+    tmap : (Nat -> Nat) -> Tree -> Tree;
     ```
 
     which applies a function to all natural numbers stored in a tree.

theme/index.hbs

@@ -125,10 +125,8 @@
                         </button>
                         <ul id="theme-list" class="theme-popup" aria-label="Themes" role="menu">
                             <li role="none"><button role="menuitem" class="theme" id="light">Light</button></li>
-                            <li role="none"><button role="menuitem" class="theme" id="rust">Rust</button></li>
-                            <li role="none"><button role="menuitem" class="theme" id="coal">Coal</button></li>
-                            <li role="none"><button role="menuitem" class="theme" id="navy">Navy</button></li>
-                            <li role="none"><button role="menuitem" class="theme" id="ayu">Ayu</button></li>
+                            <li role="none"><button role="menuitem" class="theme theme-selected" id="ayu">Dark</button></li>
+
                         </ul>
                         {{#if search_enabled}}
                         <button id="search-toggle" class="icon-button" type="button" title="Search. (Shortkey: s)" aria-label="Toggle Searchbar" aria-expanded="false" aria-keyshortcuts="S" aria-controls="searchbar">
@@ -287,6 +285,14 @@
 
         <script src="{{ path_to_root }}clipboard.min.js"></script>
         <script src="{{ path_to_root }}highlight.js"></script>
+        <script src="{{ path_to_root }}theme/juvix.js"></script>
+        <script src="{{ path_to_root }}theme/pascal.js"></script>
+        <script >
+            hljs.registerLanguage('juvix', hljsDefineJuvix);
+            hljs.registerLanguage('jrepl', hljsDefineJuvixRepl);
+            hljs.registerLanguage('pascal', hljsDefinePascal);
+        </script>
+
         <script src="{{ path_to_root }}book.js"></script>
 
         <!-- Custom JS scripts -->

theme/juvix.css

@@ -0,0 +1,27 @@
+.hljs-meta {
+  color: coral;
+}
+
+.hljs-inductive {
+  color: #86b300;
+}
+
+.hljs-number {
+  color: #00a822;
+}
+
+.hljs-function {
+  color: #d78810;
+}
+
+.hljs-symbol {
+  color: #d78810;
+}
+
+.hljs-string {
+  color: #f07171;
+}
+
+.hljs-keyword {
+  color: #399ee6;
+}

theme/juvix.js

@@ -0,0 +1,338 @@
+/*
+The following is specifically tailored for compatibility with HighlightJS
+10.1.1, which is used in MdBook. Support for the latest version of HighlightJS,
+v11.7, can be found at the following repository:
+https://github.com/anoma/highlightjs-juvix
+*/
+
+var module = module ? module : {}; // shim for browser use
+
+const MATCH_NOTHING_RE = /$^/; // to force a mode to never match
+
+const INLINE_COMMENT = {
+  className: "comment",
+  begin: /--/,
+  end: /$/,
+};
+
+const BLOCK_COMMENT = {
+  className: "comment",
+  begin: /\{-/,
+  end: /-\}/,
+  relevance: 1,
+};
+
+const COMMENT = {
+  scope: "comment",
+  contains: ["self"],
+  variants: [INLINE_COMMENT, BLOCK_COMMENT],
+};
+
+const STRINGS = {
+  className: "string",
+  variants: [hljs.QUOTE_STRING_MODE],
+};
+
+const NUMBERS = hljs.C_NUMBER_MODE;
+
+const RESERVED_SYMBOLS = {
+  className: "keyword",
+  begin:
+    /(@|:=|->|→|↦|;|\||\{|\}|\\|λ|\s:\s|\_|Type|\slet\s|\sin\s|terminating|positive|axiom|builtin|open|end)/,
+  endsSameBegin: true,
+};
+
+const OTHER_SYMBOLS_AND_OPERATORS = [
+  {
+    className: "operator",
+    begin: /(\*|\|\||&&|==|>>|=?>|<=?|-\s|\+)/,
+    endsSameBegin: true,
+  },
+  { className: "punctuation", begin: /(\(|\))/, endsSameBegin: true },
+  { begin: /::/, endsSameBegin: true },
+  // an issue of this hljs version is that some keywords are not highlighted
+  // even though they are in the keywords list. This is a workaround
+  { className: "literal", begin: /(true|false)/, endsSameBegin: true },
+  { className: "built_in", begin: /(trace|IO|if|case)/, endsSameBegin: true },
+];
+
+const MODULE_NAME_RE = /[a-zA-Z][a-zA-Z0-9_]*(\.[a-zA-Z][a-zA-Z0-9_]*)*/;
+const IDEN_RE = /[^(\s|;|\{|\}|\(|\)|@)]+/;
+//some symbols may brake the use of this
+
+function hljsDefineJuvix(hljs) {
+  const JUVIX_KEYWORDS = {
+    keyword: "let in print terminating positive axiom builtin open end",
+    built_in: "trace IO if case",
+    literal: "true false",
+  };
+
+  const MODULE_BEGIN = {
+    className: "keyword",
+    begin: /module/,
+    end: /;/,
+    contains: [
+      BLOCK_COMMENT,
+      {
+        className: "title",
+        begin: MODULE_NAME_RE,
+        endsParent: true,
+        contains: [BLOCK_COMMENT],
+      },
+    ],
+  };
+
+  const PUBLIC = {
+    className: "keyword",
+    begin: /public/,
+    end: /;/,
+    endsParent: true,
+    contains: [COMMENT],
+  };
+
+  const MODULE_END = {
+    className: "keyword",
+    begin: /end/,
+    end: /;/,
+    contains: [COMMENT],
+  };
+
+  const INFIX = {
+    className: "keyword",
+    begin: /((infix(l|r)?)|postfix)/,
+    end: MATCH_NOTHING_RE,
+    contains: [
+      COMMENT,
+      {
+        className: "number",
+        begin: /\d+/,
+        end: MATCH_NOTHING_RE,
+        endsParent: true,
+        contains: [
+          COMMENT,
+          {
+            className: "operator",
+            begin: IDEN_RE,
+            end: MATCH_NOTHING_RE,
+            endsParent: true,
+            contains: [
+              COMMENT,
+              {
+                className: "keyword",
+                begin: /;/,
+                endsSameBegin: true,
+                endsParent: true,
+              },
+            ],
+          },
+        ],
+      },
+    ],
+  };
+
+  const IMPORT = {
+    className: "keyword",
+    begin: /(((open )?import)|(open( import)?))/,
+    end: MATCH_NOTHING_RE,
+    // endsParent: true,
+    contains: [
+      COMMENT,
+      {
+        className: "title",
+        begin: MODULE_NAME_RE,
+        end: MATCH_NOTHING_RE,
+        endsParent: true,
+        contains: [
+          COMMENT,
+          PUBLIC,
+          {
+            className: "keyword",
+            begin: /;/,
+            endsParent: true,
+          },
+          {
+            className: "keyword",
+            begin: /(hiding|using)/,
+            end: MATCH_NOTHING_RE,
+            contains: [
+              COMMENT,
+              {
+                className: "keyword",
+                begin: /\{/,
+                end: /\}/,
+                endsParent: true,
+                contains: [
+                  COMMENT,
+                  {
+                    className: "symbol",
+                    begin: IDEN_RE,
+                    contains: [COMMENT, PUBLIC],
+                  },
+                ],
+              },
+            ],
+          },
+        ],
+      },
+    ],
+  };
+
+  const INDUCTIVE = {
+    className: "inductive",
+    begin: /type/,
+    end: MATCH_NOTHING_RE,
+    keywords: "type",
+    contains: [
+      COMMENT,
+      {
+        className: "keyword",
+        begin: /;/,
+        endsParent: true,
+      },
+      {
+        // className: "symbol",
+        begin: IDEN_RE,
+        end: MATCH_NOTHING_RE,
+        endsParent: true,
+        contains: [
+          COMMENT,
+          RESERVED_SYMBOLS,
+          {
+            //  ( A : Type )
+            begin: /\(/,
+            end: /\)/,
+            contains: [
+              COMMENT,
+              {
+                // className: "symbol",
+                begin: IDEN_RE,
+                end: MATCH_NOTHING_RE,
+                endsParent: true,
+                contains: [
+                  COMMENT,
+                  {
+                    // type annotation
+                    className: "keyword",
+                    begin: /:/,
+                    end: /Type/,
+                    endsParent: true,
+                  },
+                ],
+              },
+            ],
+          },
+        ],
+      },
+    ],
+  };
+
+  var OPTS = [
+    COMMENT,
+    RESERVED_SYMBOLS,
+    MODULE_BEGIN,
+    MODULE_END,
+    IMPORT,
+    INFIX,
+    INDUCTIVE,
+    NUMBERS,
+    STRINGS,
+  ];
+
+  return {
+    name: "Juvix",
+    aliases: ["juvix"],
+    keywords: JUVIX_KEYWORDS,
+    contains: OPTS.concat({
+      begin: /(?=[^(\s|;|\{|\}|\(|\)|@)]+\s*:)/,
+      end: MATCH_NOTHING_RE,
+      endsSameBegin: true,
+      contains: [
+        {
+          className: "function",
+          begin: /^\s*[^(\s|;|\{|\}|\(|\)|@)]+(?=\s*:\s+.*;)/,
+          end: MATCH_NOTHING_RE,
+          contains: [
+            COMMENT,
+            {
+              className: "keyword",
+              begin: /:\s+/,
+              endsSameBegin: true,
+              endsParent: true,
+            },
+            {
+              className: "keyword",
+              begin: /;/,
+              endsSameBegin: true,
+              endsParent: true,
+            },
+          ],
+        },
+        {
+          className: "keyword",
+          begin: /;/,
+          endsSameBegin: true,
+          endsParent: true,
+        },
+      ]
+        .concat(OPTS)
+        .concat([OTHER_SYMBOLS_AND_OPERATORS]),
+    }),
+  };
+}
+
+function hljsDefineJuvixRepl(hljs) {
+  return {
+    name: "Juvix REPL",
+    aliases: ["jrepl"],
+    case_insensitive: false,
+    unicodeRegex: true,
+    contains: [
+      {
+        className: "meta",
+        begin: /^(Juvix REPL|OK)/,
+        end: /$/,
+      },
+      {
+        begin: /^(?=([a-zA-Z][a-zA-Z0-9_]*(\.[a-zA-Z][a-zA-Z0-9_]*))?>)/,
+        end: /$/,
+        contains: [
+          {
+            className: "meta",
+            begin: /([a-zA-Z][a-zA-Z0-9_]*(\.[a-zA-Z][a-zA-Z0-9_]*))?>\s+/,
+            endsSameBegin: true,
+          },
+          {
+            className: "keyword",
+            begin: /:[a-z]+/,
+            endsWithParent: true,
+            contains: [
+              {
+                subLanguage: "juvix",
+                endsWithParent: true,
+              },
+            ],
+          },
+          {
+            subLanguage: "juvix",
+            endsWithParent: true,
+          },
+        ],
+      },
+      {
+        begin: /^/,
+        end: /$/,
+        contains: [
+          {
+            subLanguage: "juvix",
+            endsWithParent: true,
+          },
+        ],
+      },
+    ],
+  };
+}
+
+module.exports = function (hljs) {
+  hljs.registerLanguage("juvix", hljsDefineJuvix);
+  hljs.registerLanguage("jrepl", hljsDefineJuvixRepl);
+};

theme/pascal.js

@@ -0,0 +1,83 @@
+// To be used with highlight.js v10.1.1
+function hljsDefinePascal(e) {
+  var a =
+      "exports register file shl array record property for mod while set ally label uses raise not stored class safecall var interface or private static exit index inherited to else stdcall override shr asm far resourcestring finalization packed virtual out and protected library do xorwrite goto near function end div overload object unit begin string on inline repeat until destructor write message program with read initialization except default nil if case cdecl in downto threadvar of try pascal const external constructor type public then implementation finally published procedure absolute reintroduce operator as is abstract alias assembler bitpacked break continue cppdecl cvar enumerator experimental platform deprecated unimplemented dynamic export far16 forward generic helper implements interrupt iochecks local name nodefault noreturn nostackframe oldfpccall otherwise saveregisters softfloat specialize strict unaligned varargs ",
+    r = [
+      e.C_LINE_COMMENT_MODE,
+      e.COMMENT(/\{/, /\}/, { relevance: 0 }),
+      e.COMMENT(/\(\*/, /\*\)/, { relevance: 10 }),
+    ],
+    n = {
+      className: "meta",
+      variants: [
+        { begin: /\{\$/, end: /\}/ },
+        { begin: /\(\*\$/, end: /\*\)/ },
+      ],
+    },
+    t = {
+      className: "string",
+      begin: /'/,
+      end: /'/,
+      contains: [{ begin: /''/ }],
+    },
+    s = { className: "string", begin: /(#\d+)+/ },
+    i = {
+      begin: e.IDENT_RE + "\\s*=\\s*class\\s*\\(",
+      returnBegin: !0,
+      contains: [e.TITLE_MODE],
+    },
+    c = {
+      className: "function",
+      beginKeywords: "function constructor destructor procedure",
+      end: /[:;]/,
+      keywords: "function constructor|10 destructor|10 procedure|10",
+      contains: [
+        e.TITLE_MODE,
+        {
+          className: "params",
+          begin: /\(/,
+          end: /\)/,
+          keywords: a,
+          contains: [t, s, n].concat(r),
+        },
+        n,
+      ].concat(r),
+    };
+  return {
+    name: "Delphi",
+    aliases: [
+      "dpr",
+      "dfm",
+      "pas",
+      "pascal",
+      "freepascal",
+      "lazarus",
+      "lpr",
+      "lfm",
+    ],
+    case_insensitive: !0,
+    keywords: a,
+    illegal: /"|\$[G-Zg-z]|\/\*|<\/|\|/,
+    contains: [
+      t,
+      s,
+      e.NUMBER_MODE,
+      {
+        className: "number",
+        relevance: 0,
+        variants: [
+          { begin: "\\$[0-9A-Fa-f]+" },
+          { begin: "&[0-7]+" },
+          { begin: "%[01]+" },
+        ],
+      },
+      i,
+      c,
+      n,
+    ].concat(r),
+  };
+}
+
+module.exports = function (hljs) {
+  hljs.registerLanguage("pascal", hljsDefinePascal);
+};