# HG changeset patch
# User wenzelm
# Date 1668198933 -3600
# Node ID 78a2030240f11542a86e7a6c97b98536a6c51603
# Parent  ac5833ebe6d16bc31e14d0af82901d799d3428f2
support for JavaScript syntax and Node.js platform;

diff -r ac5833ebe6d1 -r 78a2030240f1 etc/build.props
--- a/etc/build.props	Thu Nov 10 14:55:20 2022 +0100
+++ b/etc/build.props	Fri Nov 11 21:35:33 2022 +0100
@@ -78,6 +78,7 @@
   src/Pure/General/graph_display.scala \
   src/Pure/General/graphics_file.scala \
   src/Pure/General/http.scala \
+  src/Pure/General/js.scala \
   src/Pure/General/json.scala \
   src/Pure/General/json_api.scala \
   src/Pure/General/linear_set.scala \
@@ -158,6 +159,7 @@
   src/Pure/System/java_statistics.scala \
   src/Pure/System/linux.scala \
   src/Pure/System/mingw.scala \
+  src/Pure/System/nodejs.scala \
   src/Pure/System/numa.scala \
   src/Pure/System/options.scala \
   src/Pure/System/platform.scala \
diff -r ac5833ebe6d1 -r 78a2030240f1 src/Pure/General/js.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/js.scala	Fri Nov 11 21:35:33 2022 +0100
@@ -0,0 +1,39 @@
+/*  Title:      Pure/General/json.scala
+    Author:     Makarius
+
+Support for JavaScript syntax.
+*/
+
+package isabelle
+
+
+object JS {
+  /* basic syntax */
+
+  type Source = String
+
+  def arguments(args: Source*): Source = args.mkString("(", ", ", ")")
+  def function(f: Source, args: Source*): Source = f + arguments(args: _*)
+  def selection(a: Source, arg: Source): Source = a + "[" + arg + "]"
+
+  def commands(args: Source*): Source = args.mkString("; ")
+  def command_list(args: List[Source]): Source = args.mkString("; ")
+
+
+  /* JSON values */
+
+  def value(t: JSON.T): Source = JSON.Format(t)
+  def string(s: String): Source = value(s)
+
+  def json_parse(arg: Source): Source = function("JSON.parse", arg)
+  def json_print(arg: Source): Source = function("JSON.stringify", arg)
+
+
+  /* file-system operations */
+
+  def standard_path(p: Path, dir: Boolean = false): Source =
+    string(File.standard_path(p) + (if (dir) "/" else ""))
+
+  def platform_path(p: Path, dir: Boolean = false): Source =
+    string(File.platform_path(p) + (if (dir) File.platform_path(Path.root) else ""))
+}
diff -r ac5833ebe6d1 -r 78a2030240f1 src/Pure/System/nodejs.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/System/nodejs.scala	Fri Nov 11 21:35:33 2022 +0100
@@ -0,0 +1,43 @@
+/*  Title:      Pure/System/nodejs.scala
+    Author:     Makarius
+
+Support for the Node.js platform, as provided by Isabelle/VSCodium component.
+
+See also: https://nodejs.org/docs/latest-v16.x
+*/
+
+package isabelle
+
+
+object Nodejs {
+  /* 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))
+
+  def require_path(name: JS.Source, path: Path, dir: Boolean = false): JS.Source =
+    require_module(name, JS.platform_path(path, dir = dir))
+
+
+  /* file-system operations */
+
+  def require_fs: JS.Source = require_builtin("fs")
+
+  val encoding_utf8: JSON.T = JSON.Object("encoding" -> "utf8")
+
+  def read_file(path: Path): JS.Source =
+    JS.function("fs.readFileSync", JS.platform_path(path), JS.value(encoding_utf8))
+
+  def write_file(path: Path, arg: JS.Source): JS.Source =
+    JS.function("fs.writeFileSync", JS.platform_path(path), arg, JS.value(encoding_utf8))
+
+
+  /* external process */
+
+  def execute(js: String): Process_Result =
+    Isabelle_System.bash("isabelle node -", input = js,
+      description = "Node.js").check
+}