more markup, e.g. to locate defining theory node in formal document output;

--- a/src/Pure/General/name_space.ML	Tue Sep 07 21:47:50 2021 +0200
+++ b/src/Pure/General/name_space.ML	Tue Sep 07 22:35:44 2021 +0200
@@ -113,8 +113,9 @@
   pos: Position.T,
   serial: serial};
 
-fun entry_markup def kind (name, {pos, serial, ...}: entry) =
-  Position.make_entity_markup def serial kind (name, pos);
+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);
 
 fun print_entry_ref kind (name, entry) =
   quote (Markup.markup (entry_markup {def = false} kind (name, entry)) name);

--- a/src/Pure/General/position.scala	Tue Sep 07 21:47:50 2021 +0200
+++ b/src/Pure/General/position.scala	Tue Sep 07 22:35:44 2021 +0200
@@ -29,6 +29,8 @@
   val Def_File = new Properties.String(Markup.DEF_FILE)
   val Def_Id = new Properties.Long(Markup.DEF_ID)
 
+  val Def_Theory = new Properties.Long(Markup.DEF_THEORY)
+
   object Line_File
   {
     def apply(line: Int, file: String): T =

--- a/src/Pure/PIDE/markup.ML	Tue Sep 07 21:47:50 2021 +0200
+++ b/src/Pure/PIDE/markup.ML	Tue Sep 07 22:35:44 2021 +0200
@@ -64,6 +64,7 @@
   val position_properties: string list
   val position_property: Properties.entry -> bool
   val def_name: string -> string
+  val def_theoryN: string
   val expressionN: string val expression: string -> T
   val citationN: string val citation: string -> T
   val pathN: string val path: string -> T
@@ -413,6 +414,8 @@
     SOME b => b
   | NONE => make_def a);
 
+val def_theoryN = "def_theory";
+
 
 (* expression *)
 

--- a/src/Pure/PIDE/markup.scala	Tue Sep 07 21:47:50 2021 +0200
+++ b/src/Pure/PIDE/markup.scala	Tue Sep 07 22:35:44 2021 +0200
@@ -159,6 +159,8 @@
   val DEF_FILE = "def_file"
   val DEF_ID = "def_id"
 
+  val DEF_THEORY = "def_theory"
+
   val POSITION = "position"
 
   val POSITION_PROPERTIES = Set(LINE, OFFSET, END_OFFSET, FILE, ID)