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