equal
deleted
inserted
replaced
259 |> File.write (Path.append dir index_path); |
259 |> File.write (Path.append dir index_path); |
260 |
260 |
261 fun update_index dir name = |
261 fun update_index dir name = |
262 (case try get_entries dir of |
262 (case try get_entries dir of |
263 NONE => warning ("Browser info: cannot access session index of " ^ quote (Path.pack dir)) |
263 NONE => warning ("Browser info: cannot access session index of " ^ quote (Path.pack dir)) |
264 | SOME es => (put_entries ((es \ name) @ [name]) dir; create_index dir)); |
264 | SOME es => (put_entries ((remove (op =) name es) @ [name]) dir; create_index dir)); |
265 |
265 |
266 |
266 |
267 (* document versions *) |
267 (* document versions *) |
268 |
268 |
269 fun read_version str = |
269 fun read_version str = |