25 |
25 |
26 |
26 |
27 /* component name */ |
27 /* component name */ |
28 |
28 |
29 val component = "prismjs-" + version |
29 val component = "prismjs-" + version |
30 val component_dir = Isabelle_System.new_directory(target_dir + Path.basic(component)) |
30 val component_dir = |
31 progress.echo("Component " + component_dir) |
31 Components.Directory.create(target_dir + Path.basic(component), progress = progress) |
32 |
32 |
33 |
33 |
34 /* download */ |
34 /* download */ |
35 |
35 |
36 Isabelle_System.with_tmp_dir("tmp") { tmp_dir => |
36 Isabelle_System.with_tmp_dir("tmp") { tmp_dir => |
37 Isabelle_System.bash("npm init -y && npm install prismjs@" + Bash.string(version), |
37 Isabelle_System.bash("npm init -y && npm install prismjs@" + Bash.string(version), |
38 cwd = tmp_dir.file).check |
38 cwd = tmp_dir.file).check |
39 |
39 |
40 component_dir.file.delete() |
40 Isabelle_System.rm_tree(component_dir.path) |
41 Isabelle_System.copy_dir(tmp_dir + Path.explode("node_modules/prismjs"), |
41 Isabelle_System.copy_dir(tmp_dir + Path.explode("node_modules/prismjs"), |
42 component_dir) |
42 component_dir.path) |
|
43 Isabelle_System.make_directory(component_dir.etc) |
43 } |
44 } |
44 |
45 |
45 |
46 |
46 /* settings */ |
47 /* settings */ |
47 |
48 |
48 val etc_dir = Isabelle_System.make_directory(component_dir + Path.basic("etc")) |
49 File.write(component_dir.settings, |
49 File.write(etc_dir + Path.basic("settings"), |
|
50 """# -*- shell-script -*- :mode=shellscript: |
50 """# -*- shell-script -*- :mode=shellscript: |
51 |
51 |
52 ISABELLE_PRISMJS_HOME="$COMPONENT" |
52 ISABELLE_PRISMJS_HOME="$COMPONENT" |
53 """) |
53 """) |
54 |
54 |
55 |
55 |
56 /* README */ |
56 /* README */ |
57 |
57 |
58 File.write(component_dir + Path.basic("README"), |
58 File.write(component_dir.README, |
59 """This is Prism.js """ + version + """ from https://www.npmjs.com/package/prismjs |
59 """This is Prism.js """ + version + """ from https://www.npmjs.com/package/prismjs |
60 |
60 |
61 |
61 |
62 Makarius |
62 Makarius |
63 """ + Date.Format.date(Date.now()) + "\n") |
63 """ + Date.Format.date(Date.now()) + "\n") |