src/Pure/Thy/thy_info.scala
changeset 64854 f5aa712e6250
parent 63584 68751fe1c036
child 65355 403eabd73c9a
     1.1 --- a/src/Pure/Thy/thy_info.scala	Mon Jan 09 19:34:16 2017 +0100
     1.2 +++ b/src/Pure/Thy/thy_info.scala	Mon Jan 09 20:26:59 2017 +0100
     1.3 @@ -71,7 +71,7 @@
     1.4        val import_errors =
     1.5          (for {
     1.6            (theory, names) <- seen_names.iterator_list
     1.7 -          if !resources.loaded_theories(theory)
     1.8 +          if !resources.base.loaded_theories(theory)
     1.9            if names.length > 1
    1.10          } yield
    1.11            "Incoherent imports for theory " + quote(theory) + ":\n" +
    1.12 @@ -83,10 +83,10 @@
    1.13      }
    1.14  
    1.15      lazy val syntax: Outer_Syntax =
    1.16 -      resources.base_syntax.add_keywords(keywords).add_abbrevs(abbrevs)
    1.17 +      resources.base.syntax.add_keywords(keywords).add_abbrevs(abbrevs)
    1.18  
    1.19      def loaded_theories: Set[String] =
    1.20 -      (resources.loaded_theories /: rev_deps) { case (loaded, dep) => loaded + dep.name.theory }
    1.21 +      (resources.base.loaded_theories /: rev_deps) { case (loaded, dep) => loaded + dep.name.theory }
    1.22  
    1.23      def loaded_files: List[Path] =
    1.24      {
    1.25 @@ -118,7 +118,7 @@
    1.26          required_by(initiators) + Position.here(require_pos)
    1.27  
    1.28      val required1 = required + thy
    1.29 -    if (required.seen(name) || resources.loaded_theories(name.theory)) required1
    1.30 +    if (required.seen(name) || resources.base.loaded_theories(name.theory)) required1
    1.31      else {
    1.32        try {
    1.33          if (initiators.contains(name)) error(cycle_msg(initiators))