--- 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];