src/Pure/System/isabelle_tool.scala
author wenzelm
Wed Oct 19 17:03:44 2016 +0200 (2016-10-19)
changeset 64311 3d5e7719e878
parent 64304 96bc94c87a81
child 64369 6a9816764b37
permissions -rw-r--r--
proper isabelle tool in Scala;
     1 /*  Title:      Pure/System/isabelle_tool.scala
     2     Author:     Makarius
     3     Author:     Lars Hupel
     4 
     5 Isabelle system tools: external executables or internal Scala functions.
     6 */
     7 
     8 package isabelle
     9 
    10 import java.net.URLClassLoader
    11 import scala.reflect.runtime.universe
    12 import scala.tools.reflect.{ToolBox,ToolBoxError}
    13 
    14 
    15 object Isabelle_Tool
    16 {
    17   /* Scala source tools */
    18 
    19   abstract class Body extends Function[List[String], Unit]
    20 
    21   private def compile(path: Path): Body =
    22   {
    23     def err(msg: String): Nothing =
    24       cat_error(msg, "The error(s) above occurred in Isabelle/Scala tool " + path)
    25 
    26     val source = File.read(path)
    27 
    28     val class_loader = new URLClassLoader(Array(), getClass.getClassLoader)
    29     val tool_box = universe.runtimeMirror(class_loader).mkToolBox()
    30 
    31     try {
    32       val symbol = tool_box.parse(source) match {
    33         case tree: universe.ModuleDef => tool_box.define(tree)
    34         case _ => err("Source does not describe a module (Scala object)")
    35       }
    36       tool_box.compile(universe.Ident(symbol))() match {
    37         case body: Body => body
    38         case _ => err("Ill-typed source: Isabelle_Tool.Body expected")
    39       }
    40     }
    41     catch {
    42       case e: ToolBoxError =>
    43         if (tool_box.frontEnd.hasErrors) {
    44           val infos = tool_box.frontEnd.infos.toList
    45           val msgs = infos.map(info => "Error in line " + info.pos.line + ":\n" + info.msg)
    46           err(msgs.mkString("\n"))
    47         }
    48         else
    49           err(e.toString)
    50     }
    51   }
    52 
    53 
    54   /* external tools */
    55 
    56   private def dirs(): List[Path] = Path.split(Isabelle_System.getenv_strict("ISABELLE_TOOLS"))
    57 
    58   private def is_external(dir: Path, file_name: String): Boolean =
    59   {
    60     val file = (dir + Path.basic(file_name)).file
    61     try {
    62       file.isFile && file.canRead &&
    63         (file_name.endsWith(".scala") || file.canExecute) &&
    64         !file_name.endsWith("~") && !file_name.endsWith(".orig")
    65     }
    66     catch { case _: SecurityException => false }
    67   }
    68 
    69   private def list_external(): List[(String, String)] =
    70   {
    71     val Description = """.*\bDESCRIPTION: *(.*)""".r
    72     for {
    73       dir <- dirs() if dir.is_dir
    74       file_name <- File.read_dir(dir) if is_external(dir, file_name)
    75     } yield {
    76       val source = File.read(dir + Path.basic(file_name))
    77       val name = Library.try_unsuffix(".scala", file_name) getOrElse file_name
    78       val description =
    79         split_lines(source).collectFirst({ case Description(s) => s }) getOrElse ""
    80       (name, description)
    81     }
    82   }
    83 
    84   private def find_external(name: String): Option[List[String] => Unit] =
    85     dirs.collectFirst({
    86       case dir if is_external(dir, name + ".scala") =>
    87         compile(dir + Path.basic(name + ".scala"))
    88       case dir if is_external(dir, name) =>
    89         (args: List[String]) =>
    90           {
    91             val tool = dir + Path.basic(name)
    92             val result = Isabelle_System.bash(File.bash_path(tool) + " " + Bash.strings(args))
    93             sys.exit(result.print_stdout.rc)
    94           }
    95     })
    96 
    97 
    98   /* internal tools */
    99 
   100   private val internal_tools: List[Isabelle_Tool] =
   101     List(
   102       Build.isabelle_tool,
   103       Build_Doc.isabelle_tool,
   104       Build_Stats.isabelle_tool,
   105       Check_Sources.isabelle_tool,
   106       Doc.isabelle_tool,
   107       ML_Process.isabelle_tool,
   108       Options.isabelle_tool,
   109       Profiling_Report.isabelle_tool,
   110       Remote_DMG.isabelle_tool,
   111       Update_Cartouches.isabelle_tool,
   112       Update_Header.isabelle_tool,
   113       Update_Then.isabelle_tool,
   114       Update_Theorems.isabelle_tool)
   115 
   116   private def list_internal(): List[(String, String)] =
   117     for (tool <- internal_tools.toList if tool.accessible)
   118       yield (tool.name, tool.description)
   119 
   120   private def find_internal(name: String): Option[List[String] => Unit] =
   121     internal_tools.collectFirst({
   122       case tool if tool.name == name && tool.accessible =>
   123         args => Command_Line.tool0 { tool.body(args) }
   124       })
   125 
   126 
   127   /* command line entry point */
   128 
   129   def main(args: Array[String])
   130   {
   131     Command_Line.tool0 {
   132       args.toList match {
   133         case Nil | List("-?") =>
   134           val tool_descriptions =
   135             (list_external() ::: list_internal()).sortBy(_._1).
   136               map({ case (a, "") => a case (a, b) => a + " - " + b })
   137           Getopts("""
   138 Usage: isabelle TOOL [ARGS ...]
   139 
   140   Start Isabelle TOOL with ARGS; pass "-?" for tool-specific help.
   141 
   142 Available tools:""" + tool_descriptions.mkString("\n  ", "\n  ", "\n")).usage
   143         case tool_name :: tool_args =>
   144           find_external(tool_name) orElse find_internal(tool_name) match {
   145             case Some(tool) => tool(tool_args)
   146             case None => error("Unknown Isabelle tool: " + quote(tool_name))
   147           }
   148       }
   149     }
   150   }
   151 }
   152 
   153 sealed case class Isabelle_Tool(
   154   name: String, description: String, body: List[String] => Unit, admin: Boolean = false)
   155 {
   156   def accessible: Boolean = !admin || Isabelle_System.admin()
   157 }