tuned message -- include completion;
authorwenzelm
Mon Mar 16 16:26:02 2015 +0100 (2015-03-16 ago)
changeset 597185d0c539537c9
parent 59717 44a3ed0b8265
child 59719 6410a310fdc2
tuned message -- include completion;
src/Pure/PIDE/resources.ML
src/Pure/PIDE/resources.scala
     1.1 --- a/src/Pure/PIDE/resources.ML	Mon Mar 16 15:33:32 2015 +0100
     1.2 +++ b/src/Pure/PIDE/resources.ML	Mon Mar 16 16:26:02 2015 +0100
     1.3 @@ -68,7 +68,8 @@
     1.4      val {name = (name, pos), imports, keywords} =
     1.5        Thy_Header.read (Path.position master_file) text;
     1.6      val _ = thy_name <> name andalso
     1.7 -      error ("Bad file name " ^ Path.print path ^ " for theory " ^ quote name ^ Position.here pos);
     1.8 +      error ("Bad theory name " ^ quote name ^
     1.9 +        " for file " ^ Path.print path ^ Position.here pos);
    1.10    in
    1.11     {master = (master_file, SHA1.digest text), text = text, theory_pos = pos,
    1.12      imports = imports, keywords = keywords}
     2.1 --- a/src/Pure/PIDE/resources.scala	Mon Mar 16 15:33:32 2015 +0100
     2.2 +++ b/src/Pure/PIDE/resources.scala	Mon Mar 16 16:26:02 2015 +0100
     2.3 @@ -96,8 +96,9 @@
     2.4          val base_name = Long_Name.base_name(node_name.theory)
     2.5          val (name, pos) = header.name
     2.6          if (base_name != name)
     2.7 -          error("Bad file name " + Resources.thy_path(Path.basic(base_name)) +
     2.8 -            " for theory " + quote(name) + Position.here(pos))
     2.9 +          error("Bad theory name " + quote(name) +
    2.10 +            " for file " + Resources.thy_path(Path.basic(base_name)) + Position.here(pos) +
    2.11 +            Completion.report_names(pos, 1, List((base_name, ("theory", base_name)))))
    2.12  
    2.13          val imports =
    2.14            header.imports.map({ case (s, pos) => (import_name(qualifier, node_name, s), pos) })