Highlight snippets in tutorial

2025-08-04 18:48:13 +00:00 · 2023-04-06 22:37:52 +02:00 · 2023-04-06 22:37:52 +02:00 · 01b6fe4f9f
commit 01b6fe4f9f
parent 376beb4325
11 changed files with 300 additions and 11 deletions
--- a/web/.stylelintignore
+++ b/web/.stylelintignore
@ -0,0 +1,2 @@
+packages/app/assets/hljs-vs-dark.css
+packages/app/assets/hljs-vs-light.css
--- a/web/package-lock.json
+++ b/web/package-lock.json
@ -2877,6 +2877,14 @@
        "he": "bin/he"
      }
    },
+    "node_modules/highlight.js": {
+      "version": "11.7.0",
+      "resolved": "https://registry.npmjs.org/highlight.js/-/highlight.js-11.7.0.tgz",
+      "integrity": "sha512-1rRqesRFhMO/PRF+G86evnyJkCgaZFOI+Z6kdj15TA18funfoqJXvgPCLSf0SWq3SRfg1j3HlDs8o4s3EGq1oQ==",
+      "engines": {
+        "node": ">=12.0.0"
+      }
+    },
    "node_modules/hosted-git-info": {
      "version": "4.1.0",
      "resolved": "https://registry.npmjs.org/hosted-git-info/-/hosted-git-info-4.1.0.tgz",
@ -3103,6 +3111,12 @@
        "node": ">= 4"
      }
    },
+    "node_modules/immutable": {
+      "version": "4.3.0",
+      "resolved": "https://registry.npmjs.org/immutable/-/immutable-4.3.0.tgz",
+      "integrity": "sha512-0AOCmOip+xgJwEVTQj1EfiDDOkPmuyllDuTuEX+DDXUgapLAsBIfkg3sxCYyCEA8mQqZrrxPUGjcOQ2JS3WLkg==",
+      "dev": true
+    },
    "node_modules/import-fresh": {
      "version": "3.3.0",
      "dev": true,
@ -3459,6 +3473,15 @@
        "node": ">=0.10.0"
      }
    },
+    "node_modules/klona": {
+      "version": "2.0.6",
+      "resolved": "https://registry.npmjs.org/klona/-/klona-2.0.6.tgz",
+      "integrity": "sha512-dhG34DXATL5hSxJbIexCft8FChFXtmskoZYnoPWjXQuebWYCNkVeV3KkGegCK9CP1oswI/vQibS2GY7Em/sJJA==",
+      "dev": true,
+      "engines": {
+        "node": ">= 8"
+      }
+    },
    "node_modules/known-css-properties": {
      "version": "0.25.0",
      "resolved": "https://registry.npmjs.org/known-css-properties/-/known-css-properties-0.25.0.tgz",
@ -4769,6 +4792,61 @@
      "dev": true,
      "license": "MIT"
    },
+    "node_modules/sass": {
+      "version": "1.60.0",
+      "resolved": "https://registry.npmjs.org/sass/-/sass-1.60.0.tgz",
+      "integrity": "sha512-updbwW6fNb5gGm8qMXzVO7V4sWf7LMXnMly/JEyfbfERbVH46Fn6q02BX7/eHTdKpE7d+oTkMMQpFWNUMfFbgQ==",
+      "dev": true,
+      "dependencies": {
+        "chokidar": ">=3.0.0 <4.0.0",
+        "immutable": "^4.0.0",
+        "source-map-js": ">=0.6.2 <2.0.0"
+      },
+      "bin": {
+        "sass": "sass.js"
+      },
+      "engines": {
+        "node": ">=12.0.0"
+      }
+    },
+    "node_modules/sass-loader": {
+      "version": "13.2.2",
+      "resolved": "https://registry.npmjs.org/sass-loader/-/sass-loader-13.2.2.tgz",
+      "integrity": "sha512-nrIdVAAte3B9icfBiGWvmMhT/D+eCDwnk+yA7VE/76dp/WkHX+i44Q/pfo71NYbwj0Ap+PGsn0ekOuU1WFJ2AA==",
+      "dev": true,
+      "dependencies": {
+        "klona": "^2.0.6",
+        "neo-async": "^2.6.2"
+      },
+      "engines": {
+        "node": ">= 14.15.0"
+      },
+      "funding": {
+        "type": "opencollective",
+        "url": "https://opencollective.com/webpack"
+      },
+      "peerDependencies": {
+        "fibers": ">= 3.1.0",
+        "node-sass": "^4.0.0 || ^5.0.0 || ^6.0.0 || ^7.0.0 || ^8.0.0",
+        "sass": "^1.3.0",
+        "sass-embedded": "*",
+        "webpack": "^5.0.0"
+      },
+      "peerDependenciesMeta": {
+        "fibers": {
+          "optional": true
+        },
+        "node-sass": {
+          "optional": true
+        },
+        "sass": {
+          "optional": true
+        },
+        "sass-embedded": {
+          "optional": true
+        }
+      }
+    },
    "node_modules/schema-utils": {
      "version": "4.0.0",
      "dev": true,
@ -6199,6 +6277,7 @@
      "dependencies": {
        "@picocss/pico": "^1.5.7",
        "debounce": "^1.2.1",
+        "highlight.js": "^11.7.0",
        "json-rpc-2.0": "^1.3.0",
        "monaco-editor-core": "^0.33.0",
        "monaco-languageclient": "^1.0.1",
@ -6219,6 +6298,8 @@
        "html-webpack-plugin": "^5.5.0",
        "path-browserify": "^1.0.1",
        "prettier": "^2.6.2",
+        "sass": "^1.60.0",
+        "sass-loader": "^13.2.2",
        "source-map-loader": "^4.0.0",
        "style-loader": "^3.3.1",
        "stylelint": "^14.11.0",
@ -8154,6 +8235,11 @@
      "version": "1.2.0",
      "dev": true
    },
+    "highlight.js": {
+      "version": "11.7.0",
+      "resolved": "https://registry.npmjs.org/highlight.js/-/highlight.js-11.7.0.tgz",
+      "integrity": "sha512-1rRqesRFhMO/PRF+G86evnyJkCgaZFOI+Z6kdj15TA18funfoqJXvgPCLSf0SWq3SRfg1j3HlDs8o4s3EGq1oQ=="
+    },
    "hosted-git-info": {
      "version": "4.1.0",
      "resolved": "https://registry.npmjs.org/hosted-git-info/-/hosted-git-info-4.1.0.tgz",
@ -8302,6 +8388,12 @@
      "version": "5.2.0",
      "dev": true
    },
+    "immutable": {
+      "version": "4.3.0",
+      "resolved": "https://registry.npmjs.org/immutable/-/immutable-4.3.0.tgz",
+      "integrity": "sha512-0AOCmOip+xgJwEVTQj1EfiDDOkPmuyllDuTuEX+DDXUgapLAsBIfkg3sxCYyCEA8mQqZrrxPUGjcOQ2JS3WLkg==",
+      "dev": true
+    },
    "import-fresh": {
      "version": "3.3.0",
      "dev": true,
@ -8517,6 +8609,12 @@
      "version": "6.0.3",
      "dev": true
    },
+    "klona": {
+      "version": "2.0.6",
+      "resolved": "https://registry.npmjs.org/klona/-/klona-2.0.6.tgz",
+      "integrity": "sha512-dhG34DXATL5hSxJbIexCft8FChFXtmskoZYnoPWjXQuebWYCNkVeV3KkGegCK9CP1oswI/vQibS2GY7Em/sJJA==",
+      "dev": true
+    },
    "known-css-properties": {
      "version": "0.25.0",
      "resolved": "https://registry.npmjs.org/known-css-properties/-/known-css-properties-0.25.0.tgz",
@ -8745,12 +8843,15 @@
        "eslint-config-prettier": "^8.5.0",
        "eslint-plugin-prettier": "^4.0.0",
        "file-loader": "^6.2.0",
+        "highlight.js": "^11.7.0",
        "html-webpack-plugin": "^5.5.0",
        "json-rpc-2.0": "^1.3.0",
        "monaco-editor-core": "^0.33.0",
        "monaco-languageclient": "^1.0.1",
        "path-browserify": "^1.0.1",
        "prettier": "^2.6.2",
+        "sass": "*",
+        "sass-loader": "^13.2.2",
        "source-map-loader": "^4.0.0",
        "style-loader": "^3.3.1",
        "stylelint": "^14.11.0",
@ -9379,6 +9480,27 @@
      "version": "2.1.2",
      "dev": true
    },
+    "sass": {
+      "version": "1.60.0",
+      "resolved": "https://registry.npmjs.org/sass/-/sass-1.60.0.tgz",
+      "integrity": "sha512-updbwW6fNb5gGm8qMXzVO7V4sWf7LMXnMly/JEyfbfERbVH46Fn6q02BX7/eHTdKpE7d+oTkMMQpFWNUMfFbgQ==",
+      "dev": true,
+      "requires": {
+        "chokidar": ">=3.0.0 <4.0.0",
+        "immutable": "^4.0.0",
+        "source-map-js": ">=0.6.2 <2.0.0"
+      }
+    },
+    "sass-loader": {
+      "version": "13.2.2",
+      "resolved": "https://registry.npmjs.org/sass-loader/-/sass-loader-13.2.2.tgz",
+      "integrity": "sha512-nrIdVAAte3B9icfBiGWvmMhT/D+eCDwnk+yA7VE/76dp/WkHX+i44Q/pfo71NYbwj0Ap+PGsn0ekOuU1WFJ2AA==",
+      "dev": true,
+      "requires": {
+        "klona": "^2.0.6",
+        "neo-async": "^2.6.2"
+      }
+    },
    "schema-utils": {
      "version": "4.0.0",
      "dev": true,
--- a/web/packages/app/assets/highlight.scss
+++ b/web/packages/app/assets/highlight.scss
@ -0,0 +1,8 @@
+@use "sass:meta";
+
+html[data-theme="light"] {
+    @include meta.load-css("./hljs-vs-light");
+}
+html[data-theme="dark"] {
+    @include meta.load-css("./hljs-vs-dark");
+}
--- a/web/packages/app/assets/hljs-vs-dark.css
+++ b/web/packages/app/assets/hljs-vs-dark.css
@ -0,0 +1,59 @@
+.hljs {
+  background: #1e1e1e;
+  color: #d4d4d4;
+}
+
+.hljs-comment,
+.hljs-quote,
+.hljs-variable {
+  color: #608b4e;
+}
+
+.hljs-keyword,
+.hljs-selector-tag,
+.hljs-built_in,
+.hljs-name,
+.hljs-tag {
+  color: #569cd6;
+}
+
+.hljs-string,
+.hljs-title,
+.hljs-section,
+.hljs-attribute,
+.hljs-literal,
+.hljs-template-tag,
+.hljs-template-variable,
+.hljs-type,
+.hljs-addition {
+  color: #3dc9b0;
+}
+
+.hljs-deletion,
+.hljs-selector-attr,
+.hljs-selector-pseudo,
+.hljs-meta {
+  color: #2b91af;
+}
+
+.hljs-doctag {
+  color: #808080;
+}
+
+.hljs-attr {
+  color: #f00;
+}
+
+.hljs-symbol,
+.hljs-bullet,
+.hljs-link {
+  color: #00b0e8;
+}
+
+.hljs-emphasis {
+  font-style: italic;
+}
+
+.hljs-strong {
+  font-weight: bold;
+}
--- a/web/packages/app/assets/hljs-vs-light.css
+++ b/web/packages/app/assets/hljs-vs-light.css
@ -0,0 +1,59 @@
+.hljs {
+  background: white;
+  color: black;
+}
+
+.hljs-comment,
+.hljs-quote,
+.hljs-variable {
+  color: #008000;
+}
+
+.hljs-keyword,
+.hljs-selector-tag,
+.hljs-built_in,
+.hljs-name,
+.hljs-tag {
+  color: #00f;
+}
+
+.hljs-string,
+.hljs-title,
+.hljs-section,
+.hljs-attribute,
+.hljs-literal,
+.hljs-template-tag,
+.hljs-template-variable,
+.hljs-type,
+.hljs-addition {
+  color: #008080;
+}
+
+.hljs-deletion,
+.hljs-selector-attr,
+.hljs-selector-pseudo,
+.hljs-meta {
+  color: #2b91af;
+}
+
+.hljs-doctag {
+  color: #808080;
+}
+
+.hljs-attr {
+  color: #f00;
+}
+
+.hljs-symbol,
+.hljs-bullet,
+.hljs-link {
+  color: #00b0e8;
+}
+
+.hljs-emphasis {
+  font-style: italic;
+}
+
+.hljs-strong {
+  font-weight: bold;
+}
--- a/web/packages/app/assets/index.html
+++ b/web/packages/app/assets/index.html
@ -71,21 +71,21 @@
      In that case, the constructors of the data-type can be given as a comma-separated list.
      As with all syntactic constructs, we always allow trailing commas.

-<pre><code>
+<pre><code class="language-xfn">
 data Bool { True, False, }
 </code></pre>

      In the more general case we have to specify the precise type that a constructor constructs.
      Therefore, the above data type declaration can be written more explicitly as:

-<pre><code>
+<pre><code class="language-xfn">
 data Bool { True: Bool, False: Bool }
 </code></pre>

      A simple example of a parameterized type is the type of singly-linked lists of some type <code>a</code>.
      In that case, we have to specify both the parameters of the type constructor <code>List</code>, and the instantiations of the term constructors <code>Nil</code> and <code>Cons</code>.
      For the parameter of the type constructor <code>List</code> we make use of the impredicative type universe, which is written <code>Type</code>.
-<pre><code>
+<pre><code class="language-xfn">
 data List(a: Type) {
  Nil(a: Type): List(a),
  Cons(a: Type, x: a, xs: List(a)): List(a)
@ -94,7 +94,7 @@ data List(a: Type) {

 A proper dependent type is the type of length-indexed lists: the vector type.
 The <code>VNil</code> and <code>VCons</code> constructors of vectors create vectors with different indices.
-<pre><code>
+<pre><code class="language-xfn">
 data N { Z, S(n: N) }
 data Vec(a: Type, n: Nat) {
  VNil(a:Type): Vec(a,Z),
@ -107,7 +107,7 @@ data Vec(a: Type, n: Nat) {
  <summary><b>Codata Types</b></summary>
      Codata types are specified by a list of methods or destructors.
      A very simple example is the type of pairs of a boolean and a natural number:
-<pre><code>
+<pre><code class="language-xfn">
 data Bool { True, False }
 data N { Z, S(n: N)}
 codata Pair {
@ -118,7 +118,7 @@ codata Pair {
      This type supports two observations; the first observations <code>proj1</code> yields a boolean value when invoked on a <code>Pair</code>, and the observation <code>proj2</code> yields a natural number.

      Codata types can also model infinite types. The type of infinite streams is a classical example and written like this:
-<pre><code>
+<pre><code class="language-xfn">
 codata Stream(a: Type) {
  Stream(a).head(a: Type) : a,
  Stream(a).tail(a: Type) : Stream(a),
@ -127,7 +127,7 @@ codata Stream(a: Type) {
       Sometimes we also need to reference the object on which a method is invoked in its return type.
       This is especially the case when we want an observation to yield a proof that the object satisfies some property.
       Here is a simple example which shows how this can be expressed:
-<pre><code>
+<pre><code class="language-xfn">
 codata Bool {
  Bool.neg : Bool
  (x: Bool).neg_is_inverse : Eq(Bool, x, x.neg.neg)
@ -148,7 +148,7 @@ codata Bool {
      Line comments are written using two dashes: <code>-- This is a comment</code>.
      Certain items of the program can also be annotated with a documentation comment.
      Here is an example using doc-comments:
-<pre><code>
+<pre><code class="language-xfn">
 -- | The type of booleans
 data Bool {
  -- | The boolean truth value
@ -166,7 +166,7 @@ data Bool {
      An incomplete program can be written using typed holes.
      Typed holes are written using either <code>?</code> or <code>...</code>; they have type <code>?</code> which unifies with any other type.
      For example, an incomplete implementation of boolean negation can be written as follows:
-<pre><code>
+<pre><code class="language-xfn">
 def Bool.neg : Bool {
  True =&gt; ?,
  False =&gt; ?,
@ -177,7 +177,7 @@ def Bool.neg : Bool {
  <summary><b>The Main Expression</b></summary>
      After all other data types, codata types, definitions and codefinitions an additional expression can be written.
      This is called the "main" expression of the program.
-<pre><code>
+<pre><code class="language-xfn">
 data Bool { True, False }
 def Bool.neg {
  True =&gt; False,
--- a/web/packages/app/package.json
+++ b/web/packages/app/package.json
@ -39,6 +39,8 @@
    "html-webpack-plugin": "^5.5.0",
    "path-browserify": "^1.0.1",
    "prettier": "^2.6.2",
+    "sass": "^1.60.0",
+    "sass-loader": "^13.2.2",
    "source-map-loader": "^4.0.0",
    "style-loader": "^3.3.1",
    "stylelint": "^14.11.0",
@ -53,6 +55,7 @@
  "dependencies": {
    "@picocss/pico": "^1.5.7",
    "debounce": "^1.2.1",
+    "highlight.js": "^11.7.0",
    "json-rpc-2.0": "^1.3.0",
    "monaco-editor-core": "^0.33.0",
    "monaco-languageclient": "^1.0.1",
--- a/web/packages/app/src/highlight.ts
+++ b/web/packages/app/src/highlight.ts
@ -0,0 +1,29 @@
+import { Language } from "highlight.js";
+import hljs from "highlight.js";
+import "../assets/highlight.scss";
+
+const COMMENT = hljs.COMMENT("--", "$");
+const PUNCTUATION = {
+  match: /=>|,|:|\.|{|}|\(|\)/,
+  className: "punctuation",
+};
+const UPPER_IDENT = {
+  match: /[A-Z][a-zA-Z0-9_]*[']*/,
+  className: "title.class",
+  relevance: 1,
+};
+const xfn: Language = {
+  case_insensitive: false,
+  keywords: {
+    keyword: ["data", "codata", "impl", "def", "codef", "match", "comatch", "absurd"],
+    built_in: ["Type"],
+  },
+  contains: [COMMENT, PUNCTUATION, UPPER_IDENT],
+};
+
+export const register = () => {
+  document.addEventListener("DOMContentLoaded", () => {
+    hljs.registerLanguage("xfn", () => xfn);
+    hljs.highlightAll();
+  });
+};
--- a/web/packages/app/src/index.ts
+++ b/web/packages/app/src/index.ts
@ -1,6 +1,9 @@
 import "../assets/index.module.css";

 import App from "./app";
+import * as highlight from "./highlight";
+
+highlight.register();

 const app = new App();
 app.run().catch(console.error);
--- a/web/packages/app/src/language.ts
+++ b/web/packages/app/src/language.ts
@ -115,7 +115,7 @@ export default class Language implements monaco.languages.ILanguageExtensionPoin
            /[a-z_][a-zA-Z0-9_]*[']*/,
            { cases: { "@typeKeywords": "keyword", "@keywords": "keyword", "@default": "identifier" } },
          ],
-          [/[A-Z_][a-zA-Z0-9_]*[']*/, "type.identifier"],
+          [/[A-Z][a-zA-Z0-9_]*[']*/, "type.identifier"],

          // whitespace
          { include: "@whitespace" },
--- a/web/packages/app/webpack.config.js
+++ b/web/packages/app/webpack.config.js
@ -54,6 +54,10 @@ module.exports = (env, argv) => {
          test: /\.css$/,
          use: ["style-loader", "css-loader"],
        },
+        {
+          test: /\.s[ac]ss$/i,
+          use: ["style-loader", "css-loader", "sass-loader"],
+        },
        {
          test: /\.(woff|woff2|eot|ttf|otf)$/i,
          type: "asset/resource",