# HG changeset patch
# User wenzelm
# Date 1636718540 -3600
# Node ID 71a447e4073b290fa9fad2210704d5235a86514a
# Parent  275c43a89887159a39aacc6b2905309aa6d340f5
clarified properties: avoid empty entry;

diff -r 275c43a89887 -r 71a447e4073b src/Pure/General/name_space.ML
--- a/src/Pure/General/name_space.ML	Fri Nov 12 12:51:22 2021 +0100
+++ b/src/Pure/General/name_space.ML	Fri Nov 12 13:02:20 2021 +0100
@@ -115,7 +115,7 @@
 
 fun entry_markup def kind (name, {pos, theory_long_name, serial, ...}: entry) =
   Position.make_entity_markup def serial kind (name, pos)
-  ||> not (#def def) ? cons (Markup.def_theoryN, theory_long_name);
+  ||> not (#def def orelse theory_long_name = "") ? cons (Markup.def_theoryN, theory_long_name);
 
 fun print_entry_ref kind (name, entry) =
   quote (Markup.markup (entry_markup {def = false} kind (name, entry)) name);
diff -r 275c43a89887 -r 71a447e4073b src/Pure/Thy/presentation.scala
--- a/src/Pure/Thy/presentation.scala	Fri Nov 12 12:51:22 2021 +0100
+++ b/src/Pure/Thy/presentation.scala	Fri Nov 12 13:02:20 2021 +0100
@@ -108,10 +108,10 @@
 
     object Entity_Ref
     {
-      def unapply(props: Properties.T): Option[(Path, String, String, String)] =
-        (props, props, props, props, props) match {
-          case (Markup.Ref(_), Position.Def_File(def_file), Position.Def_Theory(def_theory),
-              Markup.Kind(kind), Markup.Name(name)) =>
+      def unapply(props: Properties.T): Option[(Path, Option[String], String, String)] =
+        (props, props, props, props) match {
+          case (Markup.Ref(_), Position.Def_File(def_file), Markup.Kind(kind), Markup.Name(name)) =>
+            val def_theory = Position.Def_Theory.unapply(props)
             Some((Path.explode(def_file), def_theory, kind, name))
           case _ => None
         }
@@ -175,11 +175,9 @@
               node_relative(deps, session, node_name).map(html_dir =>
                 HTML.link(html_dir + html_name(node_name), body))
             case Entity_Ref(file_path, def_theory, kind, name) =>
-              val proper_thy_name =
-                proper_string(def_theory) orElse
-                  (if (File.eq(node.path, file_path)) Some(node.theory) else None)
               for {
-                thy_name <- proper_thy_name
+                thy_name <-
+                  def_theory orElse (if (File.eq(node.path, file_path)) Some(node.theory) else None)
                 node_name = Resources.file_node(file_path, theory = thy_name)
                 html_dir <- node_relative(deps, session, node_name)
                 html_file = node_file(node_name)