# HG changeset patch # User wenzelm # Date 1491247067 -7200 # Node ID 908a27a4b9c93862efccc1ea2b5349d9fe9b2300 # Parent ecefb68dc21d31c5304c37c4298a68c906b9de4a clarified imports; diff -r ecefb68dc21d -r 908a27a4b9c9 src/Pure/PIDE/resources.scala --- a/src/Pure/PIDE/resources.scala Mon Apr 03 17:00:36 2017 +0200 +++ b/src/Pure/PIDE/resources.scala Mon Apr 03 21:17:47 2017 +0200 @@ -79,22 +79,26 @@ def import_name(master: Document.Node.Name, s: String): Document.Node.Name = { - val thy1 = Thy_Header.base_name(s) - val thy2 = if (Long_Name.is_qualified(thy1)) thy1 else Long_Name.qualify(session_name, thy1) - (session_base.known_theories.get(thy1) orElse - session_base.known_theories.get(thy2) orElse - session_base.known_theories.get(Long_Name.base_name(thy1))) match { + val theory = Thy_Header.base_name(s) + val is_base_name = Thy_Header.is_base_name(s) + val is_qualified = is_base_name && Long_Name.is_qualified(s) + + val known_theory = + if (is_base_name) + session_base.known_theories.get(theory) orElse + (if (is_qualified) session_base.known_theories.get(Long_Name.base_name(theory)) + else session_base.known_theories.get(Long_Name.qualify(session_name, theory))) + else None + + known_theory match { case Some(name) if session_base.loaded_theory(name) => Document.Node.Name.theory(name.theory) case Some(name) => name + case None if is_qualified => Document.Node.Name.theory(theory) case None => val path = Path.explode(s) - val theory = path.base.implode - if (Long_Name.is_qualified(theory)) Document.Node.Name.theory(theory) - else { - val node = append(master.master_dir, thy_path(path)) - val master_dir = append(master.master_dir, path.dir) - Document.Node.Name(node, master_dir, Long_Name.qualify(session_name, theory)) - } + val node = append(master.master_dir, thy_path(path)) + val master_dir = append(master.master_dir, path.dir) + Document.Node.Name(node, master_dir, Long_Name.qualify(session_name, theory)) } } diff -r ecefb68dc21d -r 908a27a4b9c9 src/Pure/Thy/thy_header.scala --- a/src/Pure/Thy/thy_header.scala Mon Apr 03 17:00:36 2017 +0200 +++ b/src/Pure/Thy/thy_header.scala Mon Apr 03 21:17:47 2017 +0200 @@ -80,6 +80,9 @@ private val Base_Name = new Regex(""".*?([^/\\:]+)""") private val Thy_Name = new Regex(""".*?([^/\\:]+)\.thy""") + def is_base_name(s: String): Boolean = + s != "" && !s.exists("/\\:".contains(_)) + def base_name(s: String): String = s match { case Base_Name(name) => name case _ => error("Malformed import: " + quote(s)) }