| author | nipkow | 
| Fri, 23 Aug 2024 18:40:12 +0200 | |
| changeset 80738 | 6adf6cc82013 | 
| parent 80224 | db92e0b6a11a | 
| permissions | -rw-r--r-- | 
| 77566 
2a99fcb283ee
renamed administrative tools to build Isabelle components (unrelated to "isabelle build");
 wenzelm parents: 
76621diff
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: 
76621diff
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: 
77566diff
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: 
76548diff
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: 
76621diff
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: 
76621diff
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 | } |