# HG changeset patch
# User wenzelm
# Date 1347275996 -7200
# Node ID fb669aff821e74e3f7a5fa6ec1bd97105c3111ab
# Parent  ded41f584938400692c876b9976f6bc2e0495097
formal markup for @{file} (for hyperlinks etc.) -- interpret path wrt. master directory as usual;

diff -r ded41f584938 -r fb669aff821e src/Pure/Thy/thy_load.ML
--- a/src/Pure/Thy/thy_load.ML	Mon Sep 10 12:13:39 2012 +0200
+++ b/src/Pure/Thy/thy_load.ML	Mon Sep 10 13:19:56 2012 +0200
@@ -273,6 +273,22 @@
   in (thy, present) end;
 
 
+(* document antiquotation *)
+
+val _ =
+  Context.>> (Context.map_theory
+   (Thy_Output.antiquotation (Binding.name "file") (Scan.lift (Parse.position Parse.path))
+    (fn {context = ctxt, ...} => fn (name, pos) =>
+      let
+        val dir = master_directory (Proof_Context.theory_of ctxt);
+        val path = Path.append dir (Path.explode name);
+        val _ =
+          if File.exists path then ()
+          else error ("Bad file: " ^ Path.print (Path.expand path) ^ Position.here pos);
+        val _ = Position.report pos (Isabelle_Markup.path name);
+      in Thy_Output.verb_text name end)));
+
+
 (* global master path *)
 
 local
diff -r ded41f584938 -r fb669aff821e src/Pure/Thy/thy_output.ML
--- a/src/Pure/Thy/thy_output.ML	Mon Sep 10 12:13:39 2012 +0200
+++ b/src/Pure/Thy/thy_output.ML	Mon Sep 10 13:19:56 2012 +0200
@@ -42,6 +42,7 @@
   val maybe_pretty_source: (Proof.context -> 'a -> Pretty.T) -> Proof.context ->
     Args.src -> 'a list -> Pretty.T list
   val output: Proof.context -> Pretty.T list -> string
+  val verb_text: string -> string
 end;
 
 structure Thy_Output: THY_OUTPUT =
@@ -685,14 +686,4 @@
 
 end;
 
-
-(* files *)
-
-val _ =
-  Context.>> (Context.map_theory
-   (antiquotation (Binding.name "file") (Scan.lift Args.name)
-    (fn _ => fn path =>
-      if File.exists (Path.explode path) then verb_text path
-      else error ("Bad file: " ^ quote path))));
-
 end;