equal
deleted
inserted
replaced
16 |
16 |
17 def dirs(): List[Path] = |
17 def dirs(): List[Path] = |
18 Path.split(Isabelle_System.getenv("ISABELLE_DOCS")).map(dir => |
18 Path.split(Isabelle_System.getenv("ISABELLE_DOCS")).map(dir => |
19 if (dir.is_dir) dir |
19 if (dir.is_dir) dir |
20 else error("Bad documentation directory: " + dir)) |
20 else error("Bad documentation directory: " + dir)) |
21 |
21 |
22 |
22 |
23 /* contents */ |
23 /* contents */ |
24 |
24 |
25 private def contents_lines(): List[String] = |
25 private def contents_lines(): List[String] = |
26 for { |
26 for { |
67 |
67 |
68 /* view */ |
68 /* view */ |
69 |
69 |
70 def view(name: String) |
70 def view(name: String) |
71 { |
71 { |
72 val doc = name + "." + Isabelle_System.getenv_strict("ISABELLE_DOC_FORMAT") |
72 val doc = name + ".pdf" |
73 dirs().find(dir => (dir + Path.basic(doc)).is_file) match { |
73 dirs().find(dir => (dir + Path.basic(doc)).is_file) match { |
74 case Some(dir) => |
74 case Some(dir) => |
75 Isabelle_System.bash_env(dir.file, null, |
75 Isabelle_System.bash_env(dir.file, null, |
76 "\"$ISABELLE_TOOL\" display " + quote(doc) + " >/dev/null 2>/dev/null &") |
76 "\"$ISABELLE_TOOL\" display " + quote(doc) + " >/dev/null 2>/dev/null &") |
77 case None => error("Missing Isabelle documentation file: " + quote(doc)) |
77 case None => error("Missing Isabelle documentation file: " + quote(doc)) |