src/Pure/System/isabelle_tool.scala
author wenzelm
Tue Apr 12 15:00:26 2016 +0200 (2016-04-12)
changeset 62960 cfbb6a5b427c
parent 62838 c91ca9935280
child 63226 d8884c111bca
permissions -rw-r--r--
simplified -- avoid odd mutable state, which potentially causes problems with module initialization;
wenzelm@62829
     1
/*  Title:      Pure/System/isabelle_tool.scala
wenzelm@62829
     2
    Author:     Makarius
wenzelm@62829
     3
wenzelm@62829
     4
Isabelle system tools: external executables or internal Scala functions.
wenzelm@62829
     5
*/
wenzelm@62829
     6
wenzelm@62829
     7
package isabelle
wenzelm@62829
     8
wenzelm@62829
     9
wenzelm@62829
    10
object Isabelle_Tool
wenzelm@62829
    11
{
wenzelm@62829
    12
  /* external tools */
wenzelm@62829
    13
wenzelm@62829
    14
  private def dirs(): List[Path] = Path.split(Isabelle_System.getenv_strict("ISABELLE_TOOLS"))
wenzelm@62829
    15
wenzelm@62829
    16
  private def is_external(dir: Path, name: String): Boolean =
wenzelm@62829
    17
  {
wenzelm@62829
    18
    val file = (dir + Path.basic(name)).file
wenzelm@62829
    19
    try {
wenzelm@62829
    20
      file.isFile && file.canRead && file.canExecute &&
wenzelm@62829
    21
        !name.endsWith("~") && !name.endsWith(".orig")
wenzelm@62829
    22
    }
wenzelm@62829
    23
    catch { case _: SecurityException => false }
wenzelm@62829
    24
  }
wenzelm@62829
    25
wenzelm@62830
    26
  private def list_external(): List[(String, String)] =
wenzelm@62829
    27
  {
wenzelm@62830
    28
    val Description = """.*\bDESCRIPTION: *(.*)""".r
wenzelm@62830
    29
    for {
wenzelm@62830
    30
      dir <- dirs() if dir.is_dir
wenzelm@62830
    31
      name <- File.read_dir(dir) if is_external(dir, name)
wenzelm@62830
    32
    } yield {
wenzelm@62830
    33
      val source = File.read(dir + Path.basic(name))
wenzelm@62830
    34
      val description =
wenzelm@62830
    35
        split_lines(source).collectFirst({ case Description(s) => s }) getOrElse ""
wenzelm@62830
    36
      (name, description)
wenzelm@62830
    37
    }
wenzelm@62829
    38
  }
wenzelm@62829
    39
wenzelm@62829
    40
  private def find_external(name: String): Option[List[String] => Unit] =
wenzelm@62830
    41
    dirs.collectFirst({ case dir if is_external(dir, name) =>
wenzelm@62830
    42
      (args: List[String]) =>
wenzelm@62830
    43
        {
wenzelm@62830
    44
          val tool = dir + Path.basic(name)
wenzelm@62830
    45
          val result = Isabelle_System.bash(File.bash_path(tool) + " " + File.bash_args(args))
wenzelm@62830
    46
          sys.exit(result.print_stdout.rc)
wenzelm@62830
    47
        }
wenzelm@62830
    48
    })
wenzelm@62830
    49
wenzelm@62830
    50
wenzelm@62830
    51
  /* internal tools */
wenzelm@62830
    52
wenzelm@62960
    53
  private val internal_tools: List[Isabelle_Tool] =
wenzelm@62960
    54
    List(
wenzelm@62960
    55
      Build.isabelle_tool,
wenzelm@62960
    56
      Build_Doc.isabelle_tool,
wenzelm@62960
    57
      Check_Sources.isabelle_tool,
wenzelm@62960
    58
      Doc.isabelle_tool,
wenzelm@62960
    59
      ML_Process.isabelle_tool,
wenzelm@62960
    60
      Options.isabelle_tool,
wenzelm@62960
    61
      Update_Cartouches.isabelle_tool,
wenzelm@62960
    62
      Update_Header.isabelle_tool,
wenzelm@62960
    63
      Update_Then.isabelle_tool,
wenzelm@62960
    64
      Update_Theorems.isabelle_tool)
wenzelm@62830
    65
wenzelm@62830
    66
  private def list_internal(): List[(String, String)] =
wenzelm@62960
    67
    for (tool <- internal_tools.toList) yield (tool.name, tool.description)
wenzelm@62830
    68
wenzelm@62830
    69
  private def find_internal(name: String): Option[List[String] => Unit] =
wenzelm@62960
    70
    internal_tools.collectFirst({
wenzelm@62960
    71
      case tool if tool.name == name =>
wenzelm@62960
    72
        args => Command_Line.tool0 { tool.body(args) }
wenzelm@62960
    73
      })
wenzelm@62831
    74
wenzelm@62829
    75
wenzelm@62829
    76
  /* command line entry point */
wenzelm@62829
    77
wenzelm@62829
    78
  def main(args: Array[String])
wenzelm@62829
    79
  {
wenzelm@62829
    80
    Command_Line.tool0 {
wenzelm@62829
    81
      args.toList match {
wenzelm@62829
    82
        case Nil | List("-?") =>
wenzelm@62830
    83
          val tool_descriptions =
wenzelm@62830
    84
            (list_external() ::: list_internal()).sortBy(_._1).
wenzelm@62830
    85
              map({ case (a, "") => a case (a, b) => a + " - " + b })
wenzelm@62829
    86
          Getopts("""
wenzelm@62829
    87
Usage: isabelle TOOL [ARGS ...]
wenzelm@62829
    88
wenzelm@62829
    89
  Start Isabelle TOOL with ARGS; pass "-?" for tool-specific help.
wenzelm@62829
    90
wenzelm@62829
    91
Available tools:""" + tool_descriptions.mkString("\n  ", "\n  ", "\n")).usage
wenzelm@62829
    92
        case tool_name :: tool_args =>
wenzelm@62830
    93
          find_external(tool_name) orElse find_internal(tool_name) match {
wenzelm@62830
    94
            case Some(tool) => tool(tool_args)
wenzelm@62829
    95
            case None => error("Unknown Isabelle tool: " + quote(tool_name))
wenzelm@62829
    96
          }
wenzelm@62829
    97
      }
wenzelm@62829
    98
    }
wenzelm@62829
    99
  }
wenzelm@62829
   100
}
wenzelm@62830
   101
wenzelm@62830
   102
sealed case class Isabelle_Tool(name: String, description: String, body: List[String] => Unit)