author | wenzelm |
Sun, 03 Apr 2016 22:15:40 +0200 | |
changeset 62830 | 85024c0e953d |
parent 62829 | 4141c2a8458b |
child 62831 | 5560905a32ae |
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 |
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
3 |
|
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
4 |
Isabelle system tools: external executables or internal Scala functions. |
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
5 |
*/ |
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 |
package isabelle |
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
8 |
|
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
9 |
|
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
10 |
object Isabelle_Tool |
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
11 |
{ |
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
12 |
/* external tools */ |
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
13 |
|
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
14 |
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
|
15 |
|
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
16 |
private def is_external(dir: Path, name: String): Boolean = |
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
17 |
{ |
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
18 |
val file = (dir + Path.basic(name)).file |
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
19 |
try { |
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
20 |
file.isFile && file.canRead && file.canExecute && |
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
21 |
!name.endsWith("~") && !name.endsWith(".orig") |
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
22 |
} |
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
23 |
catch { case _: SecurityException => false } |
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
24 |
} |
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
25 |
|
62830 | 26 |
private def list_external(): List[(String, String)] = |
62829
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
27 |
{ |
62830 | 28 |
val Description = """.*\bDESCRIPTION: *(.*)""".r |
29 |
for { |
|
30 |
dir <- dirs() if dir.is_dir |
|
31 |
name <- File.read_dir(dir) if is_external(dir, name) |
|
32 |
} yield { |
|
33 |
val source = File.read(dir + Path.basic(name)) |
|
34 |
val description = |
|
35 |
split_lines(source).collectFirst({ case Description(s) => s }) getOrElse "" |
|
36 |
(name, description) |
|
37 |
} |
|
62829
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
38 |
} |
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
39 |
|
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
40 |
private def find_external(name: String): Option[List[String] => Unit] = |
62830 | 41 |
dirs.collectFirst({ case dir if is_external(dir, name) => |
42 |
(args: List[String]) => |
|
43 |
{ |
|
44 |
val tool = dir + Path.basic(name) |
|
45 |
val result = Isabelle_System.bash(File.bash_path(tool) + " " + File.bash_args(args)) |
|
46 |
sys.exit(result.print_stdout.rc) |
|
47 |
} |
|
48 |
}) |
|
49 |
||
50 |
||
51 |
/* internal tools */ |
|
52 |
||
53 |
private var internal_tools = Map.empty[String, (String, List[String] => Nothing)] |
|
54 |
||
55 |
private def list_internal(): List[(String, String)] = |
|
56 |
synchronized { |
|
57 |
for ((name, (description, _)) <- internal_tools.toList) yield (name, description) |
|
58 |
} |
|
59 |
||
60 |
private def find_internal(name: String): Option[List[String] => Unit] = |
|
61 |
synchronized { internal_tools.get(name).map(_._2) } |
|
62 |
||
63 |
private def register(isabelle_tool: Isabelle_Tool): Unit = |
|
64 |
synchronized { |
|
65 |
internal_tools += |
|
66 |
(isabelle_tool.name -> |
|
67 |
(isabelle_tool.description, |
|
68 |
args => Command_Line.tool0 { isabelle_tool.body(args) })) |
|
69 |
} |
|
62829
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
70 |
|
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
71 |
|
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
72 |
/* command line entry point */ |
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
73 |
|
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
74 |
def main(args: Array[String]) |
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
75 |
{ |
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
76 |
Command_Line.tool0 { |
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
77 |
args.toList match { |
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
78 |
case Nil | List("-?") => |
62830 | 79 |
val tool_descriptions = |
80 |
(list_external() ::: list_internal()).sortBy(_._1). |
|
81 |
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
|
82 |
Getopts(""" |
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
83 |
Usage: isabelle TOOL [ARGS ...] |
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
84 |
|
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
85 |
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
|
86 |
|
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
87 |
Available tools:""" + tool_descriptions.mkString("\n ", "\n ", "\n")).usage |
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
88 |
case tool_name :: tool_args => |
62830 | 89 |
find_external(tool_name) orElse find_internal(tool_name) match { |
90 |
case Some(tool) => tool(tool_args) |
|
62829
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
91 |
case None => error("Unknown Isabelle tool: " + quote(tool_name)) |
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
92 |
} |
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
93 |
} |
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
94 |
} |
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
95 |
} |
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
96 |
} |
62830 | 97 |
|
98 |
sealed case class Isabelle_Tool(name: String, description: String, body: List[String] => Unit) |