Update for Isabelle99-2

1 files changed, 31 insertions, 24 deletions

diff --git a/isa/depends.ML b/isa/depends.ML
index d55b7552..a18125a8 100644
--- a/isa/depends.ML
+++ b/isa/depends.ML
@@ -1,22 +1,25 @@
+(* depends.ML
 
-fun enable () = Thm.keep_derivs := ThmDeriv;
-fun disable () = Thm.keep_derivs := MinDeriv;
+   Experimental code for communicating theorem dependencies from Isabelle
+   to Proof General.
 
-enable();
+   This code is taken from thm_deps.ML in Isabelle 99-2.  It's incompatible
+   with other Isabelle versions.
 
-fun get_sess thy = if Theory.eq_thy (thy, ProtoPure.thy) then ["Pure"]
-  else
-    (case #session (Present.get_info thy) of
-        [x] => [x, "base"]
-      | xs => xs);
+   It is duplicated almost verbatim because what we need is
+   hardwired to a call on the browser tool.
+*)
 
-fun put_graph gr path =
-    File.write path (cat_lines (map (fn {name, ID, dir, unfold, path, parents} =>
-      "\"" ^ name ^ "\" \"" ^ ID ^ "\" \"" ^ dir ^ (if unfold then "\" + \"" else "\" \"") ^
-      path ^ "\" > " ^ space_implode " " (map quote parents) ^ " ;") gr));
 
-fun is_thm_axm (Theorem _) = true
-  | is_thm_axm (Axiom _) = true
+fun depends_enable () = Thm.keep_derivs := ThmDeriv;
+fun depends_disable () = Thm.keep_derivs := MinDeriv;
+
+
+
+fun is_internal (name, tags) = name = "" orelse Drule.has_internal tags;
+
+fun is_thm_axm (Theorem x) = not (is_internal x)
+  | is_thm_axm (Axiom x) = not (is_internal x)
   | is_thm_axm _ = false;
 
 fun get_name (Theorem (s, _)) = s
@@ -31,12 +34,16 @@ fun make_deps_graph ((gra, parents), Join (ta, ders)) =
       if is_none (Symtab.lookup (gra, name)) then
         let
           val (gra', parents') = foldl make_deps_graph ((gra, []), ders);
-          val prefx = rev (tl (rev (NameSpace.unpack name)));
-          val session = (case prefx of
-               (x :: _) => (case ThyInfo.lookup_theory x of
-                     (Some thy) => get_sess thy
-                   | None => [])
-             | _ => ["global"])
+          val prefx = #1 (Library.split_last (NameSpace.unpack name));
+          val session =
+            (case prefx of
+              (x :: _) =>
+                (case ThyInfo.lookup_theory x of
+                  Some thy =>
+                    let val name = #name (Present.get_info thy)
+                    in if name = "" then [] else [name] end 
+                | None => [])
+             | _ => ["global"]);
         in
           (Symtab.update ((name,
             {name = Sign.base_name name, ID = name,
@@ -52,9 +59,9 @@ fun thm_deps thms =
   let
     val _ = writeln "Generating graph ...";
     val gra = map snd (Symtab.dest (fst (foldl make_deps_graph ((Symtab.empty, []),
-      map (#der o rep_thm) thms))));
+      map (#2 o #der o Thm.rep_thm) thms))));
     val path = File.tmp_path (Path.unpack "theorems.graph");
-    val _ = put_graph gra path;
+    val _ = Present.write_graph gra path;
     val _ = system ("$ISATOOL browser -d " ^ Path.pack (Path.expand path) ^ " &");
   in () end;
 
@@ -62,10 +69,10 @@ fun new_thm_deps thms =
   let
     val header = "Proof General, the theorem dependencies are: \"";
     val gra = map snd (Symtab.dest (fst (foldl make_deps_graph ((Symtab.empty, []),
-      map (#der o rep_thm) thms))));
+      map (#2 o #der o Thm.rep_thm) thms))));
     val deps = foldl (op@) ([],(map #parents gra))
     val msg = header ^ (space_implode " " deps) ^ "\""
-  in writeln msg end;
+  in priority msg end;
 
 val old_qed = qed;