src/Pure/General/js.scala
author wenzelm
Fri, 11 Nov 2022 23:25:24 +0100
changeset 76509 b01b0014c3f9
parent 76507 78a2030240f1
child 77570 98b4a9902582
permissions -rw-r--r--
proper support for Windows;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
76507
78a2030240f1 support for JavaScript syntax and Node.js platform;
wenzelm
parents:
diff changeset
     1
/*  Title:      Pure/General/json.scala
78a2030240f1 support for JavaScript syntax and Node.js platform;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
78a2030240f1 support for JavaScript syntax and Node.js platform;
wenzelm
parents:
diff changeset
     3
78a2030240f1 support for JavaScript syntax and Node.js platform;
wenzelm
parents:
diff changeset
     4
Support for JavaScript syntax.
78a2030240f1 support for JavaScript syntax and Node.js platform;
wenzelm
parents:
diff changeset
     5
*/
78a2030240f1 support for JavaScript syntax and Node.js platform;
wenzelm
parents:
diff changeset
     6
78a2030240f1 support for JavaScript syntax and Node.js platform;
wenzelm
parents:
diff changeset
     7
package isabelle
78a2030240f1 support for JavaScript syntax and Node.js platform;
wenzelm
parents:
diff changeset
     8
78a2030240f1 support for JavaScript syntax and Node.js platform;
wenzelm
parents:
diff changeset
     9
78a2030240f1 support for JavaScript syntax and Node.js platform;
wenzelm
parents:
diff changeset
    10
object JS {
78a2030240f1 support for JavaScript syntax and Node.js platform;
wenzelm
parents:
diff changeset
    11
  /* basic syntax */
78a2030240f1 support for JavaScript syntax and Node.js platform;
wenzelm
parents:
diff changeset
    12
78a2030240f1 support for JavaScript syntax and Node.js platform;
wenzelm
parents:
diff changeset
    13
  type Source = String
78a2030240f1 support for JavaScript syntax and Node.js platform;
wenzelm
parents:
diff changeset
    14
78a2030240f1 support for JavaScript syntax and Node.js platform;
wenzelm
parents:
diff changeset
    15
  def arguments(args: Source*): Source = args.mkString("(", ", ", ")")
78a2030240f1 support for JavaScript syntax and Node.js platform;
wenzelm
parents:
diff changeset
    16
  def function(f: Source, args: Source*): Source = f + arguments(args: _*)
78a2030240f1 support for JavaScript syntax and Node.js platform;
wenzelm
parents:
diff changeset
    17
  def selection(a: Source, arg: Source): Source = a + "[" + arg + "]"
78a2030240f1 support for JavaScript syntax and Node.js platform;
wenzelm
parents:
diff changeset
    18
78a2030240f1 support for JavaScript syntax and Node.js platform;
wenzelm
parents:
diff changeset
    19
  def commands(args: Source*): Source = args.mkString("; ")
78a2030240f1 support for JavaScript syntax and Node.js platform;
wenzelm
parents:
diff changeset
    20
  def command_list(args: List[Source]): Source = args.mkString("; ")
78a2030240f1 support for JavaScript syntax and Node.js platform;
wenzelm
parents:
diff changeset
    21
78a2030240f1 support for JavaScript syntax and Node.js platform;
wenzelm
parents:
diff changeset
    22
78a2030240f1 support for JavaScript syntax and Node.js platform;
wenzelm
parents:
diff changeset
    23
  /* JSON values */
78a2030240f1 support for JavaScript syntax and Node.js platform;
wenzelm
parents:
diff changeset
    24
78a2030240f1 support for JavaScript syntax and Node.js platform;
wenzelm
parents:
diff changeset
    25
  def value(t: JSON.T): Source = JSON.Format(t)
78a2030240f1 support for JavaScript syntax and Node.js platform;
wenzelm
parents:
diff changeset
    26
  def string(s: String): Source = value(s)
78a2030240f1 support for JavaScript syntax and Node.js platform;
wenzelm
parents:
diff changeset
    27
78a2030240f1 support for JavaScript syntax and Node.js platform;
wenzelm
parents:
diff changeset
    28
  def json_parse(arg: Source): Source = function("JSON.parse", arg)
78a2030240f1 support for JavaScript syntax and Node.js platform;
wenzelm
parents:
diff changeset
    29
  def json_print(arg: Source): Source = function("JSON.stringify", arg)
78a2030240f1 support for JavaScript syntax and Node.js platform;
wenzelm
parents:
diff changeset
    30
78a2030240f1 support for JavaScript syntax and Node.js platform;
wenzelm
parents:
diff changeset
    31
78a2030240f1 support for JavaScript syntax and Node.js platform;
wenzelm
parents:
diff changeset
    32
  /* file-system operations */
78a2030240f1 support for JavaScript syntax and Node.js platform;
wenzelm
parents:
diff changeset
    33
78a2030240f1 support for JavaScript syntax and Node.js platform;
wenzelm
parents:
diff changeset
    34
  def standard_path(p: Path, dir: Boolean = false): Source =
78a2030240f1 support for JavaScript syntax and Node.js platform;
wenzelm
parents:
diff changeset
    35
    string(File.standard_path(p) + (if (dir) "/" else ""))
78a2030240f1 support for JavaScript syntax and Node.js platform;
wenzelm
parents:
diff changeset
    36
78a2030240f1 support for JavaScript syntax and Node.js platform;
wenzelm
parents:
diff changeset
    37
  def platform_path(p: Path, dir: Boolean = false): Source =
76509
b01b0014c3f9 proper support for Windows;
wenzelm
parents: 76507
diff changeset
    38
    string(File.platform_path(p) + (if (dir) "/" else ""))
76507
78a2030240f1 support for JavaScript syntax and Node.js platform;
wenzelm
parents:
diff changeset
    39
}