| author | wenzelm | 
| Tue, 28 Jan 2025 13:42:40 +0100 | |
| changeset 82007 | 04c704a6b193 | 
| parent 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),
 | 
| 
80224
 
db92e0b6a11a
clarified signature: prefer symbolic isabelle.Path over physical java.io.File;
 
wenzelm 
parents: 
77566 
diff
changeset
 | 
38  | 
cwd = tmp_dir).check  | 
| 
76508
 
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  | 
}  |