tuned signature;
authorwenzelm
Thu Oct 05 14:58:04 2017 +0200 (20 months ago)
changeset 6676619f8385ddfd3
parent 66764 006deaf5c3dc
child 66767 294c2e9a689e
tuned signature;
src/Pure/General/completion.scala
src/Pure/PIDE/resources.scala
     1.1 --- a/src/Pure/General/completion.scala	Wed Oct 04 20:16:53 2017 +0200
     1.2 +++ b/src/Pure/General/completion.scala	Thu Oct 05 14:58:04 2017 +0200
     1.3 @@ -141,8 +141,11 @@
     1.4    def report_no_completion(pos: Position.T): String =
     1.5      YXML.string_of_tree(Semantic.Info(pos, No_Completion))
     1.6  
     1.7 -  def report_names(pos: Position.T, total: Int, names: List[(String, (String, String))]): String =
     1.8 -    YXML.string_of_tree(Semantic.Info(pos, Names(total, names)))
     1.9 +  def report_names(pos: Position.T, names: List[(String, (String, String))], total: Int = 0): String =
    1.10 +    YXML.string_of_tree(Semantic.Info(pos, Names(if (total > 0) total else names.length, names)))
    1.11 +
    1.12 +  def report_theories(pos: Position.T, thys: List[String], total: Int = 0): String =
    1.13 +    report_names(pos, thys.map(name => (name, ("theory", name))), total)
    1.14  
    1.15    object Semantic
    1.16    {
     2.1 --- a/src/Pure/PIDE/resources.scala	Wed Oct 04 20:16:53 2017 +0200
     2.2 +++ b/src/Pure/PIDE/resources.scala	Thu Oct 05 14:58:04 2017 +0200
     2.3 @@ -134,7 +134,7 @@
     2.4          if (base_name != name)
     2.5            error("Bad theory name " + quote(name) +
     2.6              " for file " + thy_path(Path.basic(base_name)) + Position.here(pos) +
     2.7 -            Completion.report_names(pos, 1, List((base_name, ("theory", base_name)))))
     2.8 +            Completion.report_theories(pos, List(base_name)))
     2.9  
    2.10          val imports = header.imports.map({ case (s, pos) => (import_name(node_name, s), pos) })
    2.11          Document.Node.Header(imports, header.keywords, header.abbrevs)