14 |
14 |
15 object Present |
15 object Present |
16 { |
16 { |
17 /* maintain chapter index -- NOT thread-safe */ |
17 /* maintain chapter index -- NOT thread-safe */ |
18 |
18 |
19 private val index_path = Path.basic("index.html") |
|
20 private val sessions_path = Path.basic(".sessions") |
19 private val sessions_path = Path.basic(".sessions") |
21 |
20 |
22 private def read_sessions(dir: Path): List[(String, String)] = |
21 private def read_sessions(dir: Path): List[(String, String)] = |
23 { |
22 { |
24 val path = dir + sessions_path |
23 val path = dir + sessions_path |
43 val sessions0 = |
42 val sessions0 = |
44 try { read_sessions(dir) } |
43 try { read_sessions(dir) } |
45 catch { case _: XML.Error => Nil } |
44 catch { case _: XML.Error => Nil } |
46 |
45 |
47 val sessions = (SortedMap.empty[String, String] ++ sessions0 ++ new_sessions).toList |
46 val sessions = (SortedMap.empty[String, String] ++ sessions0 ++ new_sessions).toList |
|
47 write_sessions(dir, sessions) |
48 |
48 |
49 write_sessions(dir, sessions) |
49 val title = "Isabelle/" + chapter + " sessions" |
50 File.write(dir + index_path, HTML.chapter_index(chapter, sessions)) |
50 HTML.write_document(dir, "index.html", |
|
51 List(HTML.title(title + " (" + Distribution.version + ")")), |
|
52 HTML.chapter(title) :: |
|
53 (if (sessions.isEmpty) Nil |
|
54 else |
|
55 List(HTML.css_class("sessions")(HTML.div(List( |
|
56 HTML.itemize( |
|
57 sessions.map({ case (name, description) => |
|
58 HTML.link(name + "/index.html", HTML.text(name)) :: |
|
59 (if (description == "") Nil |
|
60 else List(HTML.pre(HTML.text(description)))) })))))))) |
51 } |
61 } |
52 |
62 |
53 def make_global_index(browser_info: Path) |
63 def make_global_index(browser_info: Path) |
54 { |
64 { |
55 if (!(browser_info + Path.explode("index.html")).is_file) { |
65 if (!(browser_info + Path.explode("index.html")).is_file) { |