support for .scala tools;
authorwenzelm
Fri Jun 03 22:27:01 2016 +0200 (2016-06-03)
changeset 63226d8884c111bca
parent 63225 19d2be0e5e9f
child 63227 d3ed7f00e818
support for .scala tools;
NEWS
src/Pure/System/isabelle_tool.scala
     1.1 --- a/NEWS	Thu Jun 02 17:47:47 2016 +0200
     1.2 +++ b/NEWS	Fri Jun 03 22:27:01 2016 +0200
     1.3 @@ -401,6 +401,10 @@
     1.4  executables are found within the shell search $PATH: "isabelle" and
     1.5  "isabelle_scala_script".
     1.6  
     1.7 +* Isabelle tools may consist of .scala files: the Scala compiler is
     1.8 +invoked on the spot. The source needs to define some object that extends
     1.9 +Isabelle_Tool.Body.
    1.10 +
    1.11  * The Isabelle ML process is now managed directly by Isabelle/Scala, and
    1.12  shell scripts merely provide optional command-line access. In
    1.13  particular:
     2.1 --- a/src/Pure/System/isabelle_tool.scala	Thu Jun 02 17:47:47 2016 +0200
     2.2 +++ b/src/Pure/System/isabelle_tool.scala	Fri Jun 03 22:27:01 2016 +0200
     2.3 @@ -1,24 +1,58 @@
     2.4  /*  Title:      Pure/System/isabelle_tool.scala
     2.5      Author:     Makarius
     2.6 +    Author:     Lars Hupel
     2.7  
     2.8  Isabelle system tools: external executables or internal Scala functions.
     2.9  */
    2.10  
    2.11  package isabelle
    2.12  
    2.13 +import java.net.URLClassLoader
    2.14 +import scala.reflect.runtime.universe
    2.15 +import scala.tools.reflect.{ToolBox,ToolBoxError}
    2.16 +
    2.17  
    2.18  object Isabelle_Tool
    2.19  {
    2.20 +  /* Scala source tools */
    2.21 +
    2.22 +  abstract class Body extends Function[List[String], Unit]
    2.23 +
    2.24 +  private def compile(path: Path): Body =
    2.25 +  {
    2.26 +    def err(msg: String): Nothing =
    2.27 +      cat_error(msg, "The error(s) above occurred in Isabelle/Scala tool " + path)
    2.28 +
    2.29 +    val source = File.read(path)
    2.30 +
    2.31 +    val class_loader = new URLClassLoader(Array(), getClass.getClassLoader)
    2.32 +    val tool_box = universe.runtimeMirror(class_loader).mkToolBox()
    2.33 +
    2.34 +    try {
    2.35 +      val symbol = tool_box.parse(source) match {
    2.36 +        case tree: universe.ModuleDef => tool_box.define(tree)
    2.37 +        case _ => err("Source does not describe a module (Scala object)")
    2.38 +      }
    2.39 +      tool_box.compile(universe.Ident(symbol))() match {
    2.40 +        case body: Body => body
    2.41 +        case _ => err("Ill-typed source: Isabelle_Tool.Body expected")
    2.42 +      }
    2.43 +    }
    2.44 +    catch { case e: ToolBoxError => err(e.toString) }
    2.45 +  }
    2.46 +
    2.47 +
    2.48    /* external tools */
    2.49  
    2.50    private def dirs(): List[Path] = Path.split(Isabelle_System.getenv_strict("ISABELLE_TOOLS"))
    2.51  
    2.52 -  private def is_external(dir: Path, name: String): Boolean =
    2.53 +  private def is_external(dir: Path, file_name: String): Boolean =
    2.54    {
    2.55 -    val file = (dir + Path.basic(name)).file
    2.56 +    val file = (dir + Path.basic(file_name)).file
    2.57      try {
    2.58 -      file.isFile && file.canRead && file.canExecute &&
    2.59 -        !name.endsWith("~") && !name.endsWith(".orig")
    2.60 +      file.isFile && file.canRead &&
    2.61 +        (file_name.endsWith(".scala") || file.canExecute) &&
    2.62 +        !file_name.endsWith("~") && !file_name.endsWith(".orig")
    2.63      }
    2.64      catch { case _: SecurityException => false }
    2.65    }
    2.66 @@ -28,9 +62,10 @@
    2.67      val Description = """.*\bDESCRIPTION: *(.*)""".r
    2.68      for {
    2.69        dir <- dirs() if dir.is_dir
    2.70 -      name <- File.read_dir(dir) if is_external(dir, name)
    2.71 +      file_name <- File.read_dir(dir) if is_external(dir, file_name)
    2.72      } yield {
    2.73 -      val source = File.read(dir + Path.basic(name))
    2.74 +      val source = File.read(dir + Path.basic(file_name))
    2.75 +      val name = Library.try_unsuffix(".scala", file_name) getOrElse file_name
    2.76        val description =
    2.77          split_lines(source).collectFirst({ case Description(s) => s }) getOrElse ""
    2.78        (name, description)
    2.79 @@ -38,13 +73,16 @@
    2.80    }
    2.81  
    2.82    private def find_external(name: String): Option[List[String] => Unit] =
    2.83 -    dirs.collectFirst({ case dir if is_external(dir, name) =>
    2.84 -      (args: List[String]) =>
    2.85 -        {
    2.86 -          val tool = dir + Path.basic(name)
    2.87 -          val result = Isabelle_System.bash(File.bash_path(tool) + " " + File.bash_args(args))
    2.88 -          sys.exit(result.print_stdout.rc)
    2.89 -        }
    2.90 +    dirs.collectFirst({
    2.91 +      case dir if is_external(dir, name + ".scala") =>
    2.92 +        compile(dir + Path.basic(name + ".scala"))
    2.93 +      case dir if is_external(dir, name) =>
    2.94 +        (args: List[String]) =>
    2.95 +          {
    2.96 +            val tool = dir + Path.basic(name)
    2.97 +            val result = Isabelle_System.bash(File.bash_path(tool) + " " + File.bash_args(args))
    2.98 +            sys.exit(result.print_stdout.rc)
    2.99 +          }
   2.100      })
   2.101  
   2.102