# HG changeset patch
# User wenzelm
# Date 1541872880 -3600
# Node ID 599b6d0d199b16d573e9d85aba10f05761b8cc88
# Parent  e1d01b351724abcea38497fabf9a2813082497a9
tuned signature;

diff -r e1d01b351724 -r 599b6d0d199b src/Pure/ML/ml_syntax.ML
--- a/src/Pure/ML/ml_syntax.ML	Sat Nov 10 17:12:09 2018 +0100
+++ b/src/Pure/ML/ml_syntax.ML	Sat Nov 10 19:01:20 2018 +0100
@@ -19,6 +19,7 @@
   val print_symbol: Symbol.symbol -> string
   val print_string: string -> string
   val print_strings: string list -> string
+  val print_path: Path.T -> string
   val print_properties: Properties.T -> string
   val print_position: Position.T -> string
   val print_range: Position.range -> string
@@ -86,6 +87,9 @@
 val print_string = quote o implode o map print_symbol o Symbol.explode;
 val print_strings = print_list print_string;
 
+fun print_path path =
+  "Path.explode " ^ print_string (Path.implode path);
+
 val print_properties = print_list (print_pair print_string print_string);
 
 fun print_position pos =
diff -r e1d01b351724 -r 599b6d0d199b src/Pure/PIDE/resources.ML
--- a/src/Pure/PIDE/resources.ML	Sat Nov 10 17:12:09 2018 +0100
+++ b/src/Pure/PIDE/resources.ML	Sat Nov 10 19:01:20 2018 +0100
@@ -259,19 +259,20 @@
 
 local
 
-fun document_antiq check ctxt (name, pos) =
-  let
-    val dir = master_directory (Proof_Context.theory_of ctxt);
-    val _ = check ctxt dir (name, pos);
-    val latex =
-      space_explode "/" name
-      |> map Latex.output_ascii
-      |> space_implode (Latex.output_ascii "/" ^ "\\discretionary{}{}{}");
-  in Latex.enclose_block "\\isatt{" "}" [Latex.string latex] end;
+fun document_antiq check =
+  Args.context -- Scan.lift (Parse.position Parse.path) >> (fn (ctxt, (name, pos)) =>
+    let
+      val dir = master_directory (Proof_Context.theory_of ctxt);
+      val _: Path.T = check ctxt dir (name, pos);
+      val latex =
+        space_explode "/" name
+        |> map Latex.output_ascii
+        |> space_implode (Latex.output_ascii "/" ^ "\\discretionary{}{}{}");
+    in Latex.enclose_block "\\isatt{" "}" [Latex.string latex] end);
 
-fun ML_antiq check ctxt (name, pos) =
-  let val path = check ctxt Path.current (name, pos);
-  in "Path.explode " ^ ML_Syntax.print_string (Path.implode path) end;
+fun ML_antiq check =
+  Args.context -- Scan.lift (Parse.position Parse.path) >> (fn (ctxt, (name, pos)) =>
+    check ctxt Path.current (name, pos) |> ML_Syntax.print_path);
 
 in
 
@@ -280,18 +281,12 @@
     (Scan.lift (Parse.position Parse.embedded)) check_session #>
   Thy_Output.antiquotation_verbatim \<^binding>\<open>doc\<close>
     (Scan.lift (Parse.position Parse.embedded)) check_doc #>
-  Thy_Output.antiquotation_raw \<^binding>\<open>path\<close>
-    (Scan.lift (Parse.position Parse.path)) (document_antiq check_path) #>
-  Thy_Output.antiquotation_raw \<^binding>\<open>file\<close>
-    (Scan.lift (Parse.position Parse.path)) (document_antiq check_file) #>
-  Thy_Output.antiquotation_raw \<^binding>\<open>dir\<close>
-    (Scan.lift (Parse.position Parse.path)) (document_antiq check_dir) #>
-  ML_Antiquotation.value \<^binding>\<open>path\<close>
-    (Args.context -- Scan.lift (Parse.position Parse.path) >> uncurry (ML_antiq check_path)) #>
-  ML_Antiquotation.value \<^binding>\<open>file\<close>
-    (Args.context -- Scan.lift (Parse.position Parse.path) >> uncurry (ML_antiq check_file)) #>
-  ML_Antiquotation.value \<^binding>\<open>dir\<close>
-    (Args.context -- Scan.lift (Parse.position Parse.path) >> uncurry (ML_antiq check_dir)));
+  Thy_Output.antiquotation_raw \<^binding>\<open>path\<close> (document_antiq check_path) (K I) #>
+  Thy_Output.antiquotation_raw \<^binding>\<open>file\<close> (document_antiq check_file) (K I) #>
+  Thy_Output.antiquotation_raw \<^binding>\<open>dir\<close> (document_antiq check_dir) (K I) #>
+  ML_Antiquotation.value \<^binding>\<open>path\<close> (ML_antiq check_path) #>
+  ML_Antiquotation.value \<^binding>\<open>file\<close> (ML_antiq check_file) #>
+  ML_Antiquotation.value \<^binding>\<open>dir\<close> (ML_antiq check_dir));
 
 end;