# HG changeset patch
# User wenzelm
# Date 1525710326 -7200
# Node ID 577072a0ceed347e9d534b18435832446616e721
# Parent  3795f67716e6ddc08fa3bd781d7f85136612d334
more checks;

diff -r 3795f67716e6 -r 577072a0ceed src/Pure/Thy/export.ML
--- a/src/Pure/Thy/export.ML	Mon May 07 17:40:03 2018 +0200
+++ b/src/Pure/Thy/export.ML	Mon May 07 18:25:26 2018 +0200
@@ -13,12 +13,24 @@
 structure Export: EXPORT =
 struct
 
+fun check_name name =
+  let
+    fun err () = error ("Bad export name " ^ quote name);
+    fun check_elem elem =
+      if member (op =) ["", ".", ".."] elem then err ()
+      else ignore (Path.basic elem handle ERROR _ => err ());
+
+    val elems = space_explode "/" name;
+    val _ = null elems andalso err ();
+    val _ = List.app check_elem elems;
+  in name end;
+
 fun gen_export compress thy name 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 = name,
+    name = check_name name,
     compress = compress} body;
 
 fun export thy name body = gen_export (size body > 60) thy name [body];