src/Pure/Thy/export.ML
changeset 69784 24bbc4e30e5b
parent 69650 c95edf19133b
child 69788 c175499a7537
     1.1 --- a/src/Pure/Thy/export.ML	Sat Feb 02 14:51:11 2019 +0100
     1.2 +++ b/src/Pure/Thy/export.ML	Sat Feb 02 15:52:14 2019 +0100
     1.3 @@ -6,8 +6,8 @@
     1.4  
     1.5  signature EXPORT =
     1.6  sig
     1.7 -  val export: theory -> string -> string list -> unit
     1.8 -  val export_raw: theory -> string -> string list -> unit
     1.9 +  val export: theory -> Path.T -> string list -> unit
    1.10 +  val export_raw: theory -> Path.T -> string list -> unit
    1.11    val markup: theory -> string -> Markup.T
    1.12    val message: theory -> string -> string
    1.13  end;
    1.14 @@ -17,20 +17,20 @@
    1.15  
    1.16  (* export *)
    1.17  
    1.18 -fun check_name name =
    1.19 +fun check_name path =
    1.20    let
    1.21 +    val name = Path.implode path;
    1.22      val _ =
    1.23 -      (case space_explode "/" name of
    1.24 -        [] => error "Empty export name"
    1.25 -      | elems => List.app Path.check_elem elems);
    1.26 +      if not (Path.is_current path) andalso Path.all_basic path then ()
    1.27 +      else error ("Bad export name: " ^ quote name);
    1.28    in name end;
    1.29  
    1.30 -fun gen_export compress thy name body =
    1.31 +fun gen_export compress thy path body =
    1.32    (Output.try_protocol_message o Markup.export)
    1.33     {id = Position.get_id (Position.thread_data ()),
    1.34      serial = serial (),
    1.35      theory_name = Context.theory_long_name thy,
    1.36 -    name = check_name name,
    1.37 +    name = check_name path,
    1.38      compress = compress} body;
    1.39  
    1.40  val export = gen_export true;