430 (true, |
430 (true, |
431 case try File.read_lines path of |
431 case try File.read_lines path of |
432 SOME (comp_thys :: incomp_thys :: fact_lines) => |
432 SOME (comp_thys :: incomp_thys :: fact_lines) => |
433 let |
433 let |
434 fun add_thy comp thy = Symtab.update (thy, comp) |
434 fun add_thy comp thy = Symtab.update (thy, comp) |
|
435 fun add_edge_to name parent = |
|
436 Graph.default_node (parent, ()) |
|
437 #> Graph.add_edge (parent, name) |
435 fun add_fact_line line = |
438 fun add_fact_line line = |
436 case extract_query line of |
439 case extract_query line of |
437 ("", _) => I (* shouldn't happen *) |
440 ("", _) => I (* shouldn't happen *) |
438 | (name, parents) => |
441 | (name, parents) => |
439 Graph.default_node (name, ()) |
442 Graph.default_node (name, ()) |
440 #> fold (fn par => Graph.add_edge (par, name)) parents |
443 #> fold (add_edge_to name) parents |
441 val thys = |
444 val thys = |
442 Symtab.empty |> fold (add_thy true) (unescape_metas comp_thys) |
445 Symtab.empty |> fold (add_thy true) (unescape_metas comp_thys) |
443 |> fold (add_thy false) (unescape_metas incomp_thys) |
446 |> fold (add_thy false) (unescape_metas incomp_thys) |
444 val fact_graph = |
447 val fact_graph = |
445 try_graph ctxt "loading state file" Graph.empty (fn () => |
448 try_graph ctxt "loading state" Graph.empty (fn () => |
446 Graph.empty |> fold add_fact_line fact_lines) |
449 Graph.empty |> fold add_fact_line fact_lines) |
447 in {thys = thys, fact_graph = fact_graph} end |
450 in {thys = thys, fact_graph = fact_graph} end |
448 | _ => empty_state) |
451 | _ => empty_state) |
449 end |
452 end |
450 |
453 |