| author | wenzelm |
| Tue, 07 Mar 2023 22:54:44 +0100 | |
| changeset 77566 | 2a99fcb283ee |
| parent 76621 | src/Pure/Admin/build_prismjs.scala@7af197063e2f |
| child 80224 | db92e0b6a11a |
| permissions | -rw-r--r-- |
|
77566
2a99fcb283ee
renamed administrative tools to build Isabelle components (unrelated to "isabelle build");
wenzelm
parents:
76621
diff
changeset
|
1 |
/* Title: Pure/Admin/component_prismjs.scala |
|
76508
ecb9e6d29698
support for the Prism.js syntax highlighter -- via external Node.js process;
wenzelm
parents:
diff
changeset
|
2 |
Author: Makarius |
|
ecb9e6d29698
support for the Prism.js syntax highlighter -- via external Node.js process;
wenzelm
parents:
diff
changeset
|
3 |
|
|
ecb9e6d29698
support for the Prism.js syntax highlighter -- via external Node.js process;
wenzelm
parents:
diff
changeset
|
4 |
Build Isabelle component for the Prism.js syntax highlighter. |
|
ecb9e6d29698
support for the Prism.js syntax highlighter -- via external Node.js process;
wenzelm
parents:
diff
changeset
|
5 |
|
|
ecb9e6d29698
support for the Prism.js syntax highlighter -- via external Node.js process;
wenzelm
parents:
diff
changeset
|
6 |
See also: |
|
ecb9e6d29698
support for the Prism.js syntax highlighter -- via external Node.js process;
wenzelm
parents:
diff
changeset
|
7 |
- https://prismjs.com |
|
ecb9e6d29698
support for the Prism.js syntax highlighter -- via external Node.js process;
wenzelm
parents:
diff
changeset
|
8 |
- https://www.npmjs.com/package/prismjs |
|
ecb9e6d29698
support for the Prism.js syntax highlighter -- via external Node.js process;
wenzelm
parents:
diff
changeset
|
9 |
*/ |
|
ecb9e6d29698
support for the Prism.js syntax highlighter -- via external Node.js process;
wenzelm
parents:
diff
changeset
|
10 |
|
|
ecb9e6d29698
support for the Prism.js syntax highlighter -- via external Node.js process;
wenzelm
parents:
diff
changeset
|
11 |
package isabelle |
|
ecb9e6d29698
support for the Prism.js syntax highlighter -- via external Node.js process;
wenzelm
parents:
diff
changeset
|
12 |
|
|
ecb9e6d29698
support for the Prism.js syntax highlighter -- via external Node.js process;
wenzelm
parents:
diff
changeset
|
13 |
|
|
77566
2a99fcb283ee
renamed administrative tools to build Isabelle components (unrelated to "isabelle build");
wenzelm
parents:
76621
diff
changeset
|
14 |
object Component_Prismjs {
|
|
76508
ecb9e6d29698
support for the Prism.js syntax highlighter -- via external Node.js process;
wenzelm
parents:
diff
changeset
|
15 |
/* build prismjs component */ |
|
ecb9e6d29698
support for the Prism.js syntax highlighter -- via external Node.js process;
wenzelm
parents:
diff
changeset
|
16 |
|
|
ecb9e6d29698
support for the Prism.js syntax highlighter -- via external Node.js process;
wenzelm
parents:
diff
changeset
|
17 |
val default_version = "1.29.0" |
|
ecb9e6d29698
support for the Prism.js syntax highlighter -- via external Node.js process;
wenzelm
parents:
diff
changeset
|
18 |
|
|
ecb9e6d29698
support for the Prism.js syntax highlighter -- via external Node.js process;
wenzelm
parents:
diff
changeset
|
19 |
def build_prismjs( |
|
ecb9e6d29698
support for the Prism.js syntax highlighter -- via external Node.js process;
wenzelm
parents:
diff
changeset
|
20 |
version: String = default_version, |
|
ecb9e6d29698
support for the Prism.js syntax highlighter -- via external Node.js process;
wenzelm
parents:
diff
changeset
|
21 |
target_dir: Path = Path.current, |
|
ecb9e6d29698
support for the Prism.js syntax highlighter -- via external Node.js process;
wenzelm
parents:
diff
changeset
|
22 |
progress: Progress = new Progress |
|
ecb9e6d29698
support for the Prism.js syntax highlighter -- via external Node.js process;
wenzelm
parents:
diff
changeset
|
23 |
): Unit = {
|
|
ecb9e6d29698
support for the Prism.js syntax highlighter -- via external Node.js process;
wenzelm
parents:
diff
changeset
|
24 |
Isabelle_System.require_command("npm", test = "help")
|
|
ecb9e6d29698
support for the Prism.js syntax highlighter -- via external Node.js process;
wenzelm
parents:
diff
changeset
|
25 |
|
|
ecb9e6d29698
support for the Prism.js syntax highlighter -- via external Node.js process;
wenzelm
parents:
diff
changeset
|
26 |
|
|
ecb9e6d29698
support for the Prism.js syntax highlighter -- via external Node.js process;
wenzelm
parents:
diff
changeset
|
27 |
/* component name */ |
|
ecb9e6d29698
support for the Prism.js syntax highlighter -- via external Node.js process;
wenzelm
parents:
diff
changeset
|
28 |
|
|
ecb9e6d29698
support for the Prism.js syntax highlighter -- via external Node.js process;
wenzelm
parents:
diff
changeset
|
29 |
val component = "prismjs-" + version |
| 76518 | 30 |
val component_dir = |
| 76547 | 31 |
Components.Directory(target_dir + Path.basic(component)).create(progress = progress) |
|
76508
ecb9e6d29698
support for the Prism.js syntax highlighter -- via external Node.js process;
wenzelm
parents:
diff
changeset
|
32 |
|
|
ecb9e6d29698
support for the Prism.js syntax highlighter -- via external Node.js process;
wenzelm
parents:
diff
changeset
|
33 |
|
|
ecb9e6d29698
support for the Prism.js syntax highlighter -- via external Node.js process;
wenzelm
parents:
diff
changeset
|
34 |
/* download */ |
|
ecb9e6d29698
support for the Prism.js syntax highlighter -- via external Node.js process;
wenzelm
parents:
diff
changeset
|
35 |
|
|
ecb9e6d29698
support for the Prism.js syntax highlighter -- via external Node.js process;
wenzelm
parents:
diff
changeset
|
36 |
Isabelle_System.with_tmp_dir("tmp") { tmp_dir =>
|
|
ecb9e6d29698
support for the Prism.js syntax highlighter -- via external Node.js process;
wenzelm
parents:
diff
changeset
|
37 |
Isabelle_System.bash("npm init -y && npm install prismjs@" + Bash.string(version),
|
|
ecb9e6d29698
support for the Prism.js syntax highlighter -- via external Node.js process;
wenzelm
parents:
diff
changeset
|
38 |
cwd = tmp_dir.file).check |
|
ecb9e6d29698
support for the Prism.js syntax highlighter -- via external Node.js process;
wenzelm
parents:
diff
changeset
|
39 |
Isabelle_System.copy_dir(tmp_dir + Path.explode("node_modules/prismjs"),
|
|
76621
7af197063e2f
clarified signature: copy directory content more directly;
wenzelm
parents:
76548
diff
changeset
|
40 |
component_dir.path, direct = true) |
|
76508
ecb9e6d29698
support for the Prism.js syntax highlighter -- via external Node.js process;
wenzelm
parents:
diff
changeset
|
41 |
} |
|
ecb9e6d29698
support for the Prism.js syntax highlighter -- via external Node.js process;
wenzelm
parents:
diff
changeset
|
42 |
|
|
ecb9e6d29698
support for the Prism.js syntax highlighter -- via external Node.js process;
wenzelm
parents:
diff
changeset
|
43 |
|
|
ecb9e6d29698
support for the Prism.js syntax highlighter -- via external Node.js process;
wenzelm
parents:
diff
changeset
|
44 |
/* settings */ |
|
ecb9e6d29698
support for the Prism.js syntax highlighter -- via external Node.js process;
wenzelm
parents:
diff
changeset
|
45 |
|
| 76548 | 46 |
component_dir.write_settings("""
|
|
76508
ecb9e6d29698
support for the Prism.js syntax highlighter -- via external Node.js process;
wenzelm
parents:
diff
changeset
|
47 |
ISABELLE_PRISMJS_HOME="$COMPONENT" |
|
ecb9e6d29698
support for the Prism.js syntax highlighter -- via external Node.js process;
wenzelm
parents:
diff
changeset
|
48 |
""") |
|
ecb9e6d29698
support for the Prism.js syntax highlighter -- via external Node.js process;
wenzelm
parents:
diff
changeset
|
49 |
|
|
ecb9e6d29698
support for the Prism.js syntax highlighter -- via external Node.js process;
wenzelm
parents:
diff
changeset
|
50 |
|
|
ecb9e6d29698
support for the Prism.js syntax highlighter -- via external Node.js process;
wenzelm
parents:
diff
changeset
|
51 |
/* README */ |
|
ecb9e6d29698
support for the Prism.js syntax highlighter -- via external Node.js process;
wenzelm
parents:
diff
changeset
|
52 |
|
| 76518 | 53 |
File.write(component_dir.README, |
|
76508
ecb9e6d29698
support for the Prism.js syntax highlighter -- via external Node.js process;
wenzelm
parents:
diff
changeset
|
54 |
"""This is Prism.js """ + version + """ from https://www.npmjs.com/package/prismjs |
|
ecb9e6d29698
support for the Prism.js syntax highlighter -- via external Node.js process;
wenzelm
parents:
diff
changeset
|
55 |
|
|
ecb9e6d29698
support for the Prism.js syntax highlighter -- via external Node.js process;
wenzelm
parents:
diff
changeset
|
56 |
|
|
ecb9e6d29698
support for the Prism.js syntax highlighter -- via external Node.js process;
wenzelm
parents:
diff
changeset
|
57 |
Makarius |
|
ecb9e6d29698
support for the Prism.js syntax highlighter -- via external Node.js process;
wenzelm
parents:
diff
changeset
|
58 |
""" + Date.Format.date(Date.now()) + "\n") |
|
ecb9e6d29698
support for the Prism.js syntax highlighter -- via external Node.js process;
wenzelm
parents:
diff
changeset
|
59 |
} |
|
ecb9e6d29698
support for the Prism.js syntax highlighter -- via external Node.js process;
wenzelm
parents:
diff
changeset
|
60 |
|
|
ecb9e6d29698
support for the Prism.js syntax highlighter -- via external Node.js process;
wenzelm
parents:
diff
changeset
|
61 |
|
|
ecb9e6d29698
support for the Prism.js syntax highlighter -- via external Node.js process;
wenzelm
parents:
diff
changeset
|
62 |
/* Isabelle tool wrapper */ |
|
ecb9e6d29698
support for the Prism.js syntax highlighter -- via external Node.js process;
wenzelm
parents:
diff
changeset
|
63 |
|
|
ecb9e6d29698
support for the Prism.js syntax highlighter -- via external Node.js process;
wenzelm
parents:
diff
changeset
|
64 |
val isabelle_tool = |
|
77566
2a99fcb283ee
renamed administrative tools to build Isabelle components (unrelated to "isabelle build");
wenzelm
parents:
76621
diff
changeset
|
65 |
Isabelle_Tool("component_prismjs", "build component for prismjs",
|
|
76508
ecb9e6d29698
support for the Prism.js syntax highlighter -- via external Node.js process;
wenzelm
parents:
diff
changeset
|
66 |
Scala_Project.here, |
|
ecb9e6d29698
support for the Prism.js syntax highlighter -- via external Node.js process;
wenzelm
parents:
diff
changeset
|
67 |
{ args =>
|
|
ecb9e6d29698
support for the Prism.js syntax highlighter -- via external Node.js process;
wenzelm
parents:
diff
changeset
|
68 |
var target_dir = Path.current |
|
ecb9e6d29698
support for the Prism.js syntax highlighter -- via external Node.js process;
wenzelm
parents:
diff
changeset
|
69 |
var version = default_version |
|
ecb9e6d29698
support for the Prism.js syntax highlighter -- via external Node.js process;
wenzelm
parents:
diff
changeset
|
70 |
|
|
ecb9e6d29698
support for the Prism.js syntax highlighter -- via external Node.js process;
wenzelm
parents:
diff
changeset
|
71 |
val getopts = Getopts("""
|
|
77566
2a99fcb283ee
renamed administrative tools to build Isabelle components (unrelated to "isabelle build");
wenzelm
parents:
76621
diff
changeset
|
72 |
Usage: isabelle component_prismjs [OPTIONS] |
|
76508
ecb9e6d29698
support for the Prism.js syntax highlighter -- via external Node.js process;
wenzelm
parents:
diff
changeset
|
73 |
|
|
ecb9e6d29698
support for the Prism.js syntax highlighter -- via external Node.js process;
wenzelm
parents:
diff
changeset
|
74 |
Options are: |
|
ecb9e6d29698
support for the Prism.js syntax highlighter -- via external Node.js process;
wenzelm
parents:
diff
changeset
|
75 |
-D DIR target directory (default ".") |
|
ecb9e6d29698
support for the Prism.js syntax highlighter -- via external Node.js process;
wenzelm
parents:
diff
changeset
|
76 |
-V VERSION version (default: """" + default_version + """") |
|
ecb9e6d29698
support for the Prism.js syntax highlighter -- via external Node.js process;
wenzelm
parents:
diff
changeset
|
77 |
|
|
ecb9e6d29698
support for the Prism.js syntax highlighter -- via external Node.js process;
wenzelm
parents:
diff
changeset
|
78 |
Build component for Prism.js. |
|
ecb9e6d29698
support for the Prism.js syntax highlighter -- via external Node.js process;
wenzelm
parents:
diff
changeset
|
79 |
""", |
|
ecb9e6d29698
support for the Prism.js syntax highlighter -- via external Node.js process;
wenzelm
parents:
diff
changeset
|
80 |
"D:" -> (arg => target_dir = Path.explode(arg)), |
|
ecb9e6d29698
support for the Prism.js syntax highlighter -- via external Node.js process;
wenzelm
parents:
diff
changeset
|
81 |
"V:" -> (arg => version = arg)) |
|
ecb9e6d29698
support for the Prism.js syntax highlighter -- via external Node.js process;
wenzelm
parents:
diff
changeset
|
82 |
|
|
ecb9e6d29698
support for the Prism.js syntax highlighter -- via external Node.js process;
wenzelm
parents:
diff
changeset
|
83 |
val more_args = getopts(args) |
|
ecb9e6d29698
support for the Prism.js syntax highlighter -- via external Node.js process;
wenzelm
parents:
diff
changeset
|
84 |
if (more_args.nonEmpty) getopts.usage() |
|
ecb9e6d29698
support for the Prism.js syntax highlighter -- via external Node.js process;
wenzelm
parents:
diff
changeset
|
85 |
|
|
ecb9e6d29698
support for the Prism.js syntax highlighter -- via external Node.js process;
wenzelm
parents:
diff
changeset
|
86 |
val progress = new Console_Progress() |
|
ecb9e6d29698
support for the Prism.js syntax highlighter -- via external Node.js process;
wenzelm
parents:
diff
changeset
|
87 |
|
|
ecb9e6d29698
support for the Prism.js syntax highlighter -- via external Node.js process;
wenzelm
parents:
diff
changeset
|
88 |
build_prismjs(version = version, target_dir = target_dir, progress = progress) |
|
ecb9e6d29698
support for the Prism.js syntax highlighter -- via external Node.js process;
wenzelm
parents:
diff
changeset
|
89 |
}) |
|
ecb9e6d29698
support for the Prism.js syntax highlighter -- via external Node.js process;
wenzelm
parents:
diff
changeset
|
90 |
} |