| BagEntity e -> {st with bagc = BagO.count_entity C.start st.bagc e}
| _ -> st
-let export_entity si moch = function
- | CrgEntity e -> X.export_entity DO.export_term si e
- | BrgEntity e -> X.export_entity BrgO.export_term si e
+let export_entity si xdir moch = function
+ | CrgEntity e -> X.export_entity DO.export_term si xdir e
+ | BrgEntity e -> X.export_entity BrgO.export_term si xdir e
| MetaEntity e ->
begin match moch with
| None -> ()
let preprocess = ref false
let root = ref ""
let cc = ref false
-let export = ref false
+let export = ref ""
let old = ref false
let st = ref (initial_status ())
let process_2 st entity =
let st = if !L.level > 2 then count_entity st entity else st in
- if !export then export_entity !O.si !moch entity;
+ if !export <> "" then export_entity !O.si !export !moch entity;
if !stage > 2 then type_check st entity else st
let process_1 st entity =
if !progress then pp_progress entity;
let st = if !L.level > 2 then count_entity st entity else st in
- if !export && !stage = 1 then export_entity !O.si !moch entity;
+ if !export <> "" && !stage = 1 then export_entity !O.si !export !moch entity;
if !stage > 1 then process_2 st (xlate_entity entity) else st
let process_0 st entity =
let f och = moch := Some och in
ML.open_out f name
in
+ let set_xdir s = export := s in
let set_root s = root := s in
let close = function
| None -> ()
in
let clear_options () =
stage := 3; moch := None; meta := false; progress := false;
- preprocess := false; root := ""; cc := false; export := false;
+ preprocess := false; root := ""; cc := false; export := "";
old := false; kernel := Brg; st := initial_status ();
L.clear (); O.clear (); H.clear (); Op.clear_reductions ()
in
flush_all ()
in
let help =
- "Usage: helena [ -VXcgijmopqux | -Ss <number> | -hkr <string> ] <file> ...\n\n" ^
+ "Usage: helena [ -VXcgijmopqu | -Ss <number> | -x <dir> | -hkr <string> ]* [ <file> ]*\n\n" ^
"Summary levels: 0 just errors (default), 1 time stamps, 2 processed file names, \
3 data information, 4 typing information, 5 reduction information\n\n" ^
"Stages: 0 parsing, 1 to intermediate, 2 to untrusted, 3 to trusted (default)\n"
let help_r = "<string> set initial segment of URI hierarchy" in
let help_s = "<number> set translation stage (see above)" in
let help_u = " activate sort inclusion" in
- let help_x = " export kernel entities (XML)" in
+ let help_x = "<dir> export kernel entities (XML) to <dir>" in
L.box 0; L.box_err ();
at_exit exit;
Arg.parse [
("-r", Arg.String set_root, help_r);
("-s", Arg.Int set_stage, help_s);
("-u", Arg.Set O.si, help_u);
- ("-x", Arg.Set export, help_x)
+ ("-x", Arg.String set_xdir, help_x)
] process_file help;
with BagT.TypeError msg -> bag_error "Type Error" msg