tuned signature;
authorwenzelm
Thu Apr 20 15:00:32 2017 +0200 (2017-04-20)
changeset 655240910f1733909
parent 65523 4f2954adc217
child 65525 360063716c71
tuned signature;
src/Pure/Thy/sessions.scala
src/Tools/VSCode/src/vscode_resources.scala
src/Tools/jEdit/src/jedit_resources.scala
     1.1 --- a/src/Pure/Thy/sessions.scala	Thu Apr 20 14:59:57 2017 +0200
     1.2 +++ b/src/Pure/Thy/sessions.scala	Thu Apr 20 15:00:32 2017 +0200
     1.3 @@ -81,6 +81,9 @@
     1.4        copy(theories = for ((a, b) <- theories) yield (a, b.map(File.platform_path(_))),
     1.5          theories_local = for ((a, b) <- theories_local) yield (a, b.map(File.platform_path(_))),
     1.6          files = for ((a, b) <- files) yield (a, b.map(c => c.map(File.platform_path(_)))))
     1.7 +
     1.8 +    def get_file(file: JFile): Option[Document.Node.Name] =
     1.9 +      files.getOrElse(file.getCanonicalFile, Nil).headOption
    1.10    }
    1.11  
    1.12    object Base
    1.13 @@ -111,9 +114,6 @@
    1.14      def known_theory(name: String): Option[Document.Node.Name] =
    1.15        known.theories.get(name)
    1.16  
    1.17 -    def known_file(file: JFile): Option[Document.Node.Name] =
    1.18 -      known.files.getOrElse(file.getCanonicalFile, Nil).headOption
    1.19 -
    1.20      def dest_known_theories: List[(String, String)] =
    1.21        for ((theory, node_name) <- known.theories.toList)
    1.22          yield (theory, node_name.node)
     2.1 --- a/src/Tools/VSCode/src/vscode_resources.scala	Thu Apr 20 14:59:57 2017 +0200
     2.2 +++ b/src/Tools/VSCode/src/vscode_resources.scala	Thu Apr 20 15:00:32 2017 +0200
     2.3 @@ -61,7 +61,7 @@
     2.4    def node_file(name: Document.Node.Name): JFile = new JFile(name.node)
     2.5  
     2.6    def node_name(file: JFile): Document.Node.Name =
     2.7 -    session_base.known_file(file) getOrElse {
     2.8 +    session_base.known.get_file(file) getOrElse {
     2.9        val node = file.getPath
    2.10        theory_name(default_qualifier, Thy_Header.theory_name(node)) match {
    2.11          case (true, theory) => Document.Node.Name.loaded_theory(theory)
     3.1 --- a/src/Tools/jEdit/src/jedit_resources.scala	Thu Apr 20 14:59:57 2017 +0200
     3.2 +++ b/src/Tools/jEdit/src/jedit_resources.scala	Thu Apr 20 15:00:32 2017 +0200
     3.3 @@ -26,7 +26,7 @@
     3.4    /* document node name */
     3.5  
     3.6    def known_file(path: String): Option[Document.Node.Name] =
     3.7 -    JEdit_Lib.check_file(path).flatMap(session_base.known_file(_))
     3.8 +    JEdit_Lib.check_file(path).flatMap(session_base.known.get_file(_))
     3.9  
    3.10    def node_name(path: String): Document.Node.Name =
    3.11      known_file(path) getOrElse {