# HG changeset patch # User wenzelm # Date 1668270098 -3600 # Node ID b0ad975cd25baa8f967273c52611cf5a9a26dcc0 # Parent b01b0014c3f92f88769aa05136f6db67d4a5bbec clarified JS namespace; diff -r b01b0014c3f9 -r b0ad975cd25b src/Pure/System/nodejs.scala --- a/src/Pure/System/nodejs.scala Fri Nov 11 23:25:24 2022 +0100 +++ b/src/Pure/System/nodejs.scala Sat Nov 12 17:21:38 2022 +0100 @@ -13,14 +13,14 @@ /* require modules */ def require_module(name: JS.Source, module: JS.Source): JS.Source = - "const " + name + " = require(" + module + ")" - - def require_builtin(name: JS.Source): JS.Source = - require_module(name, JS.string(name)) + name + " = require(" + module + ")" def require_path(name: JS.Source, path: Path, dir: Boolean = false): JS.Source = require_module(name, JS.platform_path(path, dir = dir)) + def require_builtin(name: String): JS.Source = + require_module("const " + name, JS.string(name)) + /* file-system operations */ diff -r b01b0014c3f9 -r b0ad975cd25b src/Pure/Tools/prismjs.scala --- a/src/Pure/Tools/prismjs.scala Fri Nov 11 23:25:24 2022 +0100 +++ b/src/Pure/Tools/prismjs.scala Sat Nov 12 17:21:38 2022 +0100 @@ -35,9 +35,9 @@ 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), + Nodejs.require_path("const 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() }