# HG changeset patch
# User wenzelm
# Date 1507217867 -7200
# Node ID f27488f47a47219b35038d9d87ad6937631d586d
# Parent  294c2e9a689e4036612ceaa442452a4b8d04e853
completion supports theory header imports;
tuned;

diff -r 294c2e9a689e -r f27488f47a47 NEWS
--- a/NEWS	Thu Oct 05 16:33:36 2017 +0200
+++ b/NEWS	Thu Oct 05 17:37:47 2017 +0200
@@ -30,6 +30,11 @@
   isabelle build -D '~~/src/ZF'
 
 
+*** Prover IDE -- Isabelle/Scala/jEdit ***
+
+* Completion supports theory header imports.
+
+
 *** HOL ***
 
 * SMT module:
diff -r 294c2e9a689e -r f27488f47a47 src/Pure/General/completion.scala
--- a/src/Pure/General/completion.scala	Thu Oct 05 16:33:36 2017 +0200
+++ b/src/Pure/General/completion.scala	Thu Oct 05 17:37:47 2017 +0200
@@ -138,11 +138,19 @@
     if (s == "" || s == "_") None
     else Some(s.reverseIterator.dropWhile(_ == '_').toList.reverse.mkString)
 
+  def completed(input: String): String => Boolean =
+    clean_name(input) match {
+      case None => (name: String) => false
+      case Some(prefix) => (name: String) => name.startsWith(prefix)
+    }
+
   def report_no_completion(pos: Position.T): String =
     YXML.string_of_tree(Semantic.Info(pos, No_Completion))
 
   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)))
+    if (names.isEmpty) ""
+    else
+      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)
diff -r 294c2e9a689e -r f27488f47a47 src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Thu Oct 05 16:33:36 2017 +0200
+++ b/src/Pure/PIDE/command.scala	Thu Oct 05 17:37:47 2017 +0200
@@ -438,12 +438,32 @@
       // inlined errors
       case Thy_Header.THEORY =>
         val reader = Scan.char_reader(Token.implode(span.content))
-        val header = resources.check_thy_reader(node_name, reader)
+        val imports = resources.check_thy_reader(node_name, reader).imports
+        val raw_imports =
+          try {
+            val imports1 = Thy_Header.read(reader, Token.Pos.none).imports
+            if (imports.length == imports1.length) imports1.map(_._1) else error("")
+          }
+          catch { case exn: Throwable => List.fill(imports.length)("") }
+
         val errors =
-          for ((imp, pos) <- header.imports if !can_import(imp)) yield {
+          for { ((import_name, pos), s) <- imports zip raw_imports if !can_import(import_name) }
+          yield {
+            val completion =
+              if (Thy_Header.is_base_name(s)) {
+                val completed = Completion.completed(import_name.theory_base_name)
+                val qualifier = resources.theory_qualifier(node_name)
+                val dir = node_name.master_dir
+                for {
+                  (_, known_name) <- resources.session_base.known.theories.toList
+                  if completed(known_name.theory_base_name)
+                } yield resources.standard_import(resources, qualifier, dir, known_name.theory)
+              }.sorted
+              else Nil
             val msg =
               "Bad theory import " +
-                Markup.Path(imp.node).markup(quote(imp.toString)) + Position.here(pos)
+                Markup.Path(import_name.node).markup(quote(import_name.toString)) +
+                Position.here(pos) + Completion.report_theories(pos, completion)
             Exn.Exn(ERROR(msg)): Command.Blob
           }
         (errors, -1)