# HG changeset patch
# User wenzelm
# Date 1507208284 -7200
# Node ID 19f8385ddfd3dcaf8fb74a6e962310bc5902a4d8
# Parent  006deaf5c3dcd9a623eb8434e691099a47fe24ec
tuned signature;

diff -r 006deaf5c3dc -r 19f8385ddfd3 src/Pure/General/completion.scala
--- a/src/Pure/General/completion.scala	Wed Oct 04 20:16:53 2017 +0200
+++ b/src/Pure/General/completion.scala	Thu Oct 05 14:58:04 2017 +0200
@@ -141,8 +141,11 @@
   def report_no_completion(pos: Position.T): String =
     YXML.string_of_tree(Semantic.Info(pos, No_Completion))
 
-  def report_names(pos: Position.T, total: Int, names: List[(String, (String, String))]): String =
-    YXML.string_of_tree(Semantic.Info(pos, Names(total, names)))
+  def report_names(pos: Position.T, names: List[(String, (String, String))], total: Int = 0): String =
+    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)
 
   object Semantic
   {
diff -r 006deaf5c3dc -r 19f8385ddfd3 src/Pure/PIDE/resources.scala
--- a/src/Pure/PIDE/resources.scala	Wed Oct 04 20:16:53 2017 +0200
+++ b/src/Pure/PIDE/resources.scala	Thu Oct 05 14:58:04 2017 +0200
@@ -134,7 +134,7 @@
         if (base_name != name)
           error("Bad theory name " + quote(name) +
             " for file " + thy_path(Path.basic(base_name)) + Position.here(pos) +
-            Completion.report_names(pos, 1, List((base_name, ("theory", base_name)))))
+            Completion.report_theories(pos, List(base_name)))
 
         val imports = header.imports.map({ case (s, pos) => (import_name(node_name, s), pos) })
         Document.Node.Header(imports, header.keywords, header.abbrevs)