21 !name.endsWith("~") && !name.endsWith(".orig") |
21 !name.endsWith("~") && !name.endsWith(".orig") |
22 } |
22 } |
23 catch { case _: SecurityException => false } |
23 catch { case _: SecurityException => false } |
24 } |
24 } |
25 |
25 |
26 private def run_external(dir: Path, name: String)(args: List[String]): Nothing = |
26 private def list_external(): List[(String, String)] = |
27 { |
27 { |
28 val tool = dir + Path.basic(name) |
28 val Description = """.*\bDESCRIPTION: *(.*)""".r |
29 val result = Isabelle_System.bash(File.bash_path(tool) + " " + File.bash_args(args)) |
29 for { |
30 sys.exit(result.print_stdout.rc) |
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 } |
31 } |
38 } |
32 |
39 |
33 private def find_external(name: String): Option[List[String] => Unit] = |
40 private def find_external(name: String): Option[List[String] => Unit] = |
34 dirs.collectFirst({ case dir if is_external(dir, name) => run_external(dir, name) }) |
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 } |
35 |
70 |
36 |
71 |
37 /* command line entry point */ |
72 /* command line entry point */ |
38 |
|
39 private def tool_descriptions(): List[String] = |
|
40 { |
|
41 val Description = """.*\bDESCRIPTION: *(.*)""".r |
|
42 val entries = |
|
43 for { |
|
44 dir <- dirs() if dir.is_dir |
|
45 name <- File.read_dir(dir) if is_external(dir, name) |
|
46 } yield { |
|
47 val source = File.read(dir + Path.basic(name)) |
|
48 split_lines(source).collectFirst({ case Description(s) => s }) match { |
|
49 case None => (name, "") |
|
50 case Some(description) => (name, " - " + description) |
|
51 } |
|
52 } |
|
53 entries.sortBy(_._1).map({ case (a, b) => a + b }) |
|
54 } |
|
55 |
73 |
56 def main(args: Array[String]) |
74 def main(args: Array[String]) |
57 { |
75 { |
58 Command_Line.tool0 { |
76 Command_Line.tool0 { |
59 args.toList match { |
77 args.toList match { |
60 case Nil | List("-?") => |
78 case Nil | List("-?") => |
|
79 val tool_descriptions = |
|
80 (list_external() ::: list_internal()).sortBy(_._1). |
|
81 map({ case (a, "") => a case (a, b) => a + " - " + b }) |
61 Getopts(""" |
82 Getopts(""" |
62 Usage: isabelle TOOL [ARGS ...] |
83 Usage: isabelle TOOL [ARGS ...] |
63 |
84 |
64 Start Isabelle TOOL with ARGS; pass "-?" for tool-specific help. |
85 Start Isabelle TOOL with ARGS; pass "-?" for tool-specific help. |
65 |
86 |
66 Available tools:""" + tool_descriptions.mkString("\n ", "\n ", "\n")).usage |
87 Available tools:""" + tool_descriptions.mkString("\n ", "\n ", "\n")).usage |
67 case tool_name :: tool_args => |
88 case tool_name :: tool_args => |
68 find_external(tool_name) match { |
89 find_external(tool_name) orElse find_internal(tool_name) match { |
69 case Some(run) => run(tool_args) |
90 case Some(tool) => tool(tool_args) |
70 case None => error("Unknown Isabelle tool: " + quote(tool_name)) |
91 case None => error("Unknown Isabelle tool: " + quote(tool_name)) |
71 } |
92 } |
72 } |
93 } |
73 } |
94 } |
74 } |
95 } |
75 } |
96 } |
|
97 |
|
98 sealed case class Isabelle_Tool(name: String, description: String, body: List[String] => Unit) |