proper standard_path to revert platform_path in JEdit_Sessions.session_base;
authorwenzelm
Sat Sep 16 15:35:56 2017 +0200 (21 months ago)
changeset 666686019cfb8256c
parent 66667 2e580fcf6522
child 66669 bbcb75c58086
proper standard_path to revert platform_path in JEdit_Sessions.session_base;
src/Pure/PIDE/protocol.scala
src/Pure/Thy/sessions.scala
     1.1 --- a/src/Pure/PIDE/protocol.scala	Fri Sep 15 19:56:23 2017 +0200
     1.2 +++ b/src/Pure/PIDE/protocol.scala	Sat Sep 16 15:35:56 2017 +0200
     1.3 @@ -316,11 +316,14 @@
     1.4      Symbol.encode_yxml(list(pair(string, string))(table))
     1.5    }
     1.6  
     1.7 -  def session_base(resources: Resources): Unit =
     1.8 +  def session_base(resources: Resources)
     1.9 +  {
    1.10 +    val base = resources.session_base.standard_path
    1.11      protocol_command("Prover.session_base",
    1.12 -      encode_table(resources.session_base.global_theories.toList),
    1.13 -      encode_table(resources.session_base.loaded_theories.toList),
    1.14 -      encode_table(resources.session_base.dest_known_theories))
    1.15 +      encode_table(base.global_theories.toList),
    1.16 +      encode_table(base.loaded_theories.toList),
    1.17 +      encode_table(base.dest_known_theories))
    1.18 +  }
    1.19  
    1.20  
    1.21    /* interned items */
     2.1 --- a/src/Pure/Thy/sessions.scala	Fri Sep 15 19:56:23 2017 +0200
     2.2 +++ b/src/Pure/Thy/sessions.scala	Sat Sep 16 15:35:56 2017 +0200
     2.3 @@ -81,6 +81,11 @@
     2.4          theories_local = for ((a, b) <- theories_local) yield (a, b.map(File.platform_path(_))),
     2.5          files = for ((a, b) <- files) yield (a, b.map(c => c.map(File.platform_path(_)))))
     2.6  
     2.7 +    def standard_path: Known =
     2.8 +      copy(theories = for ((a, b) <- theories) yield (a, b.map(File.standard_path(_))),
     2.9 +        theories_local = for ((a, b) <- theories_local) yield (a, b.map(File.standard_path(_))),
    2.10 +        files = for ((a, b) <- files) yield (a, b.map(c => c.map(File.standard_path(_)))))
    2.11 +
    2.12      def get_file(file: JFile, bootstrap: Boolean = false): Option[Document.Node.Name] =
    2.13      {
    2.14        val res = files.getOrElse(File.canonical(file), Nil).headOption
    2.15 @@ -114,6 +119,7 @@
    2.16      def get_imports: Base = imports getOrElse Base.bootstrap(global_theories)
    2.17  
    2.18      def platform_path: Base = copy(known = known.platform_path)
    2.19 +    def standard_path: Base = copy(known = known.standard_path)
    2.20  
    2.21      def loaded_theory(name: Document.Node.Name): Boolean =
    2.22        loaded_theories.isDefinedAt(name.theory)