# HG changeset patch
# User wenzelm
# Date 1426519562 -3600
# Node ID 5d0c539537c9eae10e0a55c3ccbdf51e69f6d302
# Parent  44a3ed0b82653c4daeee3a9cdefcc2cc841353b0
tuned message -- include completion;

diff -r 44a3ed0b8265 -r 5d0c539537c9 src/Pure/PIDE/resources.ML
--- a/src/Pure/PIDE/resources.ML	Mon Mar 16 15:33:32 2015 +0100
+++ b/src/Pure/PIDE/resources.ML	Mon Mar 16 16:26:02 2015 +0100
@@ -68,7 +68,8 @@
     val {name = (name, pos), imports, keywords} =
       Thy_Header.read (Path.position master_file) text;
     val _ = thy_name <> name andalso
-      error ("Bad file name " ^ Path.print path ^ " for theory " ^ quote name ^ Position.here pos);
+      error ("Bad theory name " ^ quote name ^
+        " for file " ^ Path.print path ^ Position.here pos);
   in
    {master = (master_file, SHA1.digest text), text = text, theory_pos = pos,
     imports = imports, keywords = keywords}
diff -r 44a3ed0b8265 -r 5d0c539537c9 src/Pure/PIDE/resources.scala
--- a/src/Pure/PIDE/resources.scala	Mon Mar 16 15:33:32 2015 +0100
+++ b/src/Pure/PIDE/resources.scala	Mon Mar 16 16:26:02 2015 +0100
@@ -96,8 +96,9 @@
         val base_name = Long_Name.base_name(node_name.theory)
         val (name, pos) = header.name
         if (base_name != name)
-          error("Bad file name " + Resources.thy_path(Path.basic(base_name)) +
-            " for theory " + quote(name) + Position.here(pos))
+          error("Bad theory name " + quote(name) +
+            " for file " + Resources.thy_path(Path.basic(base_name)) + Position.here(pos) +
+            Completion.report_names(pos, 1, List((base_name, ("theory", base_name)))))
 
         val imports =
           header.imports.map({ case (s, pos) => (import_name(qualifier, node_name, s), pos) })