# 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) })