Simplify extract_ocaml_code.

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 \

doc/extract_ocaml_code.ml

-
 (*
 
-Simple utility to extract a portion of a file
+Simple utility to extract a portion of the standard input
 
-  extract_ocaml_code <path/file.ext> <id> <dir>
+  extract_ocaml_code <id>
 
-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 <path/file.ext> <id> <dir>@\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 <id>@\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 ()