273 val thy_deps = Toplevel.unknown_theory o Toplevel.keep (fn state => |
273 val thy_deps = Toplevel.unknown_theory o Toplevel.keep (fn state => |
274 let |
274 let |
275 val thy = Toplevel.theory_of state; |
275 val thy = Toplevel.theory_of state; |
276 val thy_session = Present.session_name thy; |
276 val thy_session = Present.session_name thy; |
277 |
277 |
278 val graph = rev (Theory.nodes_of thy) |> map (fn node => |
278 val gr_nodes = rev (Theory.nodes_of thy) |> map (fn node => |
279 let |
279 let |
280 val name = Context.theory_name node; |
280 val name = Context.theory_name node; |
281 val parents = map Context.theory_name (Theory.parents_of node); |
281 val parents = map Context.theory_name (Theory.parents_of node); |
282 val session = Present.session_name node; |
282 val session = Present.session_name node; |
283 val unfold = (session = thy_session); |
283 val unfold = (session = thy_session); |
284 in |
284 in |
285 {name = name, ident = name, parents = parents, directory = session, |
285 ((name, Graph_Display.session_node |
286 unfold = unfold, path = "", content = []} |
286 {name = name, directory = session, unfold = unfold, path = ""}), parents) |
287 end); |
287 end); |
288 in Graph_Display.display_graph graph end); |
288 in Graph_Display.display_graph (map (fst o fst) gr_nodes, Graph.make gr_nodes) end); |
289 |
289 |
290 val locale_deps = Toplevel.unknown_theory o Toplevel.keep (fn state => |
290 val locale_deps = Toplevel.unknown_theory o Toplevel.keep (fn state => |
291 let |
291 let |
292 val thy = Toplevel.theory_of state; |
292 val thy = Toplevel.theory_of state; |
293 val graph = Locale.pretty_locale_deps thy |> map (fn {name, parents, body} => |
293 val gr = Locale.pretty_locale_deps thy |
294 {name = Locale.extern thy name, ident = name, parents = parents, |
294 |> map (fn {name, parents, body} => ((name, |
295 directory = "", unfold = true, path = "", content = [body]}); |
295 Graph_Display.content_node (Locale.extern thy name) [body]), parents)) |
296 in Graph_Display.display_graph graph end); |
296 |> Graph.make; |
|
297 in Graph_Display.display_graph ([], gr) end); |
297 |
298 |
298 |
299 |
299 (* print theorems, terms, types etc. *) |
300 (* print theorems, terms, types etc. *) |
300 |
301 |
301 local |
302 local |