equal
deleted
inserted
replaced
94 /* command line entry point */ |
94 /* command line entry point */ |
95 |
95 |
96 def main(args: Array[String]) |
96 def main(args: Array[String]) |
97 { |
97 { |
98 Command_Line.tool0 { |
98 Command_Line.tool0 { |
|
99 val getopts = Getopts(() => """ |
|
100 Usage: isabelle doc [DOC ...] |
|
101 |
|
102 View Isabelle documentation. |
|
103 """) |
|
104 val docs = getopts(args) |
|
105 |
99 val entries = contents() |
106 val entries = contents() |
100 if (args.isEmpty) Console.println(cat_lines(contents_lines().map(_._2))) |
107 if (docs.isEmpty) Console.println(cat_lines(contents_lines().map(_._2))) |
101 else { |
108 else { |
102 args.foreach(arg => |
109 docs.foreach(doc => |
103 entries.collectFirst { case Doc(name, _, path) if arg == name => path } match { |
110 entries.collectFirst { case Doc(name, _, path) if doc == name => path } match { |
104 case Some(path) => view(path) |
111 case Some(path) => view(path) |
105 case None => error("No Isabelle documentation entry: " + quote(arg)) |
112 case None => error("No Isabelle documentation entry: " + quote(doc)) |
106 } |
113 } |
107 ) |
114 ) |
108 } |
115 } |
109 } |
116 } |
110 } |
117 } |