src/Pure/System/isabelle_tool.scala
author wenzelm
Wed Oct 12 10:22:34 2016 +0200 (2016-10-12)
changeset 64161 2b1128e95dfb
parent 64143 578e71c2c976
child 64304 96bc94c87a81
permissions -rw-r--r--
explicit indication of Admin 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
    }
lars@63519
    41
    catch {
lars@63519
    42
      case e: ToolBoxError =>
lars@63519
    43
        if (tool_box.frontEnd.hasErrors) {
lars@63519
    44
          val infos = tool_box.frontEnd.infos.toList
lars@63519
    45
          val msgs = infos.map(info => "Error in line " + info.pos.line + ":\n" + info.msg)
lars@63519
    46
          err(msgs.mkString("\n"))
lars@63519
    47
        }
lars@63519
    48
        else
lars@63519
    49
          err(e.toString)
lars@63519
    50
    }
wenzelm@63226
    51
  }
wenzelm@63226
    52
wenzelm@63226
    53
wenzelm@62829
    54
  /* external tools */
wenzelm@62829
    55
wenzelm@62829
    56
  private def dirs(): List[Path] = Path.split(Isabelle_System.getenv_strict("ISABELLE_TOOLS"))
wenzelm@62829
    57
wenzelm@63226
    58
  private def is_external(dir: Path, file_name: String): Boolean =
wenzelm@62829
    59
  {
wenzelm@63226
    60
    val file = (dir + Path.basic(file_name)).file
wenzelm@62829
    61
    try {
wenzelm@63226
    62
      file.isFile && file.canRead &&
wenzelm@63226
    63
        (file_name.endsWith(".scala") || file.canExecute) &&
wenzelm@63226
    64
        !file_name.endsWith("~") && !file_name.endsWith(".orig")
wenzelm@62829
    65
    }
wenzelm@62829
    66
    catch { case _: SecurityException => false }
wenzelm@62829
    67
  }
wenzelm@62829
    68
wenzelm@62830
    69
  private def list_external(): List[(String, String)] =
wenzelm@62829
    70
  {
wenzelm@62830
    71
    val Description = """.*\bDESCRIPTION: *(.*)""".r
wenzelm@62830
    72
    for {
wenzelm@62830
    73
      dir <- dirs() if dir.is_dir
wenzelm@63226
    74
      file_name <- File.read_dir(dir) if is_external(dir, file_name)
wenzelm@62830
    75
    } yield {
wenzelm@63226
    76
      val source = File.read(dir + Path.basic(file_name))
wenzelm@63226
    77
      val name = Library.try_unsuffix(".scala", file_name) getOrElse file_name
wenzelm@62830
    78
      val description =
wenzelm@62830
    79
        split_lines(source).collectFirst({ case Description(s) => s }) getOrElse ""
wenzelm@62830
    80
      (name, description)
wenzelm@62830
    81
    }
wenzelm@62829
    82
  }
wenzelm@62829
    83
wenzelm@62829
    84
  private def find_external(name: String): Option[List[String] => Unit] =
wenzelm@63226
    85
    dirs.collectFirst({
wenzelm@63226
    86
      case dir if is_external(dir, name + ".scala") =>
wenzelm@63226
    87
        compile(dir + Path.basic(name + ".scala"))
wenzelm@63226
    88
      case dir if is_external(dir, name) =>
wenzelm@63226
    89
        (args: List[String]) =>
wenzelm@63226
    90
          {
wenzelm@63226
    91
            val tool = dir + Path.basic(name)
wenzelm@63226
    92
            val result = Isabelle_System.bash(File.bash_path(tool) + " " + File.bash_args(args))
wenzelm@63226
    93
            sys.exit(result.print_stdout.rc)
wenzelm@63226
    94
          }
wenzelm@62830
    95
    })
wenzelm@62830
    96
wenzelm@62830
    97
wenzelm@62830
    98
  /* internal tools */
wenzelm@62830
    99
wenzelm@62960
   100
  private val internal_tools: List[Isabelle_Tool] =
wenzelm@62960
   101
    List(
wenzelm@62960
   102
      Build.isabelle_tool,
wenzelm@62960
   103
      Build_Doc.isabelle_tool,
wenzelm@63688
   104
      Build_Stats.isabelle_tool,
wenzelm@62960
   105
      Check_Sources.isabelle_tool,
wenzelm@62960
   106
      Doc.isabelle_tool,
wenzelm@62960
   107
      ML_Process.isabelle_tool,
wenzelm@62960
   108
      Options.isabelle_tool,
wenzelm@64143
   109
      Remote_DMG.isabelle_tool,
wenzelm@62960
   110
      Update_Cartouches.isabelle_tool,
wenzelm@62960
   111
      Update_Header.isabelle_tool,
wenzelm@62960
   112
      Update_Then.isabelle_tool,
wenzelm@62960
   113
      Update_Theorems.isabelle_tool)
wenzelm@62830
   114
wenzelm@62830
   115
  private def list_internal(): List[(String, String)] =
wenzelm@64161
   116
    for (tool <- internal_tools.toList if tool.accessible)
wenzelm@64161
   117
      yield (tool.name, tool.description)
wenzelm@62830
   118
wenzelm@62830
   119
  private def find_internal(name: String): Option[List[String] => Unit] =
wenzelm@62960
   120
    internal_tools.collectFirst({
wenzelm@64161
   121
      case tool if tool.name == name && tool.accessible =>
wenzelm@62960
   122
        args => Command_Line.tool0 { tool.body(args) }
wenzelm@62960
   123
      })
wenzelm@62831
   124
wenzelm@62829
   125
wenzelm@62829
   126
  /* command line entry point */
wenzelm@62829
   127
wenzelm@62829
   128
  def main(args: Array[String])
wenzelm@62829
   129
  {
wenzelm@62829
   130
    Command_Line.tool0 {
wenzelm@62829
   131
      args.toList match {
wenzelm@62829
   132
        case Nil | List("-?") =>
wenzelm@62830
   133
          val tool_descriptions =
wenzelm@62830
   134
            (list_external() ::: list_internal()).sortBy(_._1).
wenzelm@62830
   135
              map({ case (a, "") => a case (a, b) => a + " - " + b })
wenzelm@62829
   136
          Getopts("""
wenzelm@62829
   137
Usage: isabelle TOOL [ARGS ...]
wenzelm@62829
   138
wenzelm@62829
   139
  Start Isabelle TOOL with ARGS; pass "-?" for tool-specific help.
wenzelm@62829
   140
wenzelm@62829
   141
Available tools:""" + tool_descriptions.mkString("\n  ", "\n  ", "\n")).usage
wenzelm@62829
   142
        case tool_name :: tool_args =>
wenzelm@62830
   143
          find_external(tool_name) orElse find_internal(tool_name) match {
wenzelm@62830
   144
            case Some(tool) => tool(tool_args)
wenzelm@62829
   145
            case None => error("Unknown Isabelle tool: " + quote(tool_name))
wenzelm@62829
   146
          }
wenzelm@62829
   147
      }
wenzelm@62829
   148
    }
wenzelm@62829
   149
  }
wenzelm@62829
   150
}
wenzelm@62830
   151
wenzelm@64161
   152
sealed case class Isabelle_Tool(
wenzelm@64161
   153
  name: String, description: String, body: List[String] => Unit, admin: Boolean = false)
wenzelm@64161
   154
{
wenzelm@64161
   155
  def accessible: Boolean = !admin || Isabelle_System.admin()
wenzelm@64161
   156
}