Present.display_graph;
authorwenzelm
Mon Sep 18 19:12:50 2006 +0200 (2006-09-18)
changeset 20578f26c8408a675
parent 20577 a96883a6d709
child 20579 4dc799edef89
Present.display_graph;
src/Pure/Thy/thm_deps.ML
     1.1 --- a/src/Pure/Thy/thm_deps.ML	Mon Sep 18 19:12:49 2006 +0200
     1.2 +++ b/src/Pure/Thy/thm_deps.ML	Mon Sep 18 19:12:50 2006 +0200
     1.3 @@ -67,14 +67,9 @@
     1.4        end);
     1.5  
     1.6  fun thm_deps thms =
     1.7 -  let
     1.8 -    val _ = writeln "Generating graph ...";
     1.9 -    val gra = map snd (Symtab.dest (fst
    1.10 -      (fold make_deps_graph (map Thm.proof_of thms) (Symtab.empty, []))));
    1.11 -    val path = File.tmp_path (Path.unpack "theorems.graph");
    1.12 -    val _ = Present.write_graph gra path;
    1.13 -    val _ = File.isatool ("browser -d " ^ File.shell_path path ^ " &");
    1.14 -  in () end;
    1.15 +  Present.display_graph
    1.16 +    (map snd (Symtab.dest (fst
    1.17 +      (fold make_deps_graph (map Thm.proof_of thms) (Symtab.empty, [])))));
    1.18  
    1.19  end;
    1.20