removed unused "def_theory" markup (stemming from be49c660ebbf), superseded e.g. by Document_Info.theory_by_file();
--- 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);
--- 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) :::
--- 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 *)
--- 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)