uniform ML and document antiquotations;

--- a/NEWS	Fri Aug 12 14:02:48 2016 +0200
+++ b/NEWS	Fri Aug 12 14:19:27 2016 +0200
@@ -136,17 +136,15 @@
 before. The theory syntax for 'keywords' has been simplified
 accordingly: optional abbrevs need to go into the new 'abbrevs' section.
 
-
-*** Document preparation ***
-
-* Document antiquotations for file-systems paths are more specific and
-diverse:
-
-  @{path NAME}   -- no check (formerly @{file_unchecked})
-  @{file NAME}   -- plain file (formerly file or directory)
-  @{dir NAME}    -- directory (formerly subsumed by @{file})
-
-Minor INCOMPATIBILITY.
+* ML and document antiquotations for file-systems paths are more uniform
+and diverse:
+
+  @{path NAME}   -- no file-system check
+  @{file NAME}   -- check for plain file
+  @{dir NAME}    -- check for directory
+
+Minor INCOMPATIBILITY, former uses of @{file} and @{file_unchecked} may
+have to be changed.
 
 
 *** Isar ***

--- a/src/Pure/PIDE/resources.ML	Fri Aug 12 14:02:48 2016 +0200
+++ b/src/Pure/PIDE/resources.ML	Fri Aug 12 14:19:27 2016 +0200
@@ -186,23 +186,23 @@
 
 fun err msg pos = error (msg ^ Position.here pos);
 
-fun check_path ctxt dir (name, pos) =
+fun check_path check_file ctxt dir (name, pos) =
   let
     val _ = Context_Position.report ctxt pos Markup.language_path;
 
     val path = Path.append dir (Path.explode name) handle ERROR msg => err msg pos;
     val _ = Path.expand path handle ERROR msg => err msg pos;
     val _ = Context_Position.report ctxt pos (Markup.path (Path.smart_implode path));
-  in path end;
-
-fun path_antiq check_file ctxt (name, pos) =
-  let
-    val dir = master_directory (Proof_Context.theory_of ctxt);
-    val path = check_path ctxt dir (name, pos);
     val _ =
       (case check_file of
         NONE => path
       | SOME check => (check path handle ERROR msg => err msg pos));
+  in path end;
+
+fun document_antiq check_file ctxt (name, pos) =
+  let
+    val dir = master_directory (Proof_Context.theory_of ctxt);
+    val _ = check_path check_file ctxt dir (name, pos);
   in
     space_explode "/" name
     |> map Latex.output_ascii
@@ -210,21 +210,28 @@
     |> enclose "\\isatt{" "}"
   end;
 
+fun ML_antiq check_file ctxt (name, pos) =
+  let val path = check_path check_file ctxt Path.current (name, pos);
+  in "Path.explode " ^ ML_Syntax.print_string (Path.implode path) end;
+
 in
 
 val _ = Theory.setup
  (Thy_Output.antiquotation @{binding path} (Scan.lift (Parse.position Parse.path))
-    (path_antiq NONE o #context) #>
+    (document_antiq NONE o #context) #>
   Thy_Output.antiquotation @{binding file} (Scan.lift (Parse.position Parse.path))
-    (path_antiq (SOME File.check_file) o #context) #>
+    (document_antiq (SOME File.check_file) o #context) #>
   Thy_Output.antiquotation @{binding dir} (Scan.lift (Parse.position Parse.path))
-    (path_antiq (SOME File.check_dir) o #context) #>
+    (document_antiq (SOME File.check_dir) o #context) #>
+  ML_Antiquotation.value @{binding path}
+    (Args.context -- Scan.lift (Parse.position Parse.path)
+      >> uncurry (ML_antiq NONE)) #>
   ML_Antiquotation.value @{binding file}
-    (Args.context -- Scan.lift (Parse.position Parse.path) >> (fn (ctxt, (name, pos)) =>
-      let
-        val path = check_path ctxt Path.current (name, pos);
-        val _ = File.check_file path handle ERROR msg => err msg pos;
-      in "Path.explode " ^ ML_Syntax.print_string (Path.implode path) end)));
+    (Args.context -- Scan.lift (Parse.position Parse.path)
+      >> uncurry (ML_antiq (SOME File.check_file))) #>
+  ML_Antiquotation.value @{binding dir}
+    (Args.context -- Scan.lift (Parse.position Parse.path)
+      >> uncurry (ML_antiq (SOME File.check_dir))));
 
 end;