src/Pure/Admin/build_prismjs.scala
author wenzelm
Tue, 24 Jan 2023 21:27:10 +0100
changeset 77085 351eee493580
parent 76621 7af197063e2f
permissions -rw-r--r--
more robust locations (amending 7e11e96a922d) --- notably for cleanup() in build_release, after Admin/ been deleted;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
76508
ecb9e6d29698 support for the Prism.js syntax highlighter -- via external Node.js process;
wenzelm
parents:
diff changeset
     1
/*  Title:      Pure/Admin/build_prismjs.scala
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
ecb9e6d29698 support for the Prism.js syntax highlighter -- via external Node.js process;
wenzelm
parents:
diff changeset
    14
object Build_Prismjs {
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
b30b8e23383c clarified signature: more explicit types;
wenzelm
parents: 76508
diff changeset
    30
    val component_dir =
76547
9fe5d8c70352 tuned signature;
wenzelm
parents: 76518
diff changeset
    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
0af64cc2eee9 tuned signature;
wenzelm
parents: 76547
diff changeset
    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
b30b8e23383c clarified signature: more explicit types;
wenzelm
parents: 76508
diff changeset
    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 =
ecb9e6d29698 support for the Prism.js syntax highlighter -- via external Node.js process;
wenzelm
parents:
diff changeset
    65
    Isabelle_Tool("build_prismjs", "build component for prismjs",
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("""
ecb9e6d29698 support for the Prism.js syntax highlighter -- via external Node.js process;
wenzelm
parents:
diff changeset
    72
Usage: isabelle build_prismjs [OPTIONS]
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
}