src/Pure/System/isabelle_tool.scala
author wenzelm
Sun Apr 03 23:01:39 2016 +0200 (2016-04-03)
changeset 62836 98dbed6cfa44
parent 62835 1a9ce1b13b20
child 62838 c91ca9935280
permissions -rw-r--r--
prefer internal tool;
     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 var internal_tools = Map.empty[String, (String, List[String] => Nothing)]
    54 
    55   private def list_internal(): List[(String, String)] =
    56     synchronized {
    57       for ((name, (description, _)) <- internal_tools.toList) yield (name, description)
    58     }
    59 
    60   private def find_internal(name: String): Option[List[String] => Unit] =
    61     synchronized { internal_tools.get(name).map(_._2) }
    62 
    63   private def register(isabelle_tool: Isabelle_Tool): Unit =
    64     synchronized {
    65       internal_tools +=
    66         (isabelle_tool.name ->
    67           (isabelle_tool.description,
    68             args => Command_Line.tool0 { isabelle_tool.body(args) }))
    69     }
    70 
    71   register(Build.isabelle_tool)
    72   register(Check_Sources.isabelle_tool)
    73   register(Doc.isabelle_tool)
    74   register(ML_Process.isabelle_tool)
    75   register(Options.isabelle_tool)
    76   register(Update_Cartouches.isabelle_tool)
    77   register(Update_Header.isabelle_tool)
    78   register(Update_Then.isabelle_tool)
    79   register(Update_Theorems.isabelle_tool)
    80 
    81 
    82   /* command line entry point */
    83 
    84   def main(args: Array[String])
    85   {
    86     Command_Line.tool0 {
    87       args.toList match {
    88         case Nil | List("-?") =>
    89           val tool_descriptions =
    90             (list_external() ::: list_internal()).sortBy(_._1).
    91               map({ case (a, "") => a case (a, b) => a + " - " + b })
    92           Getopts("""
    93 Usage: isabelle TOOL [ARGS ...]
    94 
    95   Start Isabelle TOOL with ARGS; pass "-?" for tool-specific help.
    96 
    97 Available tools:""" + tool_descriptions.mkString("\n  ", "\n  ", "\n")).usage
    98         case tool_name :: tool_args =>
    99           find_external(tool_name) orElse find_internal(tool_name) match {
   100             case Some(tool) => tool(tool_args)
   101             case None => error("Unknown Isabelle tool: " + quote(tool_name))
   102           }
   103       }
   104     }
   105   }
   106 }
   107 
   108 sealed case class Isabelle_Tool(name: String, description: String, body: List[String] => Unit)