added document antiquotation @{file};

--- a/NEWS	Sun Nov 28 21:07:28 2010 +0100
+++ b/NEWS	Mon Nov 29 11:22:40 2010 +0100
@@ -83,8 +83,11 @@
 * Discontinued ancient 'constdefs' command.  INCOMPATIBILITY, use
 'definition' instead.
 
-* Document antiquotations @{class} and @{type} for printing classes
-and type constructors.
+* Document antiquotations @{class} and @{type} print classes and type
+constructors.
+
+* Document antiquotation @{file} checks file/directory entries within
+the local file system.
 
 
 *** HOL ***

--- a/doc-src/IsarRef/Thy/Document_Preparation.thy	Sun Nov 28 21:07:28 2010 +0100
+++ b/doc-src/IsarRef/Thy/Document_Preparation.thy	Mon Nov 29 11:22:40 2010 +0100
@@ -156,6 +156,7 @@
     @{antiquotation_def ML} & : & @{text antiquotation} \\
     @{antiquotation_def ML_type} & : & @{text antiquotation} \\
     @{antiquotation_def ML_struct} & : & @{text antiquotation} \\
+    @{antiquotation_def "file"} & : & @{text antiquotation} \\
   \end{matharray}
 
   The overall content of an Isabelle/Isar theory may alternate between
@@ -201,7 +202,8 @@
       'full_prf' options thmrefs |
       'ML' options name |
       'ML_type' options name |
-      'ML_struct' options name
+      'ML_struct' options name |
+      'file' options name
     ;
     options: '[' (option * ',') ']'
     ;
@@ -287,6 +289,9 @@
   "@{ML_struct s}"} check text @{text s} as ML value, type, and
   structure, respectively.  The source is printed verbatim.
 
+  \item @{text "@{file path}"} checks that @{text "path"} refers to a
+  file (or directory) and prints it verbatim.
+
   \end{description}
 *}
 

--- a/doc-src/antiquote_setup.ML	Sun Nov 28 21:07:28 2010 +0100
+++ b/doc-src/antiquote_setup.ML	Mon Nov 29 11:22:40 2010 +0100
@@ -4,7 +4,7 @@
 Auxiliary antiquotations for the Isabelle manuals.
 *)
 
-structure AntiquoteSetup: sig end =
+structure Antiquote_Setup: sig end =
 struct
 
 (* misc utils *)
@@ -190,7 +190,6 @@
 val _ = entity_antiqs no_check "" "inference";
 val _ = entity_antiqs no_check "isatt" "executable";
 val _ = entity_antiqs (K check_tool) "isatt" "tool";
-val _ = entity_antiqs (K (File.exists o Path.explode)) "isatt" "file";
 val _ = entity_antiqs (K (can Thy_Info.get_theory)) "" "theory";
 val _ = entity_antiqs no_check "" "ML antiquotation";  (* FIXME proper check *)
 

--- a/src/Pure/Thy/thy_output.ML	Sun Nov 28 21:07:28 2010 +0100
+++ b/src/Pure/Thy/thy_output.ML	Mon Nov 29 11:22:40 2010 +0100
@@ -575,7 +575,6 @@
 val _ = basic_entities "prf" Attrib.thms (pretty_prf false);
 val _ = basic_entities "full_prf" Attrib.thms (pretty_prf true);
 val _ = basic_entity "theory" (Scan.lift Args.name) pretty_theory;
-
 val _ = basic_entities_style "thm_style" (Term_Style.parse_bare -- Attrib.thms) pretty_thm_style;
 val _ = basic_entity "term_style" (Term_Style.parse_bare -- Args.term) pretty_term_style;
 
@@ -622,6 +621,11 @@
 
 (* ML text *)
 
+val verb_text =
+  split_lines
+  #> map (space_implode "\\verb,|," o map (enclose "\\verb|" "|") o space_explode "|")
+  #> space_implode "\\isasep\\isanewline%\n";
+
 local
 
 fun ml_text name ml = antiquotation name (Scan.lift Args.name_source_position)
@@ -630,10 +634,7 @@
     Symbol_Pos.content (Symbol_Pos.explode (txt, pos))
     |> (if Config.get context quotes then quote else I)
     |> (if Config.get context display then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}"
-    else
-      split_lines
-      #> map (space_implode "\\verb,|," o map (enclose "\\verb|" "|") o space_explode "|")
-      #> space_implode "\\isasep\\isanewline%\n")));
+        else verb_text)));
 
 fun ml_enclose bg en pos txt =
   ML_Lex.read Position.none bg @ ML_Lex.read pos txt @ ML_Lex.read Position.none en;
@@ -653,4 +654,12 @@
 
 end;
 
+
+(* files *)
+
+val _ = antiquotation "file" (Scan.lift Args.name)
+  (fn {context, ...} => fn path =>
+    if File.exists (Path.explode path) then verb_text path
+    else error ("Bad file: " ^ quote path));
+
 end;