equal
deleted
inserted
replaced
98 path: string, parents: string list}; |
98 path: string, parents: string list}; |
99 |
99 |
100 fun write_graph gr path = |
100 fun write_graph gr path = |
101 File.write path (cat_lines (map (fn {name, ID, dir, unfold, path, parents} => |
101 File.write path (cat_lines (map (fn {name, ID, dir, unfold, path, parents} => |
102 "\"" ^ name ^ "\" \"" ^ ID ^ "\" \"" ^ dir ^ (if unfold then "\" + \"" else "\" \"") ^ |
102 "\"" ^ name ^ "\" \"" ^ ID ^ "\" \"" ^ dir ^ (if unfold then "\" + \"" else "\" \"") ^ |
103 path ^ "\" > " ^ space_implode " " (map quote parents) ^ " ;") gr)); |
103 path ^ "\" > " ^ space_implode " " (map Library.quote parents) ^ " ;") gr)); |
104 |
104 |
105 fun ID_of sess s = space_implode "/" (sess @ [s]); |
105 fun ID_of sess s = space_implode "/" (sess @ [s]); |
106 |
106 |
107 (*retrieve graph data from initial theory loader database*) |
107 (*retrieve graph data from initial theory loader database*) |
108 fun init_graph remote_path curr_sess = map (fn name => |
108 fun init_graph remote_path curr_sess = map (fn name => |