clarified JS namespace;
authorwenzelm
Sat, 12 Nov 2022 17:21:38 +0100
changeset 76510 b0ad975cd25b
parent 76509 b01b0014c3f9
child 76511 ec8c04dac257
clarified JS namespace;
src/Pure/System/nodejs.scala
src/Pure/Tools/prismjs.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 */
 
--- 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() }