Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
more markup, which helps to create missing imports;
authorwenzelm
Sun, 15 Mar 2015 22:15:08 +0100
changeset 59708 aed304412e43
parent 59707 10effab11669
child 59711 5b0003211207
more markup, which helps to create missing imports;
src/Pure/PIDE/command.scala file | annotate | diff | comparison | revisions 
--- a/src/Pure/PIDE/command.scala	Sun Mar 15 22:05:08 2015 +0100
+++ b/src/Pure/PIDE/command.scala	Sun Mar 15 22:15:08 2015 +0100
@@ -364,8 +364,10 @@
           resources.check_thy_reader("", node_name,
             new CharSequenceReader(span.source), Token.Pos.id(Markup.COMMAND))
         val import_errors =
-          for ((imp, pos) <- header.imports if !can_import(imp))
-            yield "Bad theory import " + quote(imp.node) + Position.here(pos)
+          for ((imp, pos) <- header.imports if !can_import(imp)) yield {
+            val name = imp.node
+            "Bad theory import " + Markup.Path(name).markup(quote(name)) + Position.here(pos)
+          }
         ((header.errors ::: import_errors).map(msg => Exn.Exn(ERROR(msg)): Command.Blob), -1)
 
       // auxiliary files
isabelle