diff -r 52ed202464a5 -r 2d61935eed4a src/Doc/antiquote_setup.ML
--- a/src/Doc/antiquote_setup.ML	Wed Nov 06 21:20:20 2013 +0100
+++ b/src/Doc/antiquote_setup.ML	Thu Nov 07 13:34:04 2013 +0100
@@ -47,6 +47,22 @@
     (K (split_lines #> map verbatim #> space_implode "\\isasep\\isanewline%\n"));
 
 
+(* unchecked file *)
+
+val file_unchecked_setup =
+  Thy_Output.antiquotation @{binding file_unchecked} (Scan.lift (Parse.position Parse.path))
+    (fn {context = ctxt, ...} => fn (name, pos) =>
+      let
+        val dir = Thy_Load.master_directory (Proof_Context.theory_of ctxt);
+        val path = Path.append dir (Path.explode name);
+        val _ = Position.report pos (Markup.path name);
+      in
+        space_explode "/" name
+        |> map Thy_Output.verb_text
+        |> space_implode (Thy_Output.verb_text "/" ^ "\\discretionary{}{}{}")
+      end);
+
+
 (* ML text *)
 
 local
@@ -233,6 +249,7 @@
 
 val setup =
   verbatim_setup #>
+  file_unchecked_setup #>
   index_ml_setup #>
   named_thms_setup #>
   thy_file_setup #>