clarified theory_name vs. loaded_theory: proper import_name for already loaded theories from other sessions (amending 4c98c929a12a);
authorwenzelm
Tue Nov 28 22:14:10 2017 +0100 (4 months ago)
changeset 67104a2fa0c6a7aff
parent 67103 39cc38a06610
child 67105 05ff3e6dbbce
clarified theory_name vs. loaded_theory: proper import_name for already loaded theories from other sessions (amending 4c98c929a12a);
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	Mon Nov 27 16:57:34 2017 +0100
     1.2 +++ b/src/Pure/PIDE/resources.ML	Tue Nov 28 22:14:10 2017 +0100
     1.3 @@ -108,26 +108,24 @@
     1.4    | NONE => Long_Name.qualifier theory);
     1.5  
     1.6  fun theory_name qualifier theory =
     1.7 -  if loaded_theory theory then (true, theory)
     1.8 -  else
     1.9 -    let val theory' =
    1.10 -      if Long_Name.is_qualified theory orelse is_some (global_theory theory)
    1.11 -      then theory
    1.12 -      else Long_Name.qualify qualifier theory
    1.13 -    in (false, theory') end;
    1.14 +  if Long_Name.is_qualified theory orelse is_some (global_theory theory)
    1.15 +  then theory
    1.16 +  else Long_Name.qualify qualifier theory;
    1.17  
    1.18  fun import_name qualifier dir s =
    1.19 -  (case theory_name qualifier (Thy_Header.import_name s) of
    1.20 -    (true, theory) => {master_dir = Path.current, theory_name = theory}
    1.21 -  | (false, theory) =>
    1.22 -      let val node_name =
    1.23 -        (case known_theory theory of
    1.24 -          SOME node_name => node_name
    1.25 -        | NONE =>
    1.26 -            if Thy_Header.is_base_name s andalso Long_Name.is_qualified s
    1.27 -            then Path.explode s
    1.28 -            else File.full_path dir (thy_path (Path.expand (Path.explode s))))
    1.29 -      in {master_dir = Path.dir node_name, theory_name = theory} end);
    1.30 +  let val theory = theory_name qualifier (Thy_Header.import_name s) in
    1.31 +    if loaded_theory theory then {master_dir = Path.current, theory_name = theory}
    1.32 +    else
    1.33 +      let
    1.34 +        val node_name =
    1.35 +          (case known_theory theory of
    1.36 +            SOME node_name => node_name
    1.37 +          | NONE =>
    1.38 +              if Thy_Header.is_base_name s andalso Long_Name.is_qualified s
    1.39 +              then Path.explode s
    1.40 +              else File.full_path dir (thy_path (Path.expand (Path.explode s))));
    1.41 +      in {master_dir = Path.dir node_name, theory_name = theory} end
    1.42 +  end;
    1.43  
    1.44  fun check_file dir file = File.check_file (File.full_path dir file);
    1.45  
     2.1 --- a/src/Pure/PIDE/resources.scala	Mon Nov 27 16:57:34 2017 +0100
     2.2 +++ b/src/Pure/PIDE/resources.scala	Tue Nov 28 22:14:10 2017 +0100
     2.3 @@ -86,33 +86,30 @@
     2.4      roots ::: files
     2.5    }
     2.6  
     2.7 -  def theory_name(qualifier: String, theory: String): (Boolean, String) =
     2.8 -    if (session_base.loaded_theory(theory)) (true, theory)
     2.9 -    else {
    2.10 -      val theory1 =
    2.11 -        if (Long_Name.is_qualified(theory) || session_base.global_theories.isDefinedAt(theory))
    2.12 -          theory
    2.13 -        else Long_Name.qualify(qualifier, theory)
    2.14 -      (false, theory1)
    2.15 -    }
    2.16 +  def theory_name(qualifier: String, theory: String): String =
    2.17 +    if (Long_Name.is_qualified(theory) || session_base.global_theories.isDefinedAt(theory))
    2.18 +      theory
    2.19 +    else Long_Name.qualify(qualifier, theory)
    2.20  
    2.21    def import_name(qualifier: String, dir: String, s: String): Document.Node.Name =
    2.22 -    theory_name(qualifier, Thy_Header.import_name(s)) match {
    2.23 -      case (true, theory) => Document.Node.Name.loaded_theory(theory)
    2.24 -      case (false, theory) =>
    2.25 -        session_base.known_theory(theory) match {
    2.26 -          case Some(node_name) => node_name
    2.27 -          case None =>
    2.28 -            if (Thy_Header.is_base_name(s) && Long_Name.is_qualified(s))
    2.29 -              Document.Node.Name.loaded_theory(theory)
    2.30 -            else {
    2.31 -              val path = Path.explode(s)
    2.32 -              val node = append(dir, thy_path(path))
    2.33 -              val master_dir = append(dir, path.dir)
    2.34 -              Document.Node.Name(node, master_dir, theory)
    2.35 -            }
    2.36 -        }
    2.37 +  {
    2.38 +    val theory = theory_name(qualifier, Thy_Header.import_name(s))
    2.39 +    if (session_base.loaded_theory(theory)) Document.Node.Name.loaded_theory(theory)
    2.40 +    else {
    2.41 +      session_base.known_theory(theory) match {
    2.42 +        case Some(node_name) => node_name
    2.43 +        case None =>
    2.44 +          if (Thy_Header.is_base_name(s) && Long_Name.is_qualified(s))
    2.45 +            Document.Node.Name.loaded_theory(theory)
    2.46 +          else {
    2.47 +            val path = Path.explode(s)
    2.48 +            val node = append(dir, thy_path(path))
    2.49 +            val master_dir = append(dir, path.dir)
    2.50 +            Document.Node.Name(node, master_dir, theory)
    2.51 +          }
    2.52 +      }
    2.53      }
    2.54 +  }
    2.55  
    2.56    def import_name(name: Document.Node.Name, s: String): Document.Node.Name =
    2.57      import_name(session_base.theory_qualifier(name), name.master_dir, s)
     3.1 --- a/src/Tools/VSCode/src/vscode_resources.scala	Mon Nov 27 16:57:34 2017 +0100
     3.2 +++ b/src/Tools/VSCode/src/vscode_resources.scala	Tue Nov 28 22:14:10 2017 +0100
     3.3 @@ -93,11 +93,11 @@
     3.4    def node_name(file: JFile): Document.Node.Name =
     3.5      session_base.known.get_file(file, bootstrap = true) getOrElse {
     3.6        val node = file.getPath
     3.7 -      theory_name(Sessions.DRAFT, Thy_Header.theory_name(node)) match {
     3.8 -        case (true, theory) => Document.Node.Name.loaded_theory(theory)
     3.9 -        case (false, theory) =>
    3.10 -          val master_dir = if (theory == "") "" else file.getParent
    3.11 -          Document.Node.Name(node, master_dir, theory)
    3.12 +      val theory = theory_name(Sessions.DRAFT, Thy_Header.theory_name(node))
    3.13 +      if (session_base.loaded_theory(theory)) Document.Node.Name.loaded_theory(theory)
    3.14 +      else {
    3.15 +        val master_dir = if (theory == "") "" else file.getParent
    3.16 +        Document.Node.Name(node, master_dir, theory)
    3.17        }
    3.18      }
    3.19  
     4.1 --- a/src/Tools/jEdit/src/jedit_resources.scala	Mon Nov 27 16:57:34 2017 +0100
     4.2 +++ b/src/Tools/jEdit/src/jedit_resources.scala	Tue Nov 28 22:14:10 2017 +0100
     4.3 @@ -43,11 +43,11 @@
     4.4      known_file(path) getOrElse {
     4.5        val vfs = VFSManager.getVFSForPath(path)
     4.6        val node = if (vfs.isInstanceOf[FileVFS]) MiscUtilities.resolveSymlinks(path) else path
     4.7 -      theory_name(Sessions.DRAFT, Thy_Header.theory_name(node)) match {
     4.8 -        case (true, theory) => Document.Node.Name.loaded_theory(theory)
     4.9 -        case (false, theory) =>
    4.10 -          val master_dir = if (theory == "") "" else vfs.getParentOfPath(path)
    4.11 -          Document.Node.Name(node, master_dir, theory)
    4.12 +      val theory = theory_name(Sessions.DRAFT, Thy_Header.theory_name(node))
    4.13 +      if (session_base.loaded_theory(theory)) Document.Node.Name.loaded_theory(theory)
    4.14 +      else {
    4.15 +        val master_dir = if (theory == "") "" else vfs.getParentOfPath(path)
    4.16 +        Document.Node.Name(node, master_dir, theory)
    4.17        }
    4.18      }
    4.19