src/Pure/Tools/generated_files.ML

--- a/src/Pure/Tools/generated_files.ML	Sat Mar 30 12:07:31 2019 +0100
+++ b/src/Pure/Tools/generated_files.ML	Sat Mar 30 20:54:47 2019 +0100
@@ -6,7 +6,7 @@
 
 signature GENERATED_FILES =
 sig
-  val add_files: (Path.T * Position.T) * string -> theory -> theory
+  val add_files: Path.binding * string -> theory -> theory
   val get_files: theory -> {path: Path.T, pos: Position.T, content: string} list
   val write_files: theory -> Path.T -> (Path.T * Position.T) list
   val export_files: theory -> theory list -> (Path.T * Position.T) list
@@ -53,18 +53,12 @@
 
 (* files *)
 
-fun add_files ((path0, pos), content) =
-  let
-    val path = Path.expand path0;
-    fun err msg ps = error (msg ^ ": " ^ Path.print path ^ Position.here_list ps);
-    val _ =
-      if Path.is_absolute path then err "Illegal absolute path" [pos]
-      else if Path.has_parent path then err "Illegal parent path" [pos]
-      else ();
-  in
+fun add_files (binding, content) =
+  let val (path, pos) = Path.dest_binding binding in
     (Data.map o @{apply 3(1)}) (fn files =>
       (case AList.lookup (op =) files path of
-        SOME (pos', _) => err "Duplicate generated file" [pos, pos']
+        SOME (pos', _) =>
+          error ("Duplicate generated file: " ^ Path.print path ^ Position.here_list [pos, pos'])
       | NONE => (path, (pos, content)) :: files))
   end;
 
@@ -83,7 +77,7 @@
 fun export_files thy other_thys =
   other_thys |> maps (fn other_thy =>
     get_files other_thy |> map (fn {path, pos, content} =>
-      (Export.export thy path [content]; (path, pos))));
+      (Export.export thy (Path.binding (path, pos)) [content]; (path, pos))));
 
 fun the_file_content thy path =
   (case find_first (fn file => #path file = path) (get_files thy) of
@@ -175,13 +169,14 @@
     val thy = Proof_Context.theory_of lthy;
 
     val path = Path.explode file;
+    val binding = Path.binding (path, pos);
     val file_type =
       the_file_type thy (#2 (Path.split_ext path))
         handle ERROR msg => error (msg ^ Position.here pos);
 
     val header = #make_comment file_type " generated by Isabelle ";
     val content = header ^ "\n" ^ read_source lthy file_type source;
-  in lthy |> (Local_Theory.background_theory o add_files) ((path, pos), content) end;
+  in lthy |> (Local_Theory.background_theory o add_files) (binding, content) end;