src/Pure/Thy/thy_load.scala

--- a/src/Pure/Thy/thy_load.scala	Tue Aug 21 11:00:54 2012 +0200
+++ b/src/Pure/Thy/thy_load.scala	Tue Aug 21 12:15:25 2012 +0200
@@ -20,22 +20,8 @@
 }
 
 
-class Thy_Load(preloaded: Set[String] = Set.empty)
+class Thy_Load(val loaded_theories: Set[String] = Set.empty, val base_syntax: Outer_Syntax)
 {
-  /* loaded theories provided by prover */
-
-  private var loaded_theories: Set[String] = preloaded
-
-  def register_thy(name: String): Unit =
-    synchronized { loaded_theories += name }
-
-  def register_thys(names: Set[String]): Unit =
-    synchronized { loaded_theories ++= names }
-
-  def is_loaded(thy_name: String): Boolean =
-    synchronized { loaded_theories.contains(thy_name) }
-
-
   /* file-system operations */
 
   def append(dir: String, source_path: Path): String =
@@ -54,7 +40,7 @@
   private def import_name(dir: String, s: String): Document.Node.Name =
   {
     val theory = Thy_Header.base_name(s)
-    if (is_loaded(theory)) Document.Node.Name(theory, "", theory)
+    if (loaded_theories(theory)) Document.Node.Name(theory, "", theory)
     else {
       val path = Path.explode(s)
       val node = append(dir, Thy_Load.thy_path(path))