author | wenzelm |
Sun, 03 Apr 2016 21:32:57 +0200 | |
changeset 62829 | 4141c2a8458b |
child 62830 | 85024c0e953d |
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 |
|
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
26 |
private def run_external(dir: Path, name: String)(args: List[String]): Nothing = |
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
27 |
{ |
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
28 |
val tool = dir + Path.basic(name) |
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
29 |
val result = Isabelle_System.bash(File.bash_path(tool) + " " + File.bash_args(args)) |
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
30 |
sys.exit(result.print_stdout.rc) |
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
31 |
} |
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
32 |
|
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
33 |
private def find_external(name: String): Option[List[String] => Unit] = |
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
34 |
dirs.collectFirst({ case dir if is_external(dir, name) => run_external(dir, name) }) |
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
35 |
|
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
36 |
|
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
37 |
/* command line entry point */ |
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 |
private def tool_descriptions(): List[String] = |
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
40 |
{ |
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
41 |
val Description = """.*\bDESCRIPTION: *(.*)""".r |
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
42 |
val entries = |
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
43 |
for { |
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
44 |
dir <- dirs() if dir.is_dir |
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
45 |
name <- File.read_dir(dir) if is_external(dir, name) |
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
46 |
} yield { |
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
47 |
val source = File.read(dir + Path.basic(name)) |
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
48 |
split_lines(source).collectFirst({ case Description(s) => s }) match { |
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
49 |
case None => (name, "") |
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
50 |
case Some(description) => (name, " - " + description) |
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
51 |
} |
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
52 |
} |
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
53 |
entries.sortBy(_._1).map({ case (a, b) => a + b }) |
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
54 |
} |
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 |
def main(args: Array[String]) |
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
57 |
{ |
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
58 |
Command_Line.tool0 { |
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
59 |
args.toList match { |
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
60 |
case Nil | List("-?") => |
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
61 |
Getopts(""" |
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
62 |
Usage: isabelle TOOL [ARGS ...] |
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
63 |
|
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
64 |
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
|
65 |
|
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
66 |
Available tools:""" + tool_descriptions.mkString("\n ", "\n ", "\n")).usage |
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
67 |
case tool_name :: tool_args => |
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
68 |
find_external(tool_name) match { |
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
69 |
case Some(run) => run(tool_args) |
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
70 |
case None => error("Unknown Isabelle tool: " + quote(tool_name)) |
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 |
} |
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 |
} |
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
75 |
} |