src/Pure/Thy/thy_load.scala
changeset 48870 4accee106f0f
parent 48827 8791d106e30b
child 48882 61dc7d5d150a
     1.1 --- a/src/Pure/Thy/thy_load.scala	Tue Aug 21 11:00:54 2012 +0200
     1.2 +++ b/src/Pure/Thy/thy_load.scala	Tue Aug 21 12:15:25 2012 +0200
     1.3 @@ -20,22 +20,8 @@
     1.4  }
     1.5  
     1.6  
     1.7 -class Thy_Load(preloaded: Set[String] = Set.empty)
     1.8 +class Thy_Load(val loaded_theories: Set[String] = Set.empty, val base_syntax: Outer_Syntax)
     1.9  {
    1.10 -  /* loaded theories provided by prover */
    1.11 -
    1.12 -  private var loaded_theories: Set[String] = preloaded
    1.13 -
    1.14 -  def register_thy(name: String): Unit =
    1.15 -    synchronized { loaded_theories += name }
    1.16 -
    1.17 -  def register_thys(names: Set[String]): Unit =
    1.18 -    synchronized { loaded_theories ++= names }
    1.19 -
    1.20 -  def is_loaded(thy_name: String): Boolean =
    1.21 -    synchronized { loaded_theories.contains(thy_name) }
    1.22 -
    1.23 -
    1.24    /* file-system operations */
    1.25  
    1.26    def append(dir: String, source_path: Path): String =
    1.27 @@ -54,7 +40,7 @@
    1.28    private def import_name(dir: String, s: String): Document.Node.Name =
    1.29    {
    1.30      val theory = Thy_Header.base_name(s)
    1.31 -    if (is_loaded(theory)) Document.Node.Name(theory, "", theory)
    1.32 +    if (loaded_theories(theory)) Document.Node.Name(theory, "", theory)
    1.33      else {
    1.34        val path = Path.explode(s)
    1.35        val node = append(dir, Thy_Load.thy_path(path))