src/Pure/Thy/thy_resources.scala
changeset 67940 b4e80f062fbf
parent 67939 544a7a21298e
child 67943 b45f0c0ea14f
     1.1 --- a/src/Pure/Thy/thy_resources.scala	Fri Mar 23 22:44:43 2018 +0100
     1.2 +++ b/src/Pure/Thy/thy_resources.scala	Fri Mar 23 22:53:32 2018 +0100
     1.3 @@ -90,7 +90,7 @@
     1.4      /* theories */
     1.5  
     1.6      def use_theories(
     1.7 -      theories: List[(String, Position.T)],
     1.8 +      theories: List[String],
     1.9        qualifier: String = Sessions.DRAFT,
    1.10        master_dir: String = "",
    1.11        id: UUID = UUID(),
    1.12 @@ -231,15 +231,12 @@
    1.13    def load_theories(
    1.14      session: Session,
    1.15      id: UUID,
    1.16 -    theories: List[(String, Position.T)],
    1.17 +    theories: List[String],
    1.18      qualifier: String = Sessions.DRAFT,
    1.19      master_dir: String = "",
    1.20      progress: Progress = No_Progress): List[Document.Node.Name] =
    1.21    {
    1.22 -    val import_names =
    1.23 -      for ((thy, pos) <- theories)
    1.24 -      yield (import_name(qualifier, master_dir, thy), pos)
    1.25 -
    1.26 +    val import_names = theories.map(thy => import_name(qualifier, master_dir, thy) -> Position.none)
    1.27      val dependencies = resources.dependencies(import_names, progress = progress).check_errors
    1.28      val dep_theories = dependencies.theories
    1.29