77570
|
1 |
/* Title: Pure/General/js.scala
|
76507
|
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 |
}
|