--- a/Admin/components/components.sha1 Fri Nov 11 21:35:33 2022 +0100
+++ b/Admin/components/components.sha1 Fri Nov 11 23:04:55 2022 +0100
@@ -402,6 +402,7 @@
f84c7ecafb07a0d763f1d70edc54f7c43c2e8c63 postgresql-42.4.0.tar.gz
143d0d32a13d7d8e15b9bab866e14ad4308a6246 postgresql-42.5.0.tar.gz
f132329ca1045858ef456cc08b197c9eeea6881b postgresql-9.4.1212.tar.gz
+3fc5e7f759e7220b9e3fc5bac296e312e34a60ad prismjs-1.29.0.tar.gz
f042bba5fb82c7eb8aee99f92eb6ec38c8a067f7 python-3.10.4.tar.gz
0885e1f1d8feaca78d2f204b6487e6eec6dfab4b scala-2.10.0.tar.gz
f7dc7a4e1aea46408fd6e44b8cfacb33af61afbc scala-2.10.1.tar.gz
--- a/Admin/components/main Fri Nov 11 21:35:33 2022 +0100
+++ b/Admin/components/main Fri Nov 11 23:04:55 2022 +0100
@@ -27,6 +27,7 @@
pdfjs-2.14.305
polyml-test-bafe319bc3a6-1
postgresql-42.5.0
+prismjs-1.29.0
scala-3.2.0-2
smbc-0.4.1
spass-3.8ds-2
--- a/etc/build.props Fri Nov 11 21:35:33 2022 +0100
+++ b/etc/build.props Fri Nov 11 23:04:55 2022 +0100
@@ -31,6 +31,7 @@
src/Pure/Admin/build_pdfjs.scala \
src/Pure/Admin/build_polyml.scala \
src/Pure/Admin/build_postgresql.scala \
+ src/Pure/Admin/build_prismjs.scala \
src/Pure/Admin/build_release.scala \
src/Pure/Admin/build_scala.scala \
src/Pure/Admin/build_spass.scala \
@@ -196,6 +197,7 @@
src/Pure/Tools/mkroot.scala \
src/Pure/Tools/phabricator.scala \
src/Pure/Tools/print_operation.scala \
+ src/Pure/Tools/prismjs.scala \
src/Pure/Tools/profiling_report.scala \
src/Pure/Tools/scala_build.scala \
src/Pure/Tools/scala_project.scala \
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Admin/build_prismjs.scala Fri Nov 11 23:04:55 2022 +0100
@@ -0,0 +1,95 @@
+/* Title: Pure/Admin/build_prismjs.scala
+ Author: Makarius
+
+Build Isabelle component for the Prism.js syntax highlighter.
+
+See also:
+ - https://prismjs.com
+ - https://www.npmjs.com/package/prismjs
+*/
+
+package isabelle
+
+
+object Build_Prismjs {
+ /* build prismjs component */
+
+ val default_version = "1.29.0"
+
+ def build_prismjs(
+ version: String = default_version,
+ target_dir: Path = Path.current,
+ progress: Progress = new Progress
+ ): Unit = {
+ Isabelle_System.require_command("npm", test = "help")
+
+
+ /* component name */
+
+ val component = "prismjs-" + version
+ val component_dir = Isabelle_System.new_directory(target_dir + Path.basic(component))
+ progress.echo("Component " + component_dir)
+
+
+ /* download */
+
+ Isabelle_System.with_tmp_dir("tmp") { tmp_dir =>
+ Isabelle_System.bash("npm init -y && npm install prismjs@" + Bash.string(version),
+ cwd = tmp_dir.file).check
+
+ component_dir.file.delete()
+ Isabelle_System.copy_dir(tmp_dir + Path.explode("node_modules/prismjs"),
+ component_dir)
+ }
+
+
+ /* settings */
+
+ val etc_dir = Isabelle_System.make_directory(component_dir + Path.basic("etc"))
+ File.write(etc_dir + Path.basic("settings"),
+ """# -*- shell-script -*- :mode=shellscript:
+
+ISABELLE_PRISMJS_HOME="$COMPONENT"
+""")
+
+
+ /* README */
+
+ File.write(component_dir + Path.basic("README"),
+ """This is Prism.js """ + version + """ from https://www.npmjs.com/package/prismjs
+
+
+ Makarius
+ """ + Date.Format.date(Date.now()) + "\n")
+ }
+
+
+ /* Isabelle tool wrapper */
+
+ val isabelle_tool =
+ Isabelle_Tool("build_prismjs", "build component for prismjs",
+ Scala_Project.here,
+ { args =>
+ var target_dir = Path.current
+ var version = default_version
+
+ val getopts = Getopts("""
+Usage: isabelle build_prismjs [OPTIONS]
+
+ Options are:
+ -D DIR target directory (default ".")
+ -V VERSION version (default: """" + default_version + """")
+
+ Build component for Prism.js.
+""",
+ "D:" -> (arg => target_dir = Path.explode(arg)),
+ "V:" -> (arg => version = arg))
+
+ val more_args = getopts(args)
+ if (more_args.nonEmpty) getopts.usage()
+
+ val progress = new Console_Progress()
+
+ build_prismjs(version = version, target_dir = target_dir, progress = progress)
+ })
+}
--- a/src/Pure/System/isabelle_tool.scala Fri Nov 11 21:35:33 2022 +0100
+++ b/src/Pure/System/isabelle_tool.scala Fri Nov 11 23:04:55 2022 +0100
@@ -174,6 +174,7 @@
Build_PolyML.isabelle_tool1,
Build_PolyML.isabelle_tool2,
Build_PostgreSQL.isabelle_tool,
+ Build_Prismjs.isabelle_tool,
Build_SPASS.isabelle_tool,
Build_SQLite.isabelle_tool,
Build_Scala.isabelle_tool,
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Tools/prismjs.scala Fri Nov 11 23:04:55 2022 +0100
@@ -0,0 +1,105 @@
+/* Title: Pure/Tools/prismjs.scala
+ Author: Makarius
+
+Support for the Prism.js syntax highlighter -- via external Node.js process.
+*/
+
+package isabelle
+
+import scala.collection.mutable
+
+
+object Prismjs {
+ /* component resources */
+
+ val HOME: Path = Path.explode("$ISABELLE_PRISMJS_HOME")
+
+ lazy val available_languages: List[String] = {
+ val components_path = HOME + Path.explode("components.json")
+ val components_json = JSON.parse(File.read(components_path))
+ JSON.value(components_json, "languages") match {
+ case Some(JSON.Object(langs)) =>
+ (for ((lang, JSON.Object(info)) <- langs.iterator if lang != "meta") yield {
+ val alias =
+ JSON.Value.List.unapply(info.getOrElse("alias", Nil), JSON.Value.String.unapply)
+ .getOrElse(Nil)
+ lang :: alias
+ }).toList.flatten.sorted
+ case _ => error("Failed to determine languages from " + components_path)
+ }
+ }
+
+
+ /* JavaScript prelude */
+
+ def prelude(lang: JS.Source): JS.Source =
+ cat_lines(List(
+ Nodejs.require_fs,
+ Nodejs.require_path("prismjs", HOME),
+ Nodejs.require_path("prismjs_load", HOME + Path.explode("components"), dir = true),
+ JS.function("prismjs_load", lang),
+ """
+function prismjs_content(t) {
+ if (Array.isArray(t)) { return t.map(prismjs_content).join() }
+ else if (t instanceof prismjs.Token) { return prismjs_content(t.content) }
+ else { return t }
+}
+
+function prismjs_tokenize(text, lang) {
+ return prismjs.tokenize(text, prismjs.languages[lang]).map(function (t) {
+ if (t instanceof prismjs.Token) {
+ return {"kind": t.type, "content": prismjs_content(t)}
+ }
+ else { return {"kind": "", "content": t} }
+ })
+}
+"""))
+
+
+ /* tokenize */
+
+ sealed case class Token(
+ kind: String,
+ content: String,
+ range: Text.Range = Text.Range.zero)
+
+ def tokenize(text: String, language: String): List[Token] = {
+ if (!available_languages.contains(language)) {
+ error("Unknown language " + quote(language))
+ }
+
+ val json =
+ Isabelle_System.with_tmp_file("input", ext = "json") { input =>
+ Isabelle_System.with_tmp_file("output", ext = "json") { output =>
+ File.write(input, text)
+ val lang = JS.value(language)
+ Nodejs.execute(
+ prelude(lang) + "\n" +
+ Nodejs.write_file(output,
+ JS.json_print(JS.function("prismjs_tokenize", Nodejs.read_file(input), lang))))
+ JSON.parse(File.read(output))
+ }
+ }
+
+ def parse_token(t: JSON.T): Token =
+ (for {
+ kind <- JSON.string(t, "kind")
+ content <- JSON.string(t, "content")
+ } yield Token(kind, content)).getOrElse(error("Malformed JSON token: " + t))
+
+ val tokens0 =
+ JSON.Value.List.unapply(json, t => Some(parse_token(t)))
+ .getOrElse(error("Malformed JSON: array expected"))
+
+ var stop = 0
+ val tokens = new mutable.ListBuffer[Token]
+ for (tok <- tokens0) {
+ val start = stop
+ stop += tok.content.length
+ if (tok.kind.nonEmpty) {
+ tokens += tok.copy(range = Text.Range(start, stop))
+ }
+ }
+ tokens.toList
+ }
+}