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