| 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 aut_xl = initial_lexer AutLexer.token
-let entity_of_input lexbuf = function
- | Text ->
+let parbuf = ref [] (* parser buffer *)
+
+let gen_text command =
+ parbuf := TxtEntity command :: !parbuf
+
+let entity_of_input lexbuf i = match i, !parbuf with
+ | Text, [] ->
begin match TxtParser.entry (token txt_xl) lexbuf with
| Some e, unget -> txt_xl.unget <- unget; Some (TxtEntity e)
| None, _ -> None
end
- | Automath ->
+ | Text, hd :: tl ->
+ parbuf := tl; Some hd
+ | Automath, _ ->
begin match AutParser.entry (token aut_xl) lexbuf with
| Some e, unget -> aut_xl.unget <- unget; Some (AutEntity e)
| None, _ -> 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 =
match entity, !old with
| AutEntity e, true -> MA.meta_of_aut frr h st.mst e
| AutEntity e, false -> DA.crg_of_aut err g st.dst e
- | TxtEntity e, false -> DT.crg_of_txt crr d st.tst e
+ | TxtEntity e, false -> DT.crg_of_txt crr d gen_text st.tst e
| _ -> assert false
in
let st = if !L.level > 2 then count_input st entity else st in
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