# HG changeset patch
# User wenzelm
# Date 1394706845 -3600
# Node ID efa24d31e59537dc9e444342720001ff5ae4db51
# Parent  4a7a07c018570db3e2d760c49d1a6ff650213650
added ML antiquotation @{path};

diff -r 4a7a07c01857 -r efa24d31e595 NEWS
--- a/NEWS	Thu Mar 13 10:34:48 2014 +0100
+++ b/NEWS	Thu Mar 13 11:34:05 2014 +0100
@@ -445,6 +445,12 @@
 * ML antiquotation @{here} refers to its source position, which is
 occasionally useful for experimentation and diagnostic purposes.
 
+* ML antiquotation @{path} produces a Path.T value, similarly to
+Path.explode, but with compile-time check against the file-system and
+some PIDE markup.  Note that unlike theory source, ML does not have a
+well-defined master directory, so an absolute symbolic path
+specification is usually required, e.g. "~~/src/HOL".
+
 
 *** System ***
 
diff -r 4a7a07c01857 -r efa24d31e595 src/Doc/antiquote_setup.ML
--- a/src/Doc/antiquote_setup.ML	Thu Mar 13 10:34:48 2014 +0100
+++ b/src/Doc/antiquote_setup.ML	Thu Mar 13 11:34:05 2014 +0100
@@ -166,12 +166,12 @@
   | parse_named _ _ = [];
 
 val jedit_actions =
-  (case XML.parse (File.read (Path.explode "~~/src/Tools/jEdit/src/actions.xml")) of
+  (case XML.parse (File.read @{path "~~/src/Tools/jEdit/src/actions.xml"}) of
     XML.Elem (("ACTIONS", _), body) => maps (parse_named "ACTION") body
   | _ => []);
 
 val jedit_dockables =
-  (case XML.parse (File.read (Path.explode "~~/src/Tools/jEdit/src/dockables.xml")) of
+  (case XML.parse (File.read @{path "~~/src/Tools/jEdit/src/dockables.xml"}) of
     XML.Elem (("DOCKABLES", _), body) => maps (parse_named "DOCKABLE") body
   | _ => []);
 
diff -r 4a7a07c01857 -r efa24d31e595 src/HOL/Tools/Quickcheck/narrowing_generators.ML
--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Thu Mar 13 10:34:48 2014 +0100
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Thu Mar 13 11:34:05 2014 +0100
@@ -200,10 +200,10 @@
 (** invocation of Haskell interpreter **)
 
 val narrowing_engine =
-  File.read (Path.explode "~~/src/HOL/Tools/Quickcheck/Narrowing_Engine.hs")
+  File.read @{path "~~/src/HOL/Tools/Quickcheck/Narrowing_Engine.hs"}
 
 val pnf_narrowing_engine =
-  File.read (Path.explode "~~/src/HOL/Tools/Quickcheck/PNF_Narrowing_Engine.hs")
+  File.read @{path "~~/src/HOL/Tools/Quickcheck/PNF_Narrowing_Engine.hs"}
 
 fun exec verbose code =
   ML_Context.exec (fn () => Secure.use_text ML_Env.local_context (0, "generated code") verbose code)
diff -r 4a7a07c01857 -r efa24d31e595 src/Pure/Thy/thy_load.ML
--- a/src/Pure/Thy/thy_load.ML	Thu Mar 13 10:34:48 2014 +0100
+++ b/src/Pure/Thy/thy_load.ML	Thu Mar 13 11:34:05 2014 +0100
@@ -190,13 +190,14 @@
   in (thy, present, size text) end;
 
 
-(* document antiquotation *)
+(* antiquotations *)
 
-fun file_antiq strict ctxt (name, pos) =
+local
+
+fun check_path strict ctxt dir (name, pos) =
   let
     val _ = Context_Position.report ctxt pos Markup.language_path;
 
-    val dir = master_directory (Proof_Context.theory_of ctxt);
     val path = Path.append dir (Path.explode name)
       handle ERROR msg => error (msg ^ Position.here pos);
 
@@ -213,16 +214,30 @@
             Context_Position.if_visible ctxt Output.report
               (Markup.markup (Markup.bad |> Markup.properties (Position.properties_of pos)) msg)
         end;
+  in path end;
+
+fun file_antiq strict ctxt (name, pos) =
+  let
+    val dir = master_directory (Proof_Context.theory_of ctxt);
+    val _ = check_path strict ctxt dir (name, pos);
   in
     space_explode "/" name
     |> map Thy_Output.verb_text
     |> space_implode (Thy_Output.verb_text "/" ^ "\\discretionary{}{}{}")
   end;
 
+in
+
 val _ = Theory.setup
-  (Thy_Output.antiquotation (Binding.name "file") (Scan.lift (Parse.position Parse.path))
+ (Thy_Output.antiquotation (Binding.name "file") (Scan.lift (Parse.position Parse.path))
     (file_antiq true o #context) #>
-  (Thy_Output.antiquotation (Binding.name "file_unchecked") (Scan.lift (Parse.position Parse.path))
-    (file_antiq false o #context)));
+  Thy_Output.antiquotation (Binding.name "file_unchecked") (Scan.lift (Parse.position Parse.path))
+    (file_antiq false o #context) #>
+  ML_Antiquotation.value (Binding.name "path")
+    (Args.context -- Scan.lift (Parse.position Parse.path) >> (fn (ctxt, arg) =>
+      let val path = check_path true ctxt Path.current arg
+      in "Path.explode " ^ ML_Syntax.print_string (Path.implode path) end)));
 
 end;
+
+end;
diff -r 4a7a07c01857 -r efa24d31e595 src/Tools/WWW_Find/unicode_symbols.ML
--- a/src/Tools/WWW_Find/unicode_symbols.ML	Thu Mar 13 10:34:48 2014 +0100
+++ b/src/Tools/WWW_Find/unicode_symbols.ML	Thu Mar 13 11:34:05 2014 +0100
@@ -177,7 +177,7 @@
 
 local
 val (fromsym, fromabbr, tosym, toabbr) =
-  read_symbols (Path.explode "~~/src/Tools/WWW_Find/etc/symbols");
+  read_symbols @{path "~~/src/Tools/WWW_Find/etc/symbols"};
 in
 val symbol_to_unicode = Symtab.lookup fromsym;
 val abbrev_to_unicode = Symtab.lookup fromabbr;