author | wenzelm |
Sun, 03 Apr 2016 23:16:13 +0200 | |
changeset 62838 | c91ca9935280 |
parent 62836 | 98dbed6cfa44 |
child 62960 | cfbb6a5b427c |
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 |
|
62833 | 71 |
register(Build.isabelle_tool) |
62838 | 72 |
register(Build_Doc.isabelle_tool) |
62834 | 73 |
register(Check_Sources.isabelle_tool) |
62831 | 74 |
register(Doc.isabelle_tool) |
62835
1a9ce1b13b20
prefer internal tool -- assuming that ISABELLE_TMP_PREFIX is created properly by Isabelle_System.isabelle_tmp_prefix;
wenzelm
parents:
62834
diff
changeset
|
75 |
register(ML_Process.isabelle_tool) |
62832 | 76 |
register(Options.isabelle_tool) |
62836 | 77 |
register(Update_Cartouches.isabelle_tool) |
78 |
register(Update_Header.isabelle_tool) |
|
79 |
register(Update_Then.isabelle_tool) |
|
80 |
register(Update_Theorems.isabelle_tool) |
|
62831 | 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 |
/* command line entry point */ |
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 |
def main(args: Array[String]) |
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 |
Command_Line.tool0 { |
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
88 |
args.toList match { |
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
89 |
case Nil | List("-?") => |
62830 | 90 |
val tool_descriptions = |
91 |
(list_external() ::: list_internal()).sortBy(_._1). |
|
92 |
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
|
93 |
Getopts(""" |
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
94 |
Usage: isabelle TOOL [ARGS ...] |
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 |
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
|
97 |
|
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
98 |
Available tools:""" + tool_descriptions.mkString("\n ", "\n ", "\n")).usage |
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
99 |
case tool_name :: tool_args => |
62830 | 100 |
find_external(tool_name) orElse find_internal(tool_name) match { |
101 |
case Some(tool) => tool(tool_args) |
|
62829
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
102 |
case None => error("Unknown Isabelle tool: " + quote(tool_name)) |
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
103 |
} |
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
104 |
} |
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
105 |
} |
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
106 |
} |
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
diff
changeset
|
107 |
} |
62830 | 108 |
|
109 |
sealed case class Isabelle_Tool(name: String, description: String, body: List[String] => Unit) |