src/Pure/System/isabelle_tool.scala

support for Dotnet / Fsharp platform, via dynamically installed Isabelle component;

/*  Title:      Pure/System/isabelle_tool.scala
    Author:     Makarius

Isabelle system tools: external executables or internal Scala functions.
*/

package isabelle


object Isabelle_Tool {
  /* external tools */

  private def dirs(): List[Path] = Path.split(Isabelle_System.getenv_strict("ISABELLE_TOOLS"))

  private def is_external(dir: Path, name: String): Boolean = {
    val file = (dir + Path.explode(name)).file
    try { file.isFile && file.canRead && file.canExecute && !File.is_backup(name) }
    catch { case _: SecurityException => false }
  }

  private def find_external(name: String): Option[List[String] => Unit] =
    dirs().collectFirst(
      {
        case dir if is_external(dir, name) =>
          { (args: List[String]) =>
            val tool = dir + Path.explode(name)
            val result = Isabelle_System.bash(File.bash_path(tool) + " " + Bash.strings(args))
            sys.exit(result.print_stdout.rc)
          }
      })


  /* internal tools */

  private lazy val internal_tools: List[Isabelle_Tool] =
    Isabelle_System.make_services(classOf[Isabelle_Scala_Tools]).flatMap(_.tools)

  private def find_internal(name: String): Option[List[String] => Unit] =
    internal_tools.collectFirst({
      case tool if tool.name == name =>
        args => Command_Line.tool { tool.body(args) }
      })


  /* list tools */

  abstract class Entry {
    def name: String
    def position: Properties.T
    def description: String
    def print: String =
      description match {
        case "" => name
        case descr => name + " - " + descr
      }
  }

  sealed case class External(name: String, path: Path) extends Entry {
    def position: Properties.T = Position.File(path.absolute.implode)
    def description: String = {
      val Pattern = """.*\bDESCRIPTION: *(.*)""".r
      split_lines(File.read(path)).collectFirst({ case Pattern(s) => s }) getOrElse ""
    }
  }

  def external_tools(): List[External] = {
    for {
      dir <- dirs() if dir.is_dir
      name <- File.read_dir(dir) if is_external(dir, name)
    } yield External(name, dir + Path.explode(name))
  }

  def isabelle_tools(): List[Entry] =
    (external_tools() ::: internal_tools).sortBy(_.name)

  object Isabelle_Tools extends Scala.Fun_String("isabelle_tools") {
    val here = Scala_Project.here
    def apply(arg: String): String =
      if (arg.nonEmpty) error("Bad argument: " + quote(arg))
      else {
        val result = isabelle_tools().map(entry => (entry.name, entry.position))
        val body = { import XML.Encode._; list(pair(string, properties))(result) }
        YXML.string_of_body(body)
      }
  }


  /* command line entry point */

  def main(args: Array[String]): Unit = {
    Command_Line.tool {
      args.toList match {
        case Nil | List("-?") =>
          val tool_descriptions = isabelle_tools().map(_.print)
          Getopts("""
Usage: isabelle TOOL [ARGS ...]

  Start Isabelle TOOL with ARGS; pass "-?" for tool-specific help.

Available tools:""" + tool_descriptions.mkString("\n  ", "\n  ", "\n")).usage()
        case tool_name :: tool_args =>
          find_external(tool_name) orElse find_internal(tool_name) match {
            case Some(tool) => tool(tool_args)
            case None => error("Unknown Isabelle tool: " + quote(tool_name))
          }
      }
    }
  }
}

sealed case class Isabelle_Tool(
  name: String,
  description: String,
  here: Scala_Project.Here,
  body: List[String] => Unit
) extends Isabelle_Tool.Entry {
  def position: Position.T = here.position
}

class Isabelle_Scala_Tools(val tools: Isabelle_Tool*) extends Isabelle_System.Service

class Tools extends Isabelle_Scala_Tools(
  Build.isabelle_tool,
  Build_Docker.isabelle_tool,
  Build_Job.isabelle_tool,
  CI_Build.isabelle_tool,
  Doc.isabelle_tool,
  Document_Build.isabelle_tool,
  Dump.isabelle_tool,
  Export.isabelle_tool,
  ML_Process.isabelle_tool,
  Mercurial.isabelle_tool1,
  Mercurial.isabelle_tool2,
  Mkroot.isabelle_tool,
  Logo.isabelle_tool,
  Options.isabelle_tool,
  Phabricator.isabelle_tool1,
  Phabricator.isabelle_tool2,
  Phabricator.isabelle_tool3,
  Phabricator.isabelle_tool4,
  Profiling_Report.isabelle_tool,
  Server.isabelle_tool,
  Sessions.isabelle_tool,
  Scala_Project.isabelle_tool,
  Sync.isabelle_tool,
  Update.isabelle_tool,
  Update_Cartouches.isabelle_tool,
  Update_Comments.isabelle_tool,
  Update_Header.isabelle_tool,
  Update_Then.isabelle_tool,
  Update_Theorems.isabelle_tool,
  isabelle.mirabelle.Mirabelle.isabelle_tool,
  isabelle.vscode.Language_Server.isabelle_tool,
  isabelle.vscode.VSCode_Main.isabelle_tool)

class Admin_Tools extends Isabelle_Scala_Tools(
  Build_CSDP.isabelle_tool,
  Build_CVC5.isabelle_tool,
  Build_Cygwin.isabelle_tool,
  Build_Doc.isabelle_tool,
  Build_E.isabelle_tool,
  Build_Easychair.isabelle_tool,
  Build_Foiltex.isabelle_tool,
  Build_Fonts.isabelle_tool,
  Build_JCEF.isabelle_tool,
  Build_JDK.isabelle_tool,
  Build_JEdit.isabelle_tool,
  Build_LIPIcs.isabelle_tool,
  Build_LLNCS.isabelle_tool,
  Build_Minisat.isabelle_tool,
  Build_PDFjs.isabelle_tool,
  Build_PolyML.isabelle_tool1,
  Build_PolyML.isabelle_tool2,
  Build_PostgreSQL.isabelle_tool,
  Build_SPASS.isabelle_tool,
  Build_SQLite.isabelle_tool,
  Build_Scala.isabelle_tool,
  Build_Status.isabelle_tool,
  Build_Vampire.isabelle_tool,
  Build_VeriT.isabelle_tool,
  Build_Zipperposition.isabelle_tool,
  Build_Zstd.isabelle_tool,
  Check_Sources.isabelle_tool,
  Components.isabelle_tool,
  Dotnet_Setup.isabelle_tool,
  isabelle.vscode.Build_VSCode.isabelle_tool,
  isabelle.vscode.Build_VSCodium.isabelle_tool1,
  isabelle.vscode.Build_VSCodium.isabelle_tool2)