author | wenzelm |
Thu, 18 May 2017 14:14:20 +0200 | |
changeset 65865 | 177b90f33f40 |
parent 65743 | 4847ca570454 |
child 65880 | 54c6ec4166a4 |
permissions | -rw-r--r-- |
62829
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
1 |
/* Title: Pure/System/isabelle_tool.scala |
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
2 |
Author: Makarius |
63226 | 3 |
Author: Lars Hupel |
62829
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
4 |
|
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
5 |
Isabelle system tools: external executables or internal Scala functions. |
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
6 |
*/ |
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
7 |
|
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
8 |
package isabelle |
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
9 |
|
63226 | 10 |
import java.net.URLClassLoader |
11 |
import scala.reflect.runtime.universe |
|
12 |
import scala.tools.reflect.{ToolBox,ToolBoxError} |
|
13 |
||
62829
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
14 |
|
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
15 |
object Isabelle_Tool |
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
16 |
{ |
63226 | 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 |
} |
|
63519
78401d628718
more precise error information for dynamic Scala tools
Lars Hupel <lars.hupel@mytum.de>
parents:
63226
diff
changeset
|
41 |
catch { |
78401d628718
more precise error information for dynamic Scala tools
Lars Hupel <lars.hupel@mytum.de>
parents:
63226
diff
changeset
|
42 |
case e: ToolBoxError => |
78401d628718
more precise error information for dynamic Scala tools
Lars Hupel <lars.hupel@mytum.de>
parents:
63226
diff
changeset
|
43 |
if (tool_box.frontEnd.hasErrors) { |
78401d628718
more precise error information for dynamic Scala tools
Lars Hupel <lars.hupel@mytum.de>
parents:
63226
diff
changeset
|
44 |
val infos = tool_box.frontEnd.infos.toList |
78401d628718
more precise error information for dynamic Scala tools
Lars Hupel <lars.hupel@mytum.de>
parents:
63226
diff
changeset
|
45 |
val msgs = infos.map(info => "Error in line " + info.pos.line + ":\n" + info.msg) |
78401d628718
more precise error information for dynamic Scala tools
Lars Hupel <lars.hupel@mytum.de>
parents:
63226
diff
changeset
|
46 |
err(msgs.mkString("\n")) |
78401d628718
more precise error information for dynamic Scala tools
Lars Hupel <lars.hupel@mytum.de>
parents:
63226
diff
changeset
|
47 |
} |
78401d628718
more precise error information for dynamic Scala tools
Lars Hupel <lars.hupel@mytum.de>
parents:
63226
diff
changeset
|
48 |
else |
78401d628718
more precise error information for dynamic Scala tools
Lars Hupel <lars.hupel@mytum.de>
parents:
63226
diff
changeset
|
49 |
err(e.toString) |
78401d628718
more precise error information for dynamic Scala tools
Lars Hupel <lars.hupel@mytum.de>
parents:
63226
diff
changeset
|
50 |
} |
63226 | 51 |
} |
52 |
||
53 |
||
62829
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
54 |
/* external tools */ |
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
55 |
|
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
56 |
private def dirs(): List[Path] = Path.split(Isabelle_System.getenv_strict("ISABELLE_TOOLS")) |
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
57 |
|
63226 | 58 |
private def is_external(dir: Path, file_name: String): Boolean = |
62829
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
59 |
{ |
65450
b0a73039ddaa
more robust: user could provide name with "/" etc.;
wenzelm
parents:
65138
diff
changeset
|
60 |
val file = (dir + Path.explode(file_name)).file |
62829
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
61 |
try { |
63226 | 62 |
file.isFile && file.canRead && |
63 |
(file_name.endsWith(".scala") || file.canExecute) && |
|
64 |
!file_name.endsWith("~") && !file_name.endsWith(".orig") |
|
62829
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
65 |
} |
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
66 |
catch { case _: SecurityException => false } |
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
67 |
} |
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
68 |
|
62830 | 69 |
private def list_external(): List[(String, String)] = |
62829
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
70 |
{ |
62830 | 71 |
val Description = """.*\bDESCRIPTION: *(.*)""".r |
72 |
for { |
|
73 |
dir <- dirs() if dir.is_dir |
|
63226 | 74 |
file_name <- File.read_dir(dir) if is_external(dir, file_name) |
62830 | 75 |
} yield { |
65450
b0a73039ddaa
more robust: user could provide name with "/" etc.;
wenzelm
parents:
65138
diff
changeset
|
76 |
val source = File.read(dir + Path.explode(file_name)) |
65606 | 77 |
val name = Library.perhaps_unsuffix(".scala", file_name) |
62830 | 78 |
val description = |
79 |
split_lines(source).collectFirst({ case Description(s) => s }) getOrElse "" |
|
80 |
(name, description) |
|
81 |
} |
|
62829
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
82 |
} |
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
83 |
|
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
84 |
private def find_external(name: String): Option[List[String] => Unit] = |
63226 | 85 |
dirs.collectFirst({ |
86 |
case dir if is_external(dir, name + ".scala") => |
|
65450
b0a73039ddaa
more robust: user could provide name with "/" etc.;
wenzelm
parents:
65138
diff
changeset
|
87 |
compile(dir + Path.explode(name + ".scala")) |
63226 | 88 |
case dir if is_external(dir, name) => |
89 |
(args: List[String]) => |
|
90 |
{ |
|
65450
b0a73039ddaa
more robust: user could provide name with "/" etc.;
wenzelm
parents:
65138
diff
changeset
|
91 |
val tool = dir + Path.explode(name) |
64304 | 92 |
val result = Isabelle_System.bash(File.bash_path(tool) + " " + Bash.strings(args)) |
63226 | 93 |
sys.exit(result.print_stdout.rc) |
94 |
} |
|
62830 | 95 |
}) |
96 |
||
97 |
||
98 |
/* internal tools */ |
|
99 |
||
62960
cfbb6a5b427c
simplified -- avoid odd mutable state, which potentially causes problems with module initialization;
wenzelm
parents:
62838
diff
changeset
|
100 |
private val internal_tools: List[Isabelle_Tool] = |
cfbb6a5b427c
simplified -- avoid odd mutable state, which potentially causes problems with module initialization;
wenzelm
parents:
62838
diff
changeset
|
101 |
List( |
cfbb6a5b427c
simplified -- avoid odd mutable state, which potentially causes problems with module initialization;
wenzelm
parents:
62838
diff
changeset
|
102 |
Build.isabelle_tool, |
65071 | 103 |
Build_Cygwin.isabelle_tool, |
62960
cfbb6a5b427c
simplified -- avoid odd mutable state, which potentially causes problems with module initialization;
wenzelm
parents:
62838
diff
changeset
|
104 |
Build_Doc.isabelle_tool, |
64890
d8ccbd5305bf
build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
64872
diff
changeset
|
105 |
Build_Docker.isabelle_tool, |
64929 | 106 |
Build_JDK.isabelle_tool, |
64500
159ea1055b39
back to regular Isabelle tool (reverting abc34a149690);
wenzelm
parents:
64490
diff
changeset
|
107 |
Build_PolyML.isabelle_tool, |
65743 | 108 |
Build_Status.isabelle_tool, |
62960
cfbb6a5b427c
simplified -- avoid odd mutable state, which potentially causes problems with module initialization;
wenzelm
parents:
62838
diff
changeset
|
109 |
Check_Sources.isabelle_tool, |
cfbb6a5b427c
simplified -- avoid odd mutable state, which potentially causes problems with module initialization;
wenzelm
parents:
62838
diff
changeset
|
110 |
Doc.isabelle_tool, |
65557 | 111 |
Imports.isabelle_tool, |
62960
cfbb6a5b427c
simplified -- avoid odd mutable state, which potentially causes problems with module initialization;
wenzelm
parents:
62838
diff
changeset
|
112 |
ML_Process.isabelle_tool, |
64369 | 113 |
NEWS.isabelle_tool, |
62960
cfbb6a5b427c
simplified -- avoid odd mutable state, which potentially causes problems with module initialization;
wenzelm
parents:
62838
diff
changeset
|
114 |
Options.isabelle_tool, |
64311 | 115 |
Profiling_Report.isabelle_tool, |
64143 | 116 |
Remote_DMG.isabelle_tool, |
62960
cfbb6a5b427c
simplified -- avoid odd mutable state, which potentially causes problems with module initialization;
wenzelm
parents:
62838
diff
changeset
|
117 |
Update_Cartouches.isabelle_tool, |
cfbb6a5b427c
simplified -- avoid odd mutable state, which potentially causes problems with module initialization;
wenzelm
parents:
62838
diff
changeset
|
118 |
Update_Header.isabelle_tool, |
cfbb6a5b427c
simplified -- avoid odd mutable state, which potentially causes problems with module initialization;
wenzelm
parents:
62838
diff
changeset
|
119 |
Update_Then.isabelle_tool, |
64605
9c1173a7e4cb
basic support for VSCode Language Server protocol;
wenzelm
parents:
64500
diff
changeset
|
120 |
Update_Theorems.isabelle_tool, |
65138 | 121 |
isabelle.vscode.Build_VSCode.isabelle_tool, |
64738
bcdecd466cb2
generate static TextMate grammar for VSCode editor;
wenzelm
parents:
64605
diff
changeset
|
122 |
isabelle.vscode.Grammar.isabelle_tool, |
65138 | 123 |
isabelle.vscode.Server.isabelle_tool) |
62830 | 124 |
|
125 |
private def list_internal(): List[(String, String)] = |
|
64161 | 126 |
for (tool <- internal_tools.toList if tool.accessible) |
127 |
yield (tool.name, tool.description) |
|
62830 | 128 |
|
129 |
private def find_internal(name: String): Option[List[String] => Unit] = |
|
62960
cfbb6a5b427c
simplified -- avoid odd mutable state, which potentially causes problems with module initialization;
wenzelm
parents:
62838
diff
changeset
|
130 |
internal_tools.collectFirst({ |
64161 | 131 |
case tool if tool.name == name && tool.accessible => |
62960
cfbb6a5b427c
simplified -- avoid odd mutable state, which potentially causes problems with module initialization;
wenzelm
parents:
62838
diff
changeset
|
132 |
args => Command_Line.tool0 { tool.body(args) } |
cfbb6a5b427c
simplified -- avoid odd mutable state, which potentially causes problems with module initialization;
wenzelm
parents:
62838
diff
changeset
|
133 |
}) |
62831 | 134 |
|
62829
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
135 |
|
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
136 |
/* command line entry point */ |
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
137 |
|
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
138 |
def main(args: Array[String]) |
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
139 |
{ |
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
140 |
Command_Line.tool0 { |
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
141 |
args.toList match { |
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
142 |
case Nil | List("-?") => |
62830 | 143 |
val tool_descriptions = |
144 |
(list_external() ::: list_internal()).sortBy(_._1). |
|
145 |
map({ case (a, "") => a case (a, b) => a + " - " + b }) |
|
62829
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
146 |
Getopts(""" |
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
147 |
Usage: isabelle TOOL [ARGS ...] |
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
148 |
|
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
149 |
Start Isabelle TOOL with ARGS; pass "-?" for tool-specific help. |
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
150 |
|
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
151 |
Available tools:""" + tool_descriptions.mkString("\n ", "\n ", "\n")).usage |
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
152 |
case tool_name :: tool_args => |
62830 | 153 |
find_external(tool_name) orElse find_internal(tool_name) match { |
154 |
case Some(tool) => tool(tool_args) |
|
62829
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
155 |
case None => error("Unknown Isabelle tool: " + quote(tool_name)) |
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
156 |
} |
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
157 |
} |
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
158 |
} |
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
159 |
} |
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
160 |
} |
62830 | 161 |
|
64161 | 162 |
sealed case class Isabelle_Tool( |
163 |
name: String, description: String, body: List[String] => Unit, admin: Boolean = false) |
|
164 |
{ |
|
165 |
def accessible: Boolean = !admin || Isabelle_System.admin() |
|
166 |
} |