32 fun make_deps_graph (p, AbsP (_, _, prf)) = make_deps_graph (p, prf) |
32 fun make_deps_graph (p, AbsP (_, _, prf)) = make_deps_graph (p, prf) |
33 | make_deps_graph (p, Abst (_, _, prf)) = make_deps_graph (p, prf) |
33 | make_deps_graph (p, Abst (_, _, prf)) = make_deps_graph (p, prf) |
34 | make_deps_graph (p, prf1 %% prf2) = |
34 | make_deps_graph (p, prf1 %% prf2) = |
35 make_deps_graph (make_deps_graph (p, prf1), prf2) |
35 make_deps_graph (make_deps_graph (p, prf1), prf2) |
36 | make_deps_graph (p, prf % _) = make_deps_graph (p, prf) |
36 | make_deps_graph (p, prf % _) = make_deps_graph (p, prf) |
37 | make_deps_graph (p, MinProof prfs) = foldl make_deps_graph (p, prfs) |
37 | make_deps_graph (p, MinProof prfs) = Library.foldl make_deps_graph (p, prfs) |
38 | make_deps_graph (p as (gra, parents), prf) = |
38 | make_deps_graph (p as (gra, parents), prf) = |
39 let val ((name, tags), prf') = dest_thm_axm prf |
39 let val ((name, tags), prf') = dest_thm_axm prf |
40 in |
40 in |
41 if name <> "" andalso not (Drule.has_internal tags) then |
41 if name <> "" andalso not (Drule.has_internal tags) then |
42 if is_none (Symtab.lookup (gra, name)) then |
42 if is_none (Symtab.lookup (gra, name)) then |
66 end; |
66 end; |
67 |
67 |
68 fun thm_deps thms = |
68 fun thm_deps thms = |
69 let |
69 let |
70 val _ = writeln "Generating graph ..."; |
70 val _ = writeln "Generating graph ..."; |
71 val gra = map snd (Symtab.dest (fst (foldl make_deps_graph ((Symtab.empty, []), |
71 val gra = map snd (Symtab.dest (fst (Library.foldl make_deps_graph ((Symtab.empty, []), |
72 map Thm.proof_of thms)))); |
72 map Thm.proof_of thms)))); |
73 val path = File.tmp_path (Path.unpack "theorems.graph"); |
73 val path = File.tmp_path (Path.unpack "theorems.graph"); |
74 val _ = Present.write_graph gra path; |
74 val _ = Present.write_graph gra path; |
75 val _ = system ("$ISATOOL browser -d " ^ Path.pack (Path.expand path) ^ " &"); |
75 val _ = system ("$ISATOOL browser -d " ^ Path.pack (Path.expand path) ^ " &"); |
76 in () end; |
76 in () end; |