src/Pure/Thy/sessions.scala
changeset 66668 6019cfb8256c
parent 66604 1af360d1cad2
child 66694 41177b124067
     1.1 --- a/src/Pure/Thy/sessions.scala	Fri Sep 15 19:56:23 2017 +0200
     1.2 +++ b/src/Pure/Thy/sessions.scala	Sat Sep 16 15:35:56 2017 +0200
     1.3 @@ -81,6 +81,11 @@
     1.4          theories_local = for ((a, b) <- theories_local) yield (a, b.map(File.platform_path(_))),
     1.5          files = for ((a, b) <- files) yield (a, b.map(c => c.map(File.platform_path(_)))))
     1.6  
     1.7 +    def standard_path: Known =
     1.8 +      copy(theories = for ((a, b) <- theories) yield (a, b.map(File.standard_path(_))),
     1.9 +        theories_local = for ((a, b) <- theories_local) yield (a, b.map(File.standard_path(_))),
    1.10 +        files = for ((a, b) <- files) yield (a, b.map(c => c.map(File.standard_path(_)))))
    1.11 +
    1.12      def get_file(file: JFile, bootstrap: Boolean = false): Option[Document.Node.Name] =
    1.13      {
    1.14        val res = files.getOrElse(File.canonical(file), Nil).headOption
    1.15 @@ -114,6 +119,7 @@
    1.16      def get_imports: Base = imports getOrElse Base.bootstrap(global_theories)
    1.17  
    1.18      def platform_path: Base = copy(known = known.platform_path)
    1.19 +    def standard_path: Base = copy(known = known.standard_path)
    1.20  
    1.21      def loaded_theory(name: Document.Node.Name): Boolean =
    1.22        loaded_theories.isDefinedAt(name.theory)