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