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