src/Pure/Thy/thy_info.scala

--- a/src/Pure/Thy/thy_info.scala	Tue Jul 05 22:38:44 2011 +0200
+++ b/src/Pure/Thy/thy_info.scala	Tue Jul 05 22:39:15 2011 +0200
@@ -7,6 +7,20 @@
 package isabelle
 
 
+object Thy_Info
+{
+  /* protocol messages */
+
+  object Loaded_Theory {
+    def unapply(msg: XML.Tree): Option[String] =
+      msg match {
+        case XML.Elem(Markup(Markup.LOADED_THEORY, List((Markup.NAME, name))), _) => Some(name)
+        case _ => None
+      }
+  }
+}
+
+
 class Thy_Info(thy_load: Thy_Load)
 {
   /* messages */
@@ -26,16 +40,17 @@
 
   type Deps = Map[String, Exn.Result[(String, Thy_Header.Header)]]  // name -> (text, header)
 
-  private def require_thys(
+  private def require_thys(ignored: String => Boolean,
       initiators: List[String], dir: Path, deps: Deps, strs: List[String]): Deps =
-    (deps /: strs)(require_thy(initiators, dir, _, _))
+    (deps /: strs)(require_thy(ignored, initiators, dir, _, _))
 
-  private def require_thy(initiators: List[String], dir: Path, deps: Deps, str: String): Deps =
+  private def require_thy(ignored: String => Boolean,
+      initiators: List[String], dir: Path, deps: Deps, str: String): Deps =
   {
     val path = Path.explode(str)
     val name = path.base.implode
 
-    if (deps.isDefinedAt(name)) deps
+    if (deps.isDefinedAt(name) || ignored(name)) deps
     else {
       val dir1 = dir + path.dir
       try {
@@ -47,7 +62,7 @@
               cat_error(msg, "The error(s) above occurred while examining theory " +
                 quote(name) + required_by("\n", initiators))
           }
-        require_thys(name :: initiators, dir1,
+        require_thys(ignored, name :: initiators, dir1,
           deps + (name -> Exn.Res(text, header)), header.imports)
       }
       catch { case e: Throwable => deps + (name -> Exn.Exn(e)) }
@@ -55,5 +70,5 @@
   }
 
   def dependencies(dir: Path, str: String): Deps =
-    require_thy(Nil, dir, Map.empty, str)  // FIXME capture errors in str (!??)
+    require_thy(thy_load.is_loaded, Nil, dir, Map.empty, str)  // FIXME capture errors in str (!??)
 }