# HG changeset patch
# User wenzelm
# Date 1426454108 -3600
# Node ID aed304412e43149779bd29d891300804083d776e
# Parent  10effab1166988a9b260abc2d8b4a1602e8f2785
more markup, which helps to create missing imports;

diff -r 10effab11669 -r aed304412e43 src/Pure/PIDE/command.scala
--- 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