diff --git a/Makefile.in b/Makefile.in index e8d4e13ed3b8456a5c757b7e7eba1336371ce8a1..cab9aaef027c55fffd840e8c5457361118fe1005 100644 --- a/Makefile.in +++ b/Makefile.in @@ -1873,19 +1873,19 @@ doc/extract_ocaml_code: doc/extract_ocaml_code.ml $(OCAMLC) str.cma -o $@ $< doc/logic__%.ml: examples/use_api/logic.ml doc/extract_ocaml_code - doc/extract_ocaml_code examples/use_api/logic.ml $* doc + doc/extract_ocaml_code $* < $< > $@ doc/whyconf__%.ml: src/driver/whyconf.ml doc/extract_ocaml_code - doc/extract_ocaml_code src/driver/whyconf.ml $* doc + doc/extract_ocaml_code $* < $< > $@ doc/call_provers__%.ml: src/driver/call_provers.ml doc/extract_ocaml_code - doc/extract_ocaml_code src/driver/call_provers.ml $* doc + doc/extract_ocaml_code $* < $< > $@ doc/mlw_tree__%.ml: examples/use_api/mlw_tree.ml doc/extract_ocaml_code - doc/extract_ocaml_code examples/use_api/mlw_tree.ml $* doc + doc/extract_ocaml_code $* < $< > $@ doc/transform__%.ml: examples/use_api/transform.ml doc/extract_ocaml_code - doc/extract_ocaml_code examples/use_api/transform.ml $* doc + doc/extract_ocaml_code $* < $< > $@ OCAMLCODE_LOGIC = opening printformula declarepropvars declarepropatoms \ buildtask printtask buildtask2 \ diff --git a/doc/extract_ocaml_code.ml b/doc/extract_ocaml_code.ml index 141564fea5c04c916b2a3e14f38703a7eec791b3..e021bd9aec78267f3466ccd68f25aa1473107b0a 100644 --- a/doc/extract_ocaml_code.ml +++ b/doc/extract_ocaml_code.ml @@ -1,93 +1,52 @@ - (* -Simple utility to extract a portion of a file +Simple utility to extract a portion of the standard input - extract_ocaml_code + extract_ocaml_code -extracts the part of path/file.ext between lines containing anchors BEGIN{id} and END{id} -and puts the result in the file dir/file_id.ext +outputs the part of the standard input between anchors BEGIN{id} and END{id} *) -open Format - -let filename,section,output_dir = - if Array.length Sys.argv = 4 then - Sys.argv.(1), Sys.argv.(2), Sys.argv.(3) - else - begin - eprintf "Usage: %s @\n\ -Extract the part of path/file.ext between lines containing anchors BEGIN{id} and END{id}@\n\ -and puts the result in the file dir/file_id.ext@." - Sys.argv.(0); - exit 2 - end - -let ch_in = - try - open_in filename - with - exn -> - eprintf "Cannot open %s for reading: %s@." filename (Printexc.to_string exn); - exit 1 - -let basename = Filename.basename filename - -let ext = Filename.extension basename - -let basename = Filename.remove_extension basename +let section = + match Sys.argv with + | [| _; section |] -> section + | _ -> + Format.eprintf "Usage: %s @\n\ +Output the part of the standard input between anchors BEGIN{id} and END{id}@." + Sys.argv.(0); + exit 2 let begin_re = Str.regexp_string ("BEGIN{" ^ section ^ "}") let search_begin () = try while true do - let l = input_line ch_in in + let l = read_line () in try let _ = Str.search_forward begin_re l 0 in raise Exit with Not_found -> () done with - End_of_file -> - eprintf "Error: opening anchor BEGIN{%s} not found in file %s@." section filename; - close_in ch_in; + | End_of_file -> + Format.eprintf "Error: opening anchor BEGIN{%s} not found@." section; exit 1 | Exit -> () let end_re = Str.regexp_string ("END{" ^ section ^ "}") -let file_out = Filename.concat output_dir (basename ^ "__" ^ section ^ ext) - -let ch_out = - try - open_out file_out - with - exn -> - eprintf "Cannot open %s for writing: %s@." file_out (Printexc.to_string exn); - close_in ch_in; - exit 1 - let search_end () = try while true do - let l = input_line ch_in in + let l = read_line () in try let _ = Str.search_forward end_re l 0 in raise Exit with Not_found -> - output_string ch_out l; - output_char ch_out '\n' + print_string l; + print_char '\n' done - with - End_of_file -> - eprintf "Error: ending anchor END{%s} not found in file %s@." section filename; - close_in ch_in; - close_out ch_out; - exit 1 - | Exit -> - close_in ch_in; - close_out ch_out + with Exit -> () let () = search_begin (); search_end ()