| 
76507
 | 
     1  | 
/*  Title:      Pure/General/json.scala
  | 
| 
 | 
     2  | 
    Author:     Makarius
  | 
| 
 | 
     3  | 
  | 
| 
 | 
     4  | 
Support for JavaScript syntax.
  | 
| 
 | 
     5  | 
*/
  | 
| 
 | 
     6  | 
  | 
| 
 | 
     7  | 
package isabelle
  | 
| 
 | 
     8  | 
  | 
| 
 | 
     9  | 
  | 
| 
 | 
    10  | 
object JS {
 | 
| 
 | 
    11  | 
  /* basic syntax */
  | 
| 
 | 
    12  | 
  | 
| 
 | 
    13  | 
  type Source = String
  | 
| 
 | 
    14  | 
  | 
| 
 | 
    15  | 
  def arguments(args: Source*): Source = args.mkString("(", ", ", ")")
 | 
| 
 | 
    16  | 
  def function(f: Source, args: Source*): Source = f + arguments(args: _*)
  | 
| 
 | 
    17  | 
  def selection(a: Source, arg: Source): Source = a + "[" + arg + "]"
  | 
| 
 | 
    18  | 
  | 
| 
 | 
    19  | 
  def commands(args: Source*): Source = args.mkString("; ")
 | 
| 
 | 
    20  | 
  def command_list(args: List[Source]): Source = args.mkString("; ")
 | 
| 
 | 
    21  | 
  | 
| 
 | 
    22  | 
  | 
| 
 | 
    23  | 
  /* JSON values */
  | 
| 
 | 
    24  | 
  | 
| 
 | 
    25  | 
  def value(t: JSON.T): Source = JSON.Format(t)
  | 
| 
 | 
    26  | 
  def string(s: String): Source = value(s)
  | 
| 
 | 
    27  | 
  | 
| 
 | 
    28  | 
  def json_parse(arg: Source): Source = function("JSON.parse", arg)
 | 
| 
 | 
    29  | 
  def json_print(arg: Source): Source = function("JSON.stringify", arg)
 | 
| 
 | 
    30  | 
  | 
| 
 | 
    31  | 
  | 
| 
 | 
    32  | 
  /* file-system operations */
  | 
| 
 | 
    33  | 
  | 
| 
 | 
    34  | 
  def standard_path(p: Path, dir: Boolean = false): Source =
  | 
| 
 | 
    35  | 
    string(File.standard_path(p) + (if (dir) "/" else ""))
  | 
| 
 | 
    36  | 
  | 
| 
 | 
    37  | 
  def platform_path(p: Path, dir: Boolean = false): Source =
  | 
| 
76509
 | 
    38  | 
    string(File.platform_path(p) + (if (dir) "/" else ""))
  | 
| 
76507
 | 
    39  | 
}
  |