--- a/src/Pure/General/completion.scala Sun Nov 29 16:45:29 2020 +0100
+++ b/src/Pure/General/completion.scala Sun Nov 29 17:54:50 2020 +0100
@@ -153,7 +153,7 @@
YXML.string_of_tree(Semantic.Info(pos, Names(if (total > 0) total else names.length, names)))
def report_theories(pos: Position.T, thys: List[String], total: Int = 0): String =
- report_names(pos, thys.map(name => (name, ("theory", name))), total)
+ report_names(pos, thys.map(name => (name, (Markup.THEORY, name))), total)
object Semantic
{
--- a/src/Pure/PIDE/markup.scala Sun Nov 29 16:45:29 2020 +0100
+++ b/src/Pure/PIDE/markup.scala Sun Nov 29 17:54:50 2020 +0100
@@ -267,6 +267,7 @@
/* misc entities */
+ val THEORY = "theory"
val CLASS = "class"
val TYPE_NAME = "type_name"
val FIXED = "fixed"