# HG changeset patch
# User wenzelm
# Date 1491219553 -7200
# Node ID 9a2c266f97c805ae34044a72e14476718433abe1
# Parent  b96cf915de754439577672cbdb24534022aba01a
simplified direct theory name (again, see also 570ba266f5b5, 2a7f9e79cb28);

diff -r b96cf915de75 -r 9a2c266f97c8 src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Mon Apr 03 12:49:13 2017 +0200
+++ b/src/Pure/PIDE/document.ML	Mon Apr 03 13:39:13 2017 +0200
@@ -178,9 +178,7 @@
   | NONE => false);
 
 fun loaded_theory name =
-  (case try (unsuffix ".thy") name of
-    SOME a => get_first Thy_Info.lookup_theory [a, Long_Name.base_name a]
-  | NONE => NONE);
+  get_first Thy_Info.lookup_theory [name, Long_Name.base_name name];
 
 fun get_node nodes name = String_Graph.get_node nodes name
   handle String_Graph.UNDEF _ => empty_node;
diff -r b96cf915de75 -r 9a2c266f97c8 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Mon Apr 03 12:49:13 2017 +0200
+++ b/src/Pure/PIDE/document.scala	Mon Apr 03 13:39:13 2017 +0200
@@ -98,6 +98,7 @@
     object Name
     {
       val empty = Name("")
+      def theory(theory: String): Name = Name(theory, "", theory)
 
       object Ordering extends scala.math.Ordering[Name]
       {
diff -r b96cf915de75 -r 9a2c266f97c8 src/Pure/PIDE/resources.scala
--- a/src/Pure/PIDE/resources.scala	Mon Apr 03 12:49:13 2017 +0200
+++ b/src/Pure/PIDE/resources.scala	Mon Apr 03 13:39:13 2017 +0200
@@ -77,9 +77,6 @@
     }
     else Nil
 
-  private def dummy_name(theory: String): Document.Node.Name =
-    Document.Node.Name(theory + ".thy", "", theory)
-
   def import_name(qualifier: String, master: Document.Node.Name, s: String): Document.Node.Name =
   {
     val no_qualifier = "" // FIXME
@@ -88,12 +85,12 @@
     (base.known_theories.get(thy1) orElse
      base.known_theories.get(thy2) orElse
      base.known_theories.get(Long_Name.base_name(thy1))) match {
-      case Some(name) if base.loaded_theory(name) => dummy_name(name.theory)
+      case Some(name) if base.loaded_theory(name) => Document.Node.Name.theory(name.theory)
       case Some(name) => name
       case None =>
         val path = Path.explode(s)
         val theory = path.base.implode
-        if (Long_Name.is_qualified(theory)) dummy_name(theory)
+        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)