equal
deleted
inserted
replaced
80 |
80 |
81 /* view */ |
81 /* view */ |
82 |
82 |
83 def view(path: Path) |
83 def view(path: Path) |
84 { |
84 { |
85 if (path.is_file) Console.println(Library.trim_line(File.read(path))) |
85 if (path.is_file) Output.writeln(Library.trim_line(File.read(path)), stdout = true) |
86 else { |
86 else { |
87 val pdf = path.ext("pdf") |
87 val pdf = path.ext("pdf") |
88 if (pdf.is_file) Isabelle_System.pdf_viewer(pdf) |
88 if (pdf.is_file) Isabelle_System.pdf_viewer(pdf) |
89 else error("Bad Isabelle documentation file: " + pdf) |
89 else error("Bad Isabelle documentation file: " + pdf) |
90 } |
90 } |
101 View Isabelle documentation. |
101 View Isabelle documentation. |
102 """) |
102 """) |
103 val docs = getopts(args) |
103 val docs = getopts(args) |
104 |
104 |
105 val entries = contents() |
105 val entries = contents() |
106 if (docs.isEmpty) Console.println(cat_lines(contents_lines().map(_._2))) |
106 if (docs.isEmpty) Output.writeln(cat_lines(contents_lines().map(_._2)), stdout = true) |
107 else { |
107 else { |
108 docs.foreach(doc => |
108 docs.foreach(doc => |
109 entries.collectFirst { case Doc(name, _, path) if doc == name => path } match { |
109 entries.collectFirst { case Doc(name, _, path) if doc == name => path } match { |
110 case Some(path) => view(path) |
110 case Some(path) => view(path) |
111 case None => error("No Isabelle documentation entry: " + quote(doc)) |
111 case None => error("No Isabelle documentation entry: " + quote(doc)) |