equal
deleted
inserted
replaced
34 File.write(dir + sessions_path, YXML.string_of_body(list(pair(string, string))(sessions))) |
34 File.write(dir + sessions_path, YXML.string_of_body(list(pair(string, string))(sessions))) |
35 } |
35 } |
36 |
36 |
37 def update_chapter_index(browser_info: Path, chapter: String, new_sessions: List[(String, String)]) |
37 def update_chapter_index(browser_info: Path, chapter: String, new_sessions: List[(String, String)]) |
38 { |
38 { |
39 val dir = browser_info + Path.basic(chapter) |
39 val dir = Isabelle_System.make_directory(browser_info + Path.basic(chapter)) |
40 Isabelle_System.make_directory(dir) |
|
41 |
40 |
42 val sessions0 = |
41 val sessions0 = |
43 try { read_sessions(dir) } |
42 try { read_sessions(dir) } |
44 catch { case _: XML.Error => Nil } |
43 catch { case _: XML.Error => Nil } |
45 |
44 |