tuned signature;
authorwenzelm
Sun, 29 Nov 2020 17:54:50 +0100
changeset 72781 15a8de807f21
parent 72780 6205c5d4fadf
child 72782 98ecb951d911
tuned signature;
src/Pure/General/completion.scala
src/Pure/PIDE/markup.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
   {
--- 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"