# HG changeset patch
# User wenzelm
# Date 1606668890 -3600
# Node ID 15a8de807f21b12fb53356e80cd1a18bad71c0c5
# Parent  6205c5d4fadf5a6b38787e12f77d7396977cc6ec
tuned signature;

diff -r 6205c5d4fadf -r 15a8de807f21 src/Pure/General/completion.scala
--- 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
   {
diff -r 6205c5d4fadf -r 15a8de807f21 src/Pure/PIDE/markup.scala
--- 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"