401 let |
401 let |
402 val name = Context.theory_name node; |
402 val name = Context.theory_name node; |
403 val parents = map Context.theory_name (Theory.parents_of node); |
403 val parents = map Context.theory_name (Theory.parents_of node); |
404 val session = Present.session_name node; |
404 val session = Present.session_name node; |
405 val unfold = (session = thy_session); |
405 val unfold = (session = thy_session); |
406 in {name = name, ID = name, parents = parents, dir = session, unfold = unfold, path = ""} end); |
406 in |
407 in Present.display_graph gr end); |
407 {name = name, ID = name, parents = parents, dir = session, |
|
408 unfold = unfold, path = "", content = []} |
|
409 end); |
|
410 in Graph_Display.display_graph gr end); |
408 |
411 |
409 val class_deps = Toplevel.unknown_theory o Toplevel.keep (fn state => |
412 val class_deps = Toplevel.unknown_theory o Toplevel.keep (fn state => |
410 let |
413 let |
411 val ctxt = Toplevel.context_of state; |
414 val ctxt = Toplevel.context_of state; |
412 val {classes = (space, algebra), ...} = Type.rep_tsig (Proof_Context.tsig_of ctxt); |
415 val {classes = (space, algebra), ...} = Type.rep_tsig (Proof_Context.tsig_of ctxt); |
413 val classes = Sorts.classes_of algebra; |
416 val classes = Sorts.classes_of algebra; |
414 fun entry (c, (i, (_, cs))) = |
417 fun entry (c, (i, (_, cs))) = |
415 (i, {name = Name_Space.extern ctxt space c, ID = c, parents = Graph.Keys.dest cs, |
418 (i, {name = Name_Space.extern ctxt space c, ID = c, parents = Graph.Keys.dest cs, |
416 dir = "", unfold = true, path = ""}); |
419 dir = "", unfold = true, path = "", content = []}); |
417 val gr = |
420 val gr = |
418 Graph.fold (cons o entry) classes [] |
421 Graph.fold (cons o entry) classes [] |
419 |> sort (int_ord o pairself #1) |> map #2; |
422 |> sort (int_ord o pairself #1) |> map #2; |
420 in Present.display_graph gr end); |
423 in Graph_Display.display_graph gr end); |
421 |
424 |
422 fun thm_deps args = Toplevel.unknown_theory o Toplevel.keep (fn state => |
425 fun thm_deps args = Toplevel.unknown_theory o Toplevel.keep (fn state => |
423 Thm_Deps.thm_deps (Toplevel.theory_of state) |
426 Thm_Deps.thm_deps (Toplevel.theory_of state) |
424 (Attrib.eval_thms (Toplevel.context_of state) args)); |
427 (Attrib.eval_thms (Toplevel.context_of state) args)); |
425 |
428 |