src/Pure/System/isabelle_tool.scala
changeset 63226 d8884c111bca
parent 62960 cfbb6a5b427c
child 63519 78401d628718
     1.1 --- a/src/Pure/System/isabelle_tool.scala	Thu Jun 02 17:47:47 2016 +0200
     1.2 +++ b/src/Pure/System/isabelle_tool.scala	Fri Jun 03 22:27:01 2016 +0200
     1.3 @@ -1,24 +1,58 @@
     1.4  /*  Title:      Pure/System/isabelle_tool.scala
     1.5      Author:     Makarius
     1.6 +    Author:     Lars Hupel
     1.7  
     1.8  Isabelle system tools: external executables or internal Scala functions.
     1.9  */
    1.10  
    1.11  package isabelle
    1.12  
    1.13 +import java.net.URLClassLoader
    1.14 +import scala.reflect.runtime.universe
    1.15 +import scala.tools.reflect.{ToolBox,ToolBoxError}
    1.16 +
    1.17  
    1.18  object Isabelle_Tool
    1.19  {
    1.20 +  /* Scala source tools */
    1.21 +
    1.22 +  abstract class Body extends Function[List[String], Unit]
    1.23 +
    1.24 +  private def compile(path: Path): Body =
    1.25 +  {
    1.26 +    def err(msg: String): Nothing =
    1.27 +      cat_error(msg, "The error(s) above occurred in Isabelle/Scala tool " + path)
    1.28 +
    1.29 +    val source = File.read(path)
    1.30 +
    1.31 +    val class_loader = new URLClassLoader(Array(), getClass.getClassLoader)
    1.32 +    val tool_box = universe.runtimeMirror(class_loader).mkToolBox()
    1.33 +
    1.34 +    try {
    1.35 +      val symbol = tool_box.parse(source) match {
    1.36 +        case tree: universe.ModuleDef => tool_box.define(tree)
    1.37 +        case _ => err("Source does not describe a module (Scala object)")
    1.38 +      }
    1.39 +      tool_box.compile(universe.Ident(symbol))() match {
    1.40 +        case body: Body => body
    1.41 +        case _ => err("Ill-typed source: Isabelle_Tool.Body expected")
    1.42 +      }
    1.43 +    }
    1.44 +    catch { case e: ToolBoxError => err(e.toString) }
    1.45 +  }
    1.46 +
    1.47 +
    1.48    /* external tools */
    1.49  
    1.50    private def dirs(): List[Path] = Path.split(Isabelle_System.getenv_strict("ISABELLE_TOOLS"))
    1.51  
    1.52 -  private def is_external(dir: Path, name: String): Boolean =
    1.53 +  private def is_external(dir: Path, file_name: String): Boolean =
    1.54    {
    1.55 -    val file = (dir + Path.basic(name)).file
    1.56 +    val file = (dir + Path.basic(file_name)).file
    1.57      try {
    1.58 -      file.isFile && file.canRead && file.canExecute &&
    1.59 -        !name.endsWith("~") && !name.endsWith(".orig")
    1.60 +      file.isFile && file.canRead &&
    1.61 +        (file_name.endsWith(".scala") || file.canExecute) &&
    1.62 +        !file_name.endsWith("~") && !file_name.endsWith(".orig")
    1.63      }
    1.64      catch { case _: SecurityException => false }
    1.65    }
    1.66 @@ -28,9 +62,10 @@
    1.67      val Description = """.*\bDESCRIPTION: *(.*)""".r
    1.68      for {
    1.69        dir <- dirs() if dir.is_dir
    1.70 -      name <- File.read_dir(dir) if is_external(dir, name)
    1.71 +      file_name <- File.read_dir(dir) if is_external(dir, file_name)
    1.72      } yield {
    1.73 -      val source = File.read(dir + Path.basic(name))
    1.74 +      val source = File.read(dir + Path.basic(file_name))
    1.75 +      val name = Library.try_unsuffix(".scala", file_name) getOrElse file_name
    1.76        val description =
    1.77          split_lines(source).collectFirst({ case Description(s) => s }) getOrElse ""
    1.78        (name, description)
    1.79 @@ -38,13 +73,16 @@
    1.80    }
    1.81  
    1.82    private def find_external(name: String): Option[List[String] => Unit] =
    1.83 -    dirs.collectFirst({ case dir if is_external(dir, name) =>
    1.84 -      (args: List[String]) =>
    1.85 -        {
    1.86 -          val tool = dir + Path.basic(name)
    1.87 -          val result = Isabelle_System.bash(File.bash_path(tool) + " " + File.bash_args(args))
    1.88 -          sys.exit(result.print_stdout.rc)
    1.89 -        }
    1.90 +    dirs.collectFirst({
    1.91 +      case dir if is_external(dir, name + ".scala") =>
    1.92 +        compile(dir + Path.basic(name + ".scala"))
    1.93 +      case dir if is_external(dir, name) =>
    1.94 +        (args: List[String]) =>
    1.95 +          {
    1.96 +            val tool = dir + Path.basic(name)
    1.97 +            val result = Isabelle_System.bash(File.bash_path(tool) + " " + File.bash_args(args))
    1.98 +            sys.exit(result.print_stdout.rc)
    1.99 +          }
   1.100      })
   1.101  
   1.102