equal
deleted
inserted
replaced
13 structure Export: EXPORT = |
13 structure Export: EXPORT = |
14 struct |
14 struct |
15 |
15 |
16 fun check_name name = |
16 fun check_name name = |
17 let |
17 let |
18 fun err () = error ("Bad export name " ^ quote name); |
18 val _ = |
19 fun check_elem elem = |
19 (case space_explode "/" name of |
20 if member (op =) ["", ".", ".."] elem then err () |
20 [] => error "Empty export name" |
21 else ignore (Path.basic elem handle ERROR _ => err ()); |
21 | elems => List.app Path.check_elem elems); |
22 |
|
23 val elems = space_explode "/" name; |
|
24 val _ = null elems andalso err (); |
|
25 val _ = List.app check_elem elems; |
|
26 in name end; |
22 in name end; |
27 |
23 |
28 fun gen_export compress thy name body = |
24 fun gen_export compress thy name body = |
29 (Output.try_protocol_message o Markup.export) |
25 (Output.try_protocol_message o Markup.export) |
30 {id = Position.get_id (Position.thread_data ()), |
26 {id = Position.get_id (Position.thread_data ()), |