# HG changeset patch
# User wenzelm
# Date 1661510280 -7200
# Node ID 34dd96a06c45ce7f7a5ef7be4c4d97c1902e7b79
# Parent  2fff9ce6b460c64c62f72c9ea844d24d8c94c061
removed unused "def_theory" markup (stemming from be49c660ebbf), superseded e.g. by Document_Info.theory_by_file();

diff -r 2fff9ce6b460 -r 34dd96a06c45 src/Pure/General/name_space.ML
--- a/src/Pure/General/name_space.ML	Fri Aug 26 12:26:58 2022 +0200
+++ b/src/Pure/General/name_space.ML	Fri Aug 26 12:38:00 2022 +0200
@@ -114,8 +114,7 @@
   serial: serial};
 
 fun entry_markup def kind (name, {pos, theory_long_name, serial, ...}: entry) =
-  Position.make_entity_markup def serial kind (name, pos)
-  ||> not (#def def orelse theory_long_name = "") ? cons (Markup.def_theoryN, theory_long_name);
+  Position.make_entity_markup def serial kind (name, pos);
 
 fun print_entry_ref kind (name, entry) =
   quote (Markup.markup (entry_markup {def = false} kind (name, entry)) name);
diff -r 2fff9ce6b460 -r 34dd96a06c45 src/Pure/General/position.scala
--- a/src/Pure/General/position.scala	Fri Aug 26 12:26:58 2022 +0200
+++ b/src/Pure/General/position.scala	Fri Aug 26 12:38:00 2022 +0200
@@ -25,8 +25,6 @@
   val Def_File = new Properties.String(Markup.DEF_FILE)
   val Def_Id = new Properties.Long(Markup.DEF_ID)
 
-  val Def_Theory = new Properties.String(Markup.DEF_THEORY)
-
   object Line_File {
     def apply(line: Int, file: String): T =
       (if (line > 0) Line(line) else Nil) :::
diff -r 2fff9ce6b460 -r 34dd96a06c45 src/Pure/PIDE/markup.ML
--- a/src/Pure/PIDE/markup.ML	Fri Aug 26 12:26:58 2022 +0200
+++ b/src/Pure/PIDE/markup.ML	Fri Aug 26 12:38:00 2022 +0200
@@ -64,7 +64,6 @@
   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
@@ -427,8 +426,6 @@
     SOME b => b
   | NONE => make_def a);
 
-val def_theoryN = "def_theory";
-
 
 (* expression *)
 
diff -r 2fff9ce6b460 -r 34dd96a06c45 src/Pure/PIDE/markup.scala
--- a/src/Pure/PIDE/markup.scala	Fri Aug 26 12:26:58 2022 +0200
+++ b/src/Pure/PIDE/markup.scala	Fri Aug 26 12:38:00 2022 +0200
@@ -146,8 +146,6 @@
   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)