1/*  Title:      Pure/System/isabelle_tool.scala
2    Author:     Makarius
3    Author:     Lars Hupel
4
5Isabelle system tools: external executables or internal Scala functions.
6*/
7
8package isabelle
9
10import java.net.URLClassLoader
11import scala.reflect.runtime.universe
12import scala.tools.reflect.{ToolBox,ToolBoxError}
13
14
15object 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.explode(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.explode(file_name))
77      val name = Library.perhaps_unsuffix(".scala", 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.explode(name + ".scala"))
88      case dir if is_external(dir, name) =>
89        (args: List[String]) =>
90          {
91            val tool = dir + Path.explode(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_Cygwin.isabelle_tool,
104      Build_Doc.isabelle_tool,
105      Build_Docker.isabelle_tool,
106      Build_JDK.isabelle_tool,
107      Build_PolyML.isabelle_tool1,
108      Build_PolyML.isabelle_tool2,
109      Build_Status.isabelle_tool,
110      Check_Sources.isabelle_tool,
111      Doc.isabelle_tool,
112      Dump.isabelle_tool,
113      Export.isabelle_tool,
114      Imports.isabelle_tool,
115      Mkroot.isabelle_tool,
116      ML_Process.isabelle_tool,
117      NEWS.isabelle_tool,
118      Options.isabelle_tool,
119      Present.isabelle_tool,
120      Profiling_Report.isabelle_tool,
121      Remote_DMG.isabelle_tool,
122      Server.isabelle_tool,
123      Update_Cartouches.isabelle_tool,
124      Update_Comments.isabelle_tool,
125      Update_Header.isabelle_tool,
126      Update_Then.isabelle_tool,
127      Update_Theorems.isabelle_tool,
128      isabelle.vscode.Build_VSCode.isabelle_tool,
129      isabelle.vscode.Grammar.isabelle_tool,
130      isabelle.vscode.Server.isabelle_tool)
131
132  private def list_internal(): List[(String, String)] =
133    for (tool <- internal_tools.toList if tool.accessible)
134      yield (tool.name, tool.description)
135
136  private def find_internal(name: String): Option[List[String] => Unit] =
137    internal_tools.collectFirst({
138      case tool if tool.name == name && tool.accessible =>
139        args => Command_Line.tool0 { tool.body(args) }
140      })
141
142
143  /* command line entry point */
144
145  def main(args: Array[String])
146  {
147    Command_Line.tool0 {
148      args.toList match {
149        case Nil | List("-?") =>
150          val tool_descriptions =
151            (list_external() ::: list_internal()).sortBy(_._1).
152              map({ case (a, "") => a case (a, b) => a + " - " + b })
153          Getopts("""
154Usage: isabelle TOOL [ARGS ...]
155
156  Start Isabelle TOOL with ARGS; pass "-?" for tool-specific help.
157
158Available tools:""" + tool_descriptions.mkString("\n  ", "\n  ", "\n")).usage
159        case tool_name :: tool_args =>
160          find_external(tool_name) orElse find_internal(tool_name) match {
161            case Some(tool) => tool(tool_args)
162            case None => error("Unknown Isabelle tool: " + quote(tool_name))
163          }
164      }
165    }
166  }
167}
168
169sealed case class Isabelle_Tool(
170  name: String, description: String, body: List[String] => Unit, admin: Boolean = false)
171{
172  def accessible: Boolean = !admin || Isabelle_System.admin()
173}
174