src/Pure/PIDE/resources.scala
changeset 65361 ecefb68dc21d
parent 65359 9ca34f0407a9
child 65362 908a27a4b9c9
     1.1 --- a/src/Pure/PIDE/resources.scala	Mon Apr 03 16:50:44 2017 +0200
     1.2 +++ b/src/Pure/PIDE/resources.scala	Mon Apr 03 17:00:36 2017 +0200
     1.3 @@ -15,7 +15,7 @@
     1.4  
     1.5  class Resources(
     1.6    val session_name: String,
     1.7 -  val base: Sessions.Base,
     1.8 +  val session_base: Sessions.Base,
     1.9    val log: Logger = No_Logger)
    1.10  {
    1.11    val thy_info = new Thy_Info(this)
    1.12 @@ -81,10 +81,10 @@
    1.13    {
    1.14      val thy1 = Thy_Header.base_name(s)
    1.15      val thy2 = if (Long_Name.is_qualified(thy1)) thy1 else Long_Name.qualify(session_name, thy1)
    1.16 -    (base.known_theories.get(thy1) orElse
    1.17 -     base.known_theories.get(thy2) orElse
    1.18 -     base.known_theories.get(Long_Name.base_name(thy1))) match {
    1.19 -      case Some(name) if base.loaded_theory(name) => Document.Node.Name.theory(name.theory)
    1.20 +    (session_base.known_theories.get(thy1) orElse
    1.21 +     session_base.known_theories.get(thy2) orElse
    1.22 +     session_base.known_theories.get(Long_Name.base_name(thy1))) match {
    1.23 +      case Some(name) if session_base.loaded_theory(name) => Document.Node.Name.theory(name.theory)
    1.24        case Some(name) => name
    1.25        case None =>
    1.26          val path = Path.explode(s)
    1.27 @@ -150,7 +150,7 @@
    1.28    def undefined_blobs(nodes: Document.Nodes): List[Document.Node.Name] =
    1.29      (for {
    1.30        (node_name, node) <- nodes.iterator
    1.31 -      if !base.loaded_theory(node_name)
    1.32 +      if !session_base.loaded_theory(node_name)
    1.33        cmd <- node.load_commands.iterator
    1.34        name <- cmd.blobs_undefined.iterator
    1.35      } yield name).toList