# HG changeset patch
# User wenzelm
# Date 1504262843 -7200
# Node ID e5e56c3309769cda7173262bc365824f65b448b7
# Parent  75c090d0e699003936340ca88adaa8c1d4f38db8
more PIDE markup;

diff -r 75c090d0e699 -r e5e56c330976 src/Tools/Code/code_target.ML
--- a/src/Tools/Code/code_target.ML	Fri Sep 01 12:19:40 2017 +0200
+++ b/src/Tools/Code/code_target.ML	Fri Sep 01 12:47:23 2017 +0200
@@ -436,8 +436,14 @@
 
 (* code generation *)
 
-fun prep_destination "" = NONE
-  | prep_destination s = SOME (Path.explode s);
+fun prep_destination (s, pos) =
+  if s = "" then NONE
+  else
+    let
+      val _ = Position.report pos Markup.language_path;
+      val path = Path.explode s;
+      val _ = Position.report pos (Markup.path (Path.smart_implode path));
+    in SOME path end;
 
 fun export_code ctxt all_public cs seris =
   let
@@ -630,7 +636,7 @@
 fun code_expr_inP all_public raw_cs =
   Scan.repeat (@{keyword "in"} |-- Parse.!!! (Parse.name
     -- Scan.optional (@{keyword "module_name"} |-- Parse.name) ""
-    -- Scan.optional (@{keyword "file"} |-- Parse.name) ""
+    -- Scan.optional (@{keyword "file"} |-- Parse.position Parse.path) ("", Position.none)
     -- code_expr_argsP))
       >> (fn seri_args => export_code_cmd all_public raw_cs seri_args);