# HG changeset patch
# User wenzelm
# Date 1393845539 -3600
# Node ID 912c9aa8de32278963984aa06a29f35e49b02338
# Parent  213388bf90ffcb27b899918b867d37e443670dd9
tuned messages and markup;

diff -r 213388bf90ff -r 912c9aa8de32 src/Pure/Thy/thy_load.ML
--- a/src/Pure/Thy/thy_load.ML	Mon Mar 03 12:14:47 2014 +0100
+++ b/src/Pure/Thy/thy_load.ML	Mon Mar 03 12:18:59 2014 +0100
@@ -192,14 +192,25 @@
 
 (* document antiquotation *)
 
-fun file_antiq do_check ctxt (name, pos) =
+fun file_antiq strict ctxt (name, pos) =
   let
     val dir = master_directory (Proof_Context.theory_of ctxt);
-    val path = Path.append dir (Path.explode name);
+    val path = Path.append dir (Path.explode name)
+      handle ERROR msg => error (msg ^ Position.here pos);
+
+    val _ = Context_Position.report ctxt pos (Markup.path name);
     val _ =
-      if not do_check orelse File.exists path then ()
-      else error ("Bad file: " ^ Path.print (Path.expand path) ^ Position.here pos);
-    val _ = Context_Position.report ctxt pos (Markup.path name);
+      if can Path.expand path andalso File.exists path then ()
+      else
+        let
+          val path' = perhaps (try Path.expand) path;
+          val msg = "Bad file: " ^ Path.print path' ^ Position.here pos;
+        in
+          if strict then error msg
+          else
+            Context_Position.if_visible ctxt Output.report
+              (Markup.markup (Markup.bad |> Markup.properties (Position.properties_of pos)) msg)
+        end;
   in
     space_explode "/" name
     |> map Thy_Output.verb_text