# HG changeset patch
# User wenzelm
# Date 1660745230 -7200
# Node ID a63ccf1a583ea2d8f347ca6dd26c16648516bf16
# Parent  a1336e2d768074229c30f62a7e8e27c5ea91f5e3
clarified modules;

diff -r a1336e2d7680 -r a63ccf1a583e src/Pure/Thy/presentation.scala
--- a/src/Pure/Thy/presentation.scala	Wed Aug 17 16:03:36 2022 +0200
+++ b/src/Pure/Thy/presentation.scala	Wed Aug 17 16:07:10 2022 +0200
@@ -192,27 +192,27 @@
 
   /* formal entities */
 
-  object Entity_Context {
-    object Theory_Ref {
-      def unapply(props: Properties.T): Option[Document.Node.Name] =
-        (props, props, props) match {
-          case (Markup.Kind(Markup.THEORY), Markup.Name(theory), Position.Def_File(thy_file)) =>
-            Some(Resources.file_node(Path.explode(thy_file), theory = theory))
-          case _ => None
-        }
-    }
+  object Theory_Ref {
+    def unapply(props: Properties.T): Option[Document.Node.Name] =
+      (props, props, props) match {
+        case (Markup.Kind(Markup.THEORY), Markup.Name(theory), Position.Def_File(thy_file)) =>
+          Some(Resources.file_node(Path.explode(thy_file), theory = theory))
+        case _ => None
+      }
+  }
 
-    object Entity_Ref {
-      def unapply(props: Properties.T): Option[(Path, Option[String], String, String)] =
-        (props, props, props, props) match {
-          case (Markup.Entity.Ref.Prop(_), 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
-        }
-    }
+  object Entity_Ref {
+    def unapply(props: Properties.T): Option[(Path, Option[String], String, String)] =
+      (props, props, props, props) match {
+        case (Markup.Entity.Ref.Prop(_), 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
+      }
+  }
 
+  object Entity_Context {
     val empty: Entity_Context = new Entity_Context
 
     def make(