src/Pure/Thy/thm_deps.ML
changeset 9450 c97dba47e504
parent 7853 a4acf1b4d5a8
child 9502 50ec59aff389
     1.1 --- a/src/Pure/Thy/thm_deps.ML	Thu Jul 27 11:44:29 2000 +0200
     1.2 +++ b/src/Pure/Thy/thm_deps.ML	Thu Jul 27 18:23:12 2000 +0200
     1.3 @@ -13,7 +13,6 @@
     1.4  signature THM_DEPS =
     1.5  sig
     1.6    include BASIC_THM_DEPS
     1.7 -
     1.8    val enable : unit -> unit
     1.9    val disable : unit -> unit
    1.10  end;
    1.11 @@ -24,19 +23,10 @@
    1.12  fun enable () = Thm.keep_derivs := ThmDeriv;
    1.13  fun disable () = Thm.keep_derivs := MinDeriv;
    1.14  
    1.15 -fun get_sess thy = if Theory.eq_thy (thy, ProtoPure.thy) then ["Pure"]
    1.16 -  else
    1.17 -    (case #session (Present.get_info thy) of
    1.18 -        [x] => [x, "base"]
    1.19 -      | xs => xs);
    1.20 +fun is_internal (name, tags) = name = "" orelse Drule.has_internal tags;
    1.21  
    1.22 -fun put_graph gr path =
    1.23 -    File.write path (cat_lines (map (fn {name, ID, dir, unfold, path, parents} =>
    1.24 -      "\"" ^ name ^ "\" \"" ^ ID ^ "\" \"" ^ dir ^ (if unfold then "\" + \"" else "\" \"") ^
    1.25 -      path ^ "\" > " ^ space_implode " " (map quote parents) ^ " ;") gr));
    1.26 -
    1.27 -fun is_thm_axm (Theorem _) = true
    1.28 -  | is_thm_axm (Axiom _) = true
    1.29 +fun is_thm_axm (Theorem x) = not (is_internal x)
    1.30 +  | is_thm_axm (Axiom x) = not (is_internal x)
    1.31    | is_thm_axm _ = false;
    1.32  
    1.33  fun get_name (Theorem (s, _)) = s
    1.34 @@ -51,12 +41,16 @@
    1.35        if is_none (Symtab.lookup (gra, name)) then
    1.36          let
    1.37            val (gra', parents') = foldl make_deps_graph ((gra, []), ders);
    1.38 -          val prefx = rev (tl (rev (NameSpace.unpack name)));
    1.39 -          val session = (case prefx of
    1.40 -               (x :: _) => (case ThyInfo.lookup_theory x of
    1.41 -                     (Some thy) => get_sess thy
    1.42 -                   | None => [])
    1.43 -             | _ => ["global"])
    1.44 +          val prefx = #1 (Library.split_last (NameSpace.unpack name));
    1.45 +          val session =
    1.46 +            (case prefx of
    1.47 +              (x :: _) =>
    1.48 +                (case ThyInfo.lookup_theory x of
    1.49 +                  Some thy =>
    1.50 +                    let val name = #name (Present.get_info thy)
    1.51 +                    in if name = "" then [] else [name] end 
    1.52 +                | None => [])
    1.53 +             | _ => ["global"]);
    1.54          in
    1.55            (Symtab.update ((name,
    1.56              {name = Sign.base_name name, ID = name,
    1.57 @@ -72,14 +66,13 @@
    1.58    let
    1.59      val _ = writeln "Generating graph ...";
    1.60      val gra = map snd (Symtab.dest (fst (foldl make_deps_graph ((Symtab.empty, []),
    1.61 -      map (#der o rep_thm) thms))));
    1.62 +      map (#der o Thm.rep_thm) thms))));
    1.63      val path = File.tmp_path (Path.unpack "theorems.graph");
    1.64 -    val _ = put_graph gra path;
    1.65 +    val _ = Present.write_graph gra path;
    1.66      val _ = system ("$ISATOOL browser -d " ^ Path.pack (Path.expand path) ^ " &");
    1.67    in () end;
    1.68  
    1.69  end;
    1.70  
    1.71  structure BasicThmDeps : BASIC_THM_DEPS = ThmDeps;
    1.72 -
    1.73  open BasicThmDeps;