src/Tools/VSCode/src/build_vscode.scala
author wenzelm
Sat, 10 Nov 2018 14:08:02 +0100
changeset 69277 258bef08b31e
parent 66976 806bc39550a5
child 71726 a5fda30edae2
permissions -rw-r--r--
support for user-defined Isabelle/Scala command-line tools; misc tuning and clarification;

/*  Title:      Tools/VSCode/src/build_vscode.scala
    Author:     Makarius

Build VSCode configuration and extension module for Isabelle.
*/

package isabelle.vscode


import isabelle._


object Build_VSCode
{
  val extension_dir = Path.explode("~~/src/Tools/VSCode/extension")


  /* grammar */

  def build_grammar(options: Options, progress: Progress = No_Progress)
  {
    val logic = Grammar.default_logic
    val keywords = Sessions.base_info(options, logic).check_base.overall_syntax.keywords

    val output_path = extension_dir + Path.explode(Grammar.default_output(logic))
    progress.echo(output_path.implode)
    File.write_backup(output_path, Grammar.generate(keywords))
  }


  /* extension */

  def build_extension(progress: Progress = No_Progress, publish: Boolean = false)
  {
    val output_path = extension_dir + Path.explode("out")
    progress.echo(output_path.implode)

    progress.bash(
      "npm install && npm update --dev && vsce package" + (if (publish) " && vsce publish" else ""),
      cwd = extension_dir.file, echo = true).check
  }


  /* Isabelle tool wrapper */

  val isabelle_tool =
    Isabelle_Tool("build_vscode", "build Isabelle/VSCode extension module", args =>
    {
      var publish = false

      val getopts = Getopts("""
Usage: isabelle build_vscode

  Options are:
    -P           publish the package

Build Isabelle/VSCode extension module in directory
""" + extension_dir.expand + """

This requires npm and the vsce build and publishing tool, see also
https://code.visualstudio.com/docs/tools/vscecli
""",
        "P" -> (_ => publish = true))

      val more_args = getopts(args)
      if (more_args.nonEmpty) getopts.usage()

      val options = Options.init()
      val progress = new Console_Progress()

      build_grammar(options, progress)
      build_extension(progress, publish = publish)
    })
}