tuned;
authorwenzelm
Thu Jul 27 18:23:12 2000 +0200 (2000-07-27)
changeset 9450c97dba47e504
parent 9449 2f814053a6cc
child 9451 5c25ed3c10a0
tuned;
src/HOL/Induct/ROOT.ML
src/Pure/Thy/thm_deps.ML
     1.1 --- a/src/HOL/Induct/ROOT.ML	Thu Jul 27 11:44:29 2000 +0200
     1.2 +++ b/src/HOL/Induct/ROOT.ML	Thu Jul 27 18:23:12 2000 +0200
     1.3 @@ -1,9 +1,6 @@
     1.4 -(*  Title:      HOL/Induct/ROOT
     1.5 -    ID:         $Id$
     1.6 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7 -    Copyright   1997  University of Cambridge
     1.8 +(*  Title:      HOL/Induct/ROOT.ML
     1.9  
    1.10 -Examples of Inductive and Coinductive Definitions
    1.11 +Examples of Inductive and Coinductive Definitions.
    1.12  *)
    1.13  
    1.14  time_use_thy "Perm";
     2.1 --- a/src/Pure/Thy/thm_deps.ML	Thu Jul 27 11:44:29 2000 +0200
     2.2 +++ b/src/Pure/Thy/thm_deps.ML	Thu Jul 27 18:23:12 2000 +0200
     2.3 @@ -13,7 +13,6 @@
     2.4  signature THM_DEPS =
     2.5  sig
     2.6    include BASIC_THM_DEPS
     2.7 -
     2.8    val enable : unit -> unit
     2.9    val disable : unit -> unit
    2.10  end;
    2.11 @@ -24,19 +23,10 @@
    2.12  fun enable () = Thm.keep_derivs := ThmDeriv;
    2.13  fun disable () = Thm.keep_derivs := MinDeriv;
    2.14  
    2.15 -fun get_sess thy = if Theory.eq_thy (thy, ProtoPure.thy) then ["Pure"]
    2.16 -  else
    2.17 -    (case #session (Present.get_info thy) of
    2.18 -        [x] => [x, "base"]
    2.19 -      | xs => xs);
    2.20 +fun is_internal (name, tags) = name = "" orelse Drule.has_internal tags;
    2.21  
    2.22 -fun put_graph gr path =
    2.23 -    File.write path (cat_lines (map (fn {name, ID, dir, unfold, path, parents} =>
    2.24 -      "\"" ^ name ^ "\" \"" ^ ID ^ "\" \"" ^ dir ^ (if unfold then "\" + \"" else "\" \"") ^
    2.25 -      path ^ "\" > " ^ space_implode " " (map quote parents) ^ " ;") gr));
    2.26 -
    2.27 -fun is_thm_axm (Theorem _) = true
    2.28 -  | is_thm_axm (Axiom _) = true
    2.29 +fun is_thm_axm (Theorem x) = not (is_internal x)
    2.30 +  | is_thm_axm (Axiom x) = not (is_internal x)
    2.31    | is_thm_axm _ = false;
    2.32  
    2.33  fun get_name (Theorem (s, _)) = s
    2.34 @@ -51,12 +41,16 @@
    2.35        if is_none (Symtab.lookup (gra, name)) then
    2.36          let
    2.37            val (gra', parents') = foldl make_deps_graph ((gra, []), ders);
    2.38 -          val prefx = rev (tl (rev (NameSpace.unpack name)));
    2.39 -          val session = (case prefx of
    2.40 -               (x :: _) => (case ThyInfo.lookup_theory x of
    2.41 -                     (Some thy) => get_sess thy
    2.42 -                   | None => [])
    2.43 -             | _ => ["global"])
    2.44 +          val prefx = #1 (Library.split_last (NameSpace.unpack name));
    2.45 +          val session =
    2.46 +            (case prefx of
    2.47 +              (x :: _) =>
    2.48 +                (case ThyInfo.lookup_theory x of
    2.49 +                  Some thy =>
    2.50 +                    let val name = #name (Present.get_info thy)
    2.51 +                    in if name = "" then [] else [name] end 
    2.52 +                | None => [])
    2.53 +             | _ => ["global"]);
    2.54          in
    2.55            (Symtab.update ((name,
    2.56              {name = Sign.base_name name, ID = name,
    2.57 @@ -72,14 +66,13 @@
    2.58    let
    2.59      val _ = writeln "Generating graph ...";
    2.60      val gra = map snd (Symtab.dest (fst (foldl make_deps_graph ((Symtab.empty, []),
    2.61 -      map (#der o rep_thm) thms))));
    2.62 +      map (#der o Thm.rep_thm) thms))));
    2.63      val path = File.tmp_path (Path.unpack "theorems.graph");
    2.64 -    val _ = put_graph gra path;
    2.65 +    val _ = Present.write_graph gra path;
    2.66      val _ = system ("$ISATOOL browser -d " ^ Path.pack (Path.expand path) ^ " &");
    2.67    in () end;
    2.68  
    2.69  end;
    2.70  
    2.71  structure BasicThmDeps : BASIC_THM_DEPS = ThmDeps;
    2.72 -
    2.73  open BasicThmDeps;