tuned signature (again);
authorwenzelm
Thu Apr 13 12:19:28 2017 +0200 (2017-04-13)
changeset 65476a72ae9eb4462
parent 65475 4519c8cc4bec
child 65477 64e61b0f6972
tuned signature (again);
src/Pure/PIDE/resources.ML
src/Pure/PIDE/resources.scala
src/Tools/VSCode/src/vscode_resources.scala
src/Tools/jEdit/src/jedit_resources.scala
     1.1 --- a/src/Pure/PIDE/resources.ML	Wed Apr 12 23:44:33 2017 +0200
     1.2 +++ b/src/Pure/PIDE/resources.ML	Thu Apr 13 12:19:28 2017 +0200
     1.3 @@ -108,7 +108,7 @@
     1.4      SOME qualifier => qualifier
     1.5    | NONE => Long_Name.qualifier theory);
     1.6  
     1.7 -fun loaded_theory_name qualifier theory0 =
     1.8 +fun theory_name qualifier theory0 =
     1.9    (case loaded_theory theory0 of
    1.10      SOME theory => (true, theory)
    1.11    | NONE =>
    1.12 @@ -119,7 +119,7 @@
    1.13        in (false, theory) end);
    1.14  
    1.15  fun import_name qualifier dir s =
    1.16 -  (case loaded_theory_name qualifier (Thy_Header.import_name s) of
    1.17 +  (case theory_name qualifier (Thy_Header.import_name s) of
    1.18      (true, theory) =>
    1.19        {node_name = Path.basic theory, master_dir = Path.current, theory_name = theory}
    1.20    | (false, theory) =>
     2.1 --- a/src/Pure/PIDE/resources.scala	Wed Apr 12 23:44:33 2017 +0200
     2.2 +++ b/src/Pure/PIDE/resources.scala	Thu Apr 13 12:19:28 2017 +0200
     2.3 @@ -70,7 +70,7 @@
     2.4    def theory_qualifier(name: Document.Node.Name): String =
     2.5      session_base.global_theories.getOrElse(name.theory, Long_Name.qualifier(name.theory))
     2.6  
     2.7 -  def loaded_theory_name(qualifier: String, theory0: String): (Boolean, String) =
     2.8 +  def theory_name(qualifier: String, theory0: String): (Boolean, String) =
     2.9      session_base.loaded_theories.get(theory0) match {
    2.10        case Some(theory) => (true, theory)
    2.11        case None =>
    2.12 @@ -82,7 +82,7 @@
    2.13      }
    2.14  
    2.15    def import_name(qualifier: String, dir: String, s: String): Document.Node.Name =
    2.16 -    loaded_theory_name(qualifier, Thy_Header.import_name(s)) match {
    2.17 +    theory_name(qualifier, Thy_Header.import_name(s)) match {
    2.18        case (true, theory) => Document.Node.Name.loaded_theory(theory)
    2.19        case (false, theory) =>
    2.20          session_base.known_theories.get(theory) match {
     3.1 --- a/src/Tools/VSCode/src/vscode_resources.scala	Wed Apr 12 23:44:33 2017 +0200
     3.2 +++ b/src/Tools/VSCode/src/vscode_resources.scala	Thu Apr 13 12:19:28 2017 +0200
     3.3 @@ -63,7 +63,7 @@
     3.4    def node_name(file: JFile): Document.Node.Name =
     3.5    {
     3.6      val node = file.getPath
     3.7 -    loaded_theory_name(default_qualifier, Thy_Header.theory_name(node)) match {
     3.8 +    theory_name(default_qualifier, Thy_Header.theory_name(node)) match {
     3.9        case (true, theory) => Document.Node.Name.loaded_theory(theory)
    3.10        case (false, theory) =>
    3.11          val master_dir = if (theory == "") "" else file.getParent
     4.1 --- a/src/Tools/jEdit/src/jedit_resources.scala	Wed Apr 12 23:44:33 2017 +0200
     4.2 +++ b/src/Tools/jEdit/src/jedit_resources.scala	Thu Apr 13 12:19:28 2017 +0200
     4.3 @@ -29,7 +29,7 @@
     4.4    {
     4.5      val vfs = VFSManager.getVFSForPath(path)
     4.6      val node = if (vfs.isInstanceOf[FileVFS]) MiscUtilities.resolveSymlinks(path) else path
     4.7 -    loaded_theory_name(default_qualifier, Thy_Header.theory_name(node)) match {
     4.8 +    theory_name(default_qualifier, Thy_Header.theory_name(node)) match {
     4.9        case (true, theory) => Document.Node.Name.loaded_theory(theory)
    4.10        case (false, theory) =>
    4.11          val master_dir = if (theory == "") "" else vfs.getParentOfPath(path)