src/Pure/PIDE/resources.scala
changeset 64854 f5aa712e6250
parent 64839 842163abfc0d
child 64856 5e9bf964510a
     1.1 --- a/src/Pure/PIDE/resources.scala	Mon Jan 09 19:34:16 2017 +0100
     1.2 +++ b/src/Pure/PIDE/resources.scala	Mon Jan 09 20:26:59 2017 +0100
     1.3 @@ -17,14 +17,10 @@
     1.4  {
     1.5    def thy_path(path: Path): Path = path.ext("thy")
     1.6  
     1.7 -  val empty: Resources = new Resources(Set.empty, Map.empty, Outer_Syntax.empty)
     1.8 +  val empty: Resources = new Resources(Build.Session_Content.empty)
     1.9  }
    1.10  
    1.11 -class Resources(
    1.12 -  val loaded_theories: Set[String],
    1.13 -  val known_theories: Map[String, Document.Node.Name],
    1.14 -  val base_syntax: Outer_Syntax,
    1.15 -  val log: Logger = No_Logger)
    1.16 +class Resources(val base: Build.Session_Content, val log: Logger = No_Logger)
    1.17  {
    1.18    val thy_info = new Thy_Info(this)
    1.19  
    1.20 @@ -94,10 +90,10 @@
    1.21      val no_qualifier = "" // FIXME
    1.22      val thy1 = Thy_Header.base_name(s)
    1.23      val thy2 = if (Long_Name.is_qualified(thy1)) thy1 else Long_Name.qualify(no_qualifier, thy1)
    1.24 -    (known_theories.get(thy1) orElse
    1.25 -     known_theories.get(thy2) orElse
    1.26 -     known_theories.get(Long_Name.base_name(thy1))) match {
    1.27 -      case Some(name) if loaded_theories(name.theory) => dummy_name(name.theory)
    1.28 +    (base.known_theories.get(thy1) orElse
    1.29 +     base.known_theories.get(thy2) orElse
    1.30 +     base.known_theories.get(Long_Name.base_name(thy1))) match {
    1.31 +      case Some(name) if base.loaded_theories(name.theory) => dummy_name(name.theory)
    1.32        case Some(name) => name
    1.33        case None =>
    1.34          val path = Path.explode(s)
    1.35 @@ -164,7 +160,7 @@
    1.36    def undefined_blobs(nodes: Document.Nodes): List[Document.Node.Name] =
    1.37      (for {
    1.38        (node_name, node) <- nodes.iterator
    1.39 -      if !loaded_theories(node_name.theory)
    1.40 +      if !base.loaded_theories(node_name.theory)
    1.41        cmd <- node.load_commands.iterator
    1.42        name <- cmd.blobs_undefined.iterator
    1.43      } yield name).toList