# HG changeset patch # User wenzelm # Date 1429125627 -7200 # Node ID 2a066431a814b64cf32bbd6d5b05089b2cb0477b # Parent 6d6d652ee029b387488f063e45892ce81ab235b3 ensure that deps are defined in entries, to prevent crash of Graph_View.build_graph; diff -r 6d6d652ee029 -r 2a066431a814 src/Pure/Tools/thm_deps.ML --- a/src/Pure/Tools/thm_deps.ML Wed Apr 15 20:00:18 2015 +0200 +++ b/src/Pure/Tools/thm_deps.ML Wed Apr 15 21:20:27 2015 +0200 @@ -17,6 +17,9 @@ fun thm_deps thy thms = let + fun make_node name directory = + Graph_Display.session_node + {name = Long_Name.base_name name, directory = directory, unfold = false, path = ""}; fun add_dep ("", _, _) = I | add_dep (name, _, PBody {thms = thms', ...}) = let @@ -30,16 +33,17 @@ "" => [] | session => [session]) | NONE => []) - | _ => ["global"]); - val directory = space_implode "/" (session @ prefix); - val parents = filter_out (fn s => s = "") (map (#1 o #2) thms'); - in - cons ((name, Graph_Display.session_node - {name = Long_Name.base_name name, directory = directory, - unfold = false, path = ""}), parents) - end; + | _ => ["global"]); + val node = make_node name (space_implode "/" (session @ prefix)); + val deps = filter_out (fn s => s = "") (map (#1 o #2) thms'); + in Symtab.update (name, (node, deps)) end; + val entries0 = Proofterm.fold_body_thms add_dep (Thm.proof_bodies_of thms) Symtab.empty; + val entries1 = + Symtab.fold (fn (_, (_, deps)) => deps |> fold (fn d => fn tab => + if Symtab.defined tab d then tab + else Symtab.update (d, (make_node d "", [])) tab)) entries0 entries0; in - Proofterm.fold_body_thms add_dep (Thm.proof_bodies_of thms) [] + Symtab.fold (fn (name, (node, deps)) => cons ((name, node), deps)) entries1 [] |> Graph_Display.display_graph end; @@ -120,4 +124,3 @@ end))); end; -