equal
deleted
inserted
replaced
13 object Doc |
13 object Doc |
14 { |
14 { |
15 /* dirs */ |
15 /* dirs */ |
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")) |
19 if (dir.is_dir) dir |
|
20 else error("Bad documentation directory: " + dir)) |
|
21 |
19 |
22 |
20 |
23 /* contents */ |
21 /* contents */ |
24 |
22 |
25 private def contents_lines(): List[(Path, String)] = |
23 private def contents_lines(): List[(Path, String)] = |