src/Pure/Admin/build_prismjs.scala
author wenzelm
Wed, 30 Nov 2022 21:53:55 +0100
changeset 76547 9fe5d8c70352
parent 76518 b30b8e23383c
child 76548 0af64cc2eee9
permissions -rw-r--r--
tuned signature;
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
76518
b30b8e23383c clarified signature: more explicit types;
wenzelm
parents: 76508
diff changeset
    40
      Isabelle_System.rm_tree(component_dir.path)
76508
ecb9e6d29698 support for the Prism.js syntax highlighter -- via external Node.js process;
wenzelm
parents:
diff changeset
    41
      Isabelle_System.copy_dir(tmp_dir + Path.explode("node_modules/prismjs"),
76518
b30b8e23383c clarified signature: more explicit types;
wenzelm
parents: 76508
diff changeset
    42
        component_dir.path)
b30b8e23383c clarified signature: more explicit types;
wenzelm
parents: 76508
diff changeset
    43
      Isabelle_System.make_directory(component_dir.etc)
76508
ecb9e6d29698 support for the Prism.js syntax highlighter -- via external Node.js process;
wenzelm
parents:
diff changeset
    44
    }
ecb9e6d29698 support for the Prism.js syntax highlighter -- via external Node.js process;
wenzelm
parents:
diff changeset
    45
ecb9e6d29698 support for the Prism.js syntax highlighter -- via external Node.js process;
wenzelm
parents:
diff changeset
    46
ecb9e6d29698 support for the Prism.js syntax highlighter -- via external Node.js process;
wenzelm
parents:
diff changeset
    47
    /* settings */
ecb9e6d29698 support for the Prism.js syntax highlighter -- via external Node.js process;
wenzelm
parents:
diff changeset
    48
76518
b30b8e23383c clarified signature: more explicit types;
wenzelm
parents: 76508
diff changeset
    49
    File.write(component_dir.settings,
76508
ecb9e6d29698 support for the Prism.js syntax highlighter -- via external Node.js process;
wenzelm
parents:
diff changeset
    50
      """# -*- shell-script -*- :mode=shellscript:
ecb9e6d29698 support for the Prism.js syntax highlighter -- via external Node.js process;
wenzelm
parents:
diff changeset
    51
ecb9e6d29698 support for the Prism.js syntax highlighter -- via external Node.js process;
wenzelm
parents:
diff changeset
    52
ISABELLE_PRISMJS_HOME="$COMPONENT"
ecb9e6d29698 support for the Prism.js syntax highlighter -- via external Node.js process;
wenzelm
parents:
diff changeset
    53
""")
ecb9e6d29698 support for the Prism.js syntax highlighter -- via external Node.js process;
wenzelm
parents:
diff changeset
    54
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
    /* README */
ecb9e6d29698 support for the Prism.js syntax highlighter -- via external Node.js process;
wenzelm
parents:
diff changeset
    57
76518
b30b8e23383c clarified signature: more explicit types;
wenzelm
parents: 76508
diff changeset
    58
    File.write(component_dir.README,
76508
ecb9e6d29698 support for the Prism.js syntax highlighter -- via external Node.js process;
wenzelm
parents:
diff changeset
    59
      """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
    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
        Makarius
ecb9e6d29698 support for the Prism.js syntax highlighter -- via external Node.js process;
wenzelm
parents:
diff changeset
    63
        """ + Date.Format.date(Date.now()) + "\n")
ecb9e6d29698 support for the Prism.js syntax highlighter -- via external Node.js process;
wenzelm
parents:
diff changeset
    64
  }
ecb9e6d29698 support for the Prism.js syntax highlighter -- via external Node.js process;
wenzelm
parents:
diff changeset
    65
ecb9e6d29698 support for the Prism.js syntax highlighter -- via external Node.js process;
wenzelm
parents:
diff changeset
    66
ecb9e6d29698 support for the Prism.js syntax highlighter -- via external Node.js process;
wenzelm
parents:
diff changeset
    67
  /* Isabelle tool wrapper */
ecb9e6d29698 support for the Prism.js syntax highlighter -- via external Node.js process;
wenzelm
parents:
diff changeset
    68
ecb9e6d29698 support for the Prism.js syntax highlighter -- via external Node.js process;
wenzelm
parents:
diff changeset
    69
  val isabelle_tool =
ecb9e6d29698 support for the Prism.js syntax highlighter -- via external Node.js process;
wenzelm
parents:
diff changeset
    70
    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
    71
      Scala_Project.here,
ecb9e6d29698 support for the Prism.js syntax highlighter -- via external Node.js process;
wenzelm
parents:
diff changeset
    72
      { args =>
ecb9e6d29698 support for the Prism.js syntax highlighter -- via external Node.js process;
wenzelm
parents:
diff changeset
    73
        var target_dir = Path.current
ecb9e6d29698 support for the Prism.js syntax highlighter -- via external Node.js process;
wenzelm
parents:
diff changeset
    74
        var version = default_version
ecb9e6d29698 support for the Prism.js syntax highlighter -- via external Node.js process;
wenzelm
parents:
diff changeset
    75
ecb9e6d29698 support for the Prism.js syntax highlighter -- via external Node.js process;
wenzelm
parents:
diff changeset
    76
        val getopts = Getopts("""
ecb9e6d29698 support for the Prism.js syntax highlighter -- via external Node.js process;
wenzelm
parents:
diff changeset
    77
Usage: isabelle build_prismjs [OPTIONS]
ecb9e6d29698 support for the Prism.js syntax highlighter -- via external Node.js process;
wenzelm
parents:
diff changeset
    78
ecb9e6d29698 support for the Prism.js syntax highlighter -- via external Node.js process;
wenzelm
parents:
diff changeset
    79
  Options are:
ecb9e6d29698 support for the Prism.js syntax highlighter -- via external Node.js process;
wenzelm
parents:
diff changeset
    80
    -D DIR       target directory (default ".")
ecb9e6d29698 support for the Prism.js syntax highlighter -- via external Node.js process;
wenzelm
parents:
diff changeset
    81
    -V VERSION   version (default: """" + default_version + """")
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
  Build component for Prism.js.
ecb9e6d29698 support for the Prism.js syntax highlighter -- via external Node.js process;
wenzelm
parents:
diff changeset
    84
""",
ecb9e6d29698 support for the Prism.js syntax highlighter -- via external Node.js process;
wenzelm
parents:
diff changeset
    85
          "D:" -> (arg => target_dir = Path.explode(arg)),
ecb9e6d29698 support for the Prism.js syntax highlighter -- via external Node.js process;
wenzelm
parents:
diff changeset
    86
          "V:" -> (arg => version = arg))
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
        val more_args = getopts(args)
ecb9e6d29698 support for the Prism.js syntax highlighter -- via external Node.js process;
wenzelm
parents:
diff changeset
    89
        if (more_args.nonEmpty) getopts.usage()
ecb9e6d29698 support for the Prism.js syntax highlighter -- via external Node.js process;
wenzelm
parents:
diff changeset
    90
ecb9e6d29698 support for the Prism.js syntax highlighter -- via external Node.js process;
wenzelm
parents:
diff changeset
    91
        val progress = new Console_Progress()
ecb9e6d29698 support for the Prism.js syntax highlighter -- via external Node.js process;
wenzelm
parents:
diff changeset
    92
ecb9e6d29698 support for the Prism.js syntax highlighter -- via external Node.js process;
wenzelm
parents:
diff changeset
    93
        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
    94
      })
ecb9e6d29698 support for the Prism.js syntax highlighter -- via external Node.js process;
wenzelm
parents:
diff changeset
    95
}