equal
deleted
inserted
replaced
52 private def examples(): List[Entry] = |
52 private def examples(): List[Entry] = |
53 Section("Examples", true) :: |
53 Section("Examples", true) :: |
54 Path.split(Isabelle_System.getenv_strict("ISABELLE_DOCS_EXAMPLES")).map(file => |
54 Path.split(Isabelle_System.getenv_strict("ISABELLE_DOCS_EXAMPLES")).map(file => |
55 text_file(file) match { |
55 text_file(file) match { |
56 case Some(entry) => entry |
56 case Some(entry) => entry |
57 case None => error("Bad ISABELLE_DOCS_EXAMPLES entry: " + file) |
57 case None => error("Bad entry in ISABELLE_DOCS_EXAMPLES: " + file) |
58 }) |
58 }) |
59 |
59 |
60 def contents(): List[Entry] = |
60 def contents(): List[Entry] = |
61 (for { |
61 (for { |
62 (dir, line) <- contents_lines() |
62 (dir, line) <- contents_lines() |
89 /* command line entry point */ |
89 /* command line entry point */ |
90 |
90 |
91 def main(args: Array[String]) |
91 def main(args: Array[String]) |
92 { |
92 { |
93 Command_Line.tool { |
93 Command_Line.tool { |
|
94 val entries = contents() |
94 if (args.isEmpty) Console.println(cat_lines(contents_lines().map(_._2))) |
95 if (args.isEmpty) Console.println(cat_lines(contents_lines().map(_._2))) |
95 else { |
96 else { |
96 val entries = contents() |
|
97 args.foreach(arg => |
97 args.foreach(arg => |
98 entries.collectFirst { case Doc(name, _, path) if arg == name => path } match { |
98 entries.collectFirst { case Doc(name, _, path) if arg == name => path } match { |
99 case Some(path) => view(path) |
99 case Some(path) => view(path) |
100 case None => error("No Isabelle documentation entry: " + quote(arg)) |
100 case None => error("No Isabelle documentation entry: " + quote(arg)) |
101 } |
101 } |