# 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)