clarified signature: Path.T as in Generated_Files;

--- a/src/HOL/SPARK/Tools/spark_vcs.ML	Sat Feb 02 14:51:11 2019 +0100
+++ b/src/HOL/SPARK/Tools/spark_vcs.ML	Sat Feb 02 15:52:14 2019 +0100
@@ -973,7 +973,7 @@
              \because their proofs contain oracles:" proved'));
           val prv_path = Path.ext "prv" path;
           val _ =
-            Export.export thy (Path.implode prv_path)
+            Export.export thy prv_path
               [implode (map (fn (s, _) => snd (strip_number s) ^
                 " -- proved by " ^ Distribution.version ^ "\n") proved'')];
         in {pfuns = pfuns, type_map = type_map, env = NONE} end))

--- a/src/Pure/General/path.ML	Sat Feb 02 14:51:11 2019 +0100
+++ b/src/Pure/General/path.ML	Sat Feb 02 15:52:14 2019 +0100
@@ -7,7 +7,6 @@
 
 signature PATH =
 sig
-  val check_elem: string -> unit
   eqtype T
   val is_current: T -> bool
   val current: T
@@ -20,6 +19,7 @@
   val has_parent: T -> bool
   val is_absolute: T -> bool
   val is_basic: T -> bool
+  val all_basic: T -> bool
   val starts_basic: T -> bool
   val append: T -> T -> T
   val appends: T list -> T
@@ -57,8 +57,6 @@
 val illegal_elem = ["", "~", "~~", ".", ".."];
 val illegal_char = ["/", "\\", "$", ":", "\"", "'", "<", ">", "|", "?", "*"];
 
-in
-
 fun check_elem s =
   if member (op =) illegal_elem s then err_elem "Illegal" s
   else
@@ -69,6 +67,8 @@
         err_elem ("Illegal character " ^ quote c ^ " in") s
       else ());
 
+in
+
 val root_elem = Root o tap check_elem;
 val basic_elem = Basic o tap check_elem;
 val variable_elem = Variable o tap check_elem;
@@ -103,6 +103,9 @@
 fun is_basic (Path [Basic _]) = true
   | is_basic _ = false;
 
+fun all_basic (Path elems) =
+  forall (fn Basic _ => true | _ => false) elems;
+
 fun starts_basic (Path xs) =
   (case try List.last xs of
     SOME (Basic _) => true

--- a/src/Pure/Thy/export.ML	Sat Feb 02 14:51:11 2019 +0100
+++ b/src/Pure/Thy/export.ML	Sat Feb 02 15:52:14 2019 +0100
@@ -6,8 +6,8 @@
 
 signature EXPORT =
 sig
-  val export: theory -> string -> string list -> unit
-  val export_raw: theory -> string -> string list -> unit
+  val export: theory -> Path.T -> string list -> unit
+  val export_raw: theory -> Path.T -> string list -> unit
   val markup: theory -> string -> Markup.T
   val message: theory -> string -> string
 end;
@@ -17,20 +17,20 @@
 
 (* export *)
 
-fun check_name name =
+fun check_name path =
   let
+    val name = Path.implode path;
     val _ =
-      (case space_explode "/" name of
-        [] => error "Empty export name"
-      | elems => List.app Path.check_elem elems);
+      if not (Path.is_current path) andalso Path.all_basic path then ()
+      else error ("Bad export name: " ^ quote name);
   in name end;
 
-fun gen_export compress thy name body =
+fun gen_export compress thy path body =
   (Output.try_protocol_message o Markup.export)
    {id = Position.get_id (Position.thread_data ()),
     serial = serial (),
     theory_name = Context.theory_long_name thy,
-    name = check_name name,
+    name = check_name path,
     compress = compress} body;
 
 val export = gen_export true;

--- a/src/Pure/Thy/export_theory.ML	Sat Feb 02 14:51:11 2019 +0100
+++ b/src/Pure/Thy/export_theory.ML	Sat Feb 02 15:52:14 2019 +0100
@@ -161,7 +161,8 @@
     if Options.bool (#options context) "export_theory" then f context thy else ()));
 
 fun export_body thy name body =
-  Export.export thy ("theory/" ^ name) (Buffer.chunks (YXML.buffer_body body Buffer.empty));
+  Export.export thy (Path.make ["theory", name])
+    (Buffer.chunks (YXML.buffer_body body Buffer.empty));
 
 
 (* presentation *)

--- a/src/Pure/Thy/thy_info.ML	Sat Feb 02 14:51:11 2019 +0100
+++ b/src/Pure/Thy/thy_info.ML	Sat Feb 02 15:52:14 2019 +0100
@@ -66,7 +66,7 @@
             val output = [Latex.output_text latex, Latex.output_positions file_pos latex];
             val _ =
               if Options.bool options "export_document"
-              then Export.export thy "document.tex" output else ();
+              then Export.export thy (Path.explode "document.tex") output else ();
             val _ = if #enabled option then Present.theory_output thy output else ();
           in () end
       end));

--- a/src/Pure/Tools/generated_files.ML	Sat Feb 02 14:51:11 2019 +0100
+++ b/src/Pure/Tools/generated_files.ML	Sat Feb 02 15:52:14 2019 +0100
@@ -81,7 +81,7 @@
 fun export_files thy other_thys =
   other_thys |> maps (fn other_thy =>
     get_files other_thy |> map (fn {path, pos, text} =>
-      (Export.export thy (Path.implode path) [text]; (path, pos))));
+      (Export.export thy path [text]; (path, pos))));
 
 
 (* file types *)

--- a/src/Tools/Code/code_target.ML	Sat Feb 02 14:51:11 2019 +0100
+++ b/src/Tools/Code/code_target.ML	Sat Feb 02 15:52:14 2019 +0100
@@ -180,9 +180,10 @@
   (Export.export thy name [content]; writeln (Export.message thy ""));
 
 fun export_to_exports thy width (Singleton (extension, p)) =
-      export_information thy (generatedN ^ "." ^ extension) (Code_Printer.format [] width p)
+      export_information thy (Path.basic (generatedN ^ "." ^ extension))
+        (Code_Printer.format [] width p)
   | export_to_exports thy width (Hierarchy code_modules) = (
-      map (fn (names, p) => export_information thy (Path.implode (Path.make names))
+      map (fn (names, p) => export_information thy (Path.make names)
         (Code_Printer.format [] width p)) code_modules;
       ());