1.1 --- a/NEWS	Sun Nov 28 21:07:28 2010 +0100
     1.2 +++ b/NEWS	Mon Nov 29 11:22:40 2010 +0100
     1.3 @@ -83,8 +83,11 @@
     1.4  * Discontinued ancient 'constdefs' command.  INCOMPATIBILITY, use
     1.5  'definition' instead.
     1.6  
     1.7 -* Document antiquotations @{class} and @{type} for printing classes
     1.8 -and type constructors.
     1.9 +* Document antiquotations @{class} and @{type} print classes and type
    1.10 +constructors.
    1.11 +
    1.12 +* Document antiquotation @{file} checks file/directory entries within
    1.13 +the local file system.
    1.14  
    1.15  
    1.16  *** HOL ***

     2.1 --- a/doc-src/IsarRef/Thy/Document_Preparation.thy	Sun Nov 28 21:07:28 2010 +0100
     2.2 +++ b/doc-src/IsarRef/Thy/Document_Preparation.thy	Mon Nov 29 11:22:40 2010 +0100
     2.3 @@ -156,6 +156,7 @@
     2.4      @{antiquotation_def ML} & : & @{text antiquotation} \\
     2.5      @{antiquotation_def ML_type} & : & @{text antiquotation} \\
     2.6      @{antiquotation_def ML_struct} & : & @{text antiquotation} \\
     2.7 +    @{antiquotation_def "file"} & : & @{text antiquotation} \\
     2.8    \end{matharray}
     2.9  
    2.10    The overall content of an Isabelle/Isar theory may alternate between
    2.11 @@ -201,7 +202,8 @@
    2.12        'full_prf' options thmrefs |
    2.13        'ML' options name |
    2.14        'ML_type' options name |
    2.15 -      'ML_struct' options name
    2.16 +      'ML_struct' options name |
    2.17 +      'file' options name
    2.18      ;
    2.19      options: '[' (option * ',') ']'
    2.20      ;
    2.21 @@ -287,6 +289,9 @@
    2.22    "@{ML_struct s}"} check text @{text s} as ML value, type, and
    2.23    structure, respectively.  The source is printed verbatim.
    2.24  
    2.25 +  \item @{text "@{file path}"} checks that @{text "path"} refers to a
    2.26 +  file (or directory) and prints it verbatim.
    2.27 +
    2.28    \end{description}
    2.29  *}
    2.30  

     3.1 --- a/doc-src/antiquote_setup.ML	Sun Nov 28 21:07:28 2010 +0100
     3.2 +++ b/doc-src/antiquote_setup.ML	Mon Nov 29 11:22:40 2010 +0100
     3.3 @@ -4,7 +4,7 @@
     3.4  Auxiliary antiquotations for the Isabelle manuals.
     3.5  *)
     3.6  
     3.7 -structure AntiquoteSetup: sig end =
     3.8 +structure Antiquote_Setup: sig end =
     3.9  struct
    3.10  
    3.11  (* misc utils *)
    3.12 @@ -190,7 +190,6 @@
    3.13  val _ = entity_antiqs no_check "" "inference";
    3.14  val _ = entity_antiqs no_check "isatt" "executable";
    3.15  val _ = entity_antiqs (K check_tool) "isatt" "tool";
    3.16 -val _ = entity_antiqs (K (File.exists o Path.explode)) "isatt" "file";
    3.17  val _ = entity_antiqs (K (can Thy_Info.get_theory)) "" "theory";
    3.18  val _ = entity_antiqs no_check "" "ML antiquotation";  (* FIXME proper check *)
    3.19  

     4.1 --- a/src/Pure/Thy/thy_output.ML	Sun Nov 28 21:07:28 2010 +0100
     4.2 +++ b/src/Pure/Thy/thy_output.ML	Mon Nov 29 11:22:40 2010 +0100
     4.3 @@ -575,7 +575,6 @@
     4.4  val _ = basic_entities "prf" Attrib.thms (pretty_prf false);
     4.5  val _ = basic_entities "full_prf" Attrib.thms (pretty_prf true);
     4.6  val _ = basic_entity "theory" (Scan.lift Args.name) pretty_theory;
     4.7 -
     4.8  val _ = basic_entities_style "thm_style" (Term_Style.parse_bare -- Attrib.thms) pretty_thm_style;
     4.9  val _ = basic_entity "term_style" (Term_Style.parse_bare -- Args.term) pretty_term_style;
    4.10  
    4.11 @@ -622,6 +621,11 @@
    4.12  
    4.13  (* ML text *)
    4.14  
    4.15 +val verb_text =
    4.16 +  split_lines
    4.17 +  #> map (space_implode "\\verb,|," o map (enclose "\\verb|" "|") o space_explode "|")
    4.18 +  #> space_implode "\\isasep\\isanewline%\n";
    4.19 +
    4.20  local
    4.21  
    4.22  fun ml_text name ml = antiquotation name (Scan.lift Args.name_source_position)
    4.23 @@ -630,10 +634,7 @@
    4.24      Symbol_Pos.content (Symbol_Pos.explode (txt, pos))
    4.25      |> (if Config.get context quotes then quote else I)
    4.26      |> (if Config.get context display then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}"
    4.27 -    else
    4.28 -      split_lines
    4.29 -      #> map (space_implode "\\verb,|," o map (enclose "\\verb|" "|") o space_explode "|")
    4.30 -      #> space_implode "\\isasep\\isanewline%\n")));
    4.31 +        else verb_text)));
    4.32  
    4.33  fun ml_enclose bg en pos txt =
    4.34    ML_Lex.read Position.none bg @ ML_Lex.read pos txt @ ML_Lex.read Position.none en;
    4.35 @@ -653,4 +654,12 @@
    4.36  
    4.37  end;
    4.38  
    4.39 +
    4.40 +(* files *)
    4.41 +
    4.42 +val _ = antiquotation "file" (Scan.lift Args.name)
    4.43 +  (fn {context, ...} => fn path =>
    4.44 +    if File.exists (Path.explode path) then verb_text path
    4.45 +    else error ("Bad file: " ^ quote path));
    4.46 +
    4.47  end;