Merge branch 'v8.5'

8 files changed, 98 insertions, 129 deletions

diff --git a/tools/README.coq-tex b/tools/README.coq-tex
deleted file mode 100755
index 5c7606a96..000000000
--- a/tools/README.coq-tex
+++ /dev/null
@@ -1,13 +0,0 @@
-DESCRIPTION.
-
-The coq-tex filter extracts Coq phrases embedded in LaTeX files,
-evaluates them, and insert the outcome of the evaluation after each
-phrase.
-
-The filter is written in Perl, so you'll need Perl version 4 installed
-on your machine.
-
-USAGE. See the manual page (coq-tex.1).
-
-AUTHOR. Jean-Christophe Filliatre (jcfillia@lip.ens-lyon.fr)
-  from caml-tex of Xavier Leroy.
diff --git a/tools/README.emacs b/tools/README.emacs
index 4d8e3697a..4d8e3697a 100755..100644
--- a/tools/README.emacs
+++ b/tools/README.emacs
diff --git a/tools/coq-sl.sty b/tools/coq-sl.sty
index 9f6e5480c..9f6e5480c 100755..100644
--- a/tools/coq-sl.sty
+++ b/tools/coq-sl.sty
diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml
index 954c21d58..e902370c3 100644
--- a/tools/coq_makefile.ml
+++ b/tools/coq_makefile.ml
@@ -843,11 +843,9 @@ let do_makefile args =
   if not (makefile = None) then close_out !output_channel;
   exit 0
 
-let main () =
+let _ =
   let args =
     if Array.length Sys.argv = 1 then usage ();
     List.tl (Array.to_list Sys.argv)
   in
     do_makefile args
-
-let _ = Printexc.catch main ()
diff --git a/tools/coq_tex.ml b/tools/coq_tex.ml
index fc652f584..dbdc2e9db 100644
--- a/tools/coq_tex.ml
+++ b/tools/coq_tex.ml
@@ -24,10 +24,7 @@ let hrule = ref false
 let small = ref false
 let boot = ref false
 
-let coq_prompt = Str.regexp "Coq < "
-let any_prompt = Str.regexp "^[A-Z0-9a-z_\\$']* < "
-
-let remove_prompt s = Str.replace_first any_prompt "" s
+let any_prompt = Str.regexp "[A-Z0-9a-z_\\$']* < "
 
 (* First pass: extract the Coq phrases to evaluate from [texfile]
  * and put them into the file [inputv] *)
@@ -58,30 +55,19 @@ let extract texfile inputv =
       ("Set Printing Width " ^ (string_of_int !linelen) ^".\n");
     outside ()
   with End_of_file ->
-    begin close_in chan_in; close_out chan_out end
+    (* a dummy command, just in case the last line was a comment *)
+    output_string chan_out "Set Printing Width 78.\n";
+    close_in chan_in;
+    close_out chan_out
 
 (* Second pass: insert the answers of Coq from [coq_output] into the
  * TeX file [texfile]. The result goes in file [result]. *)
 
-let begin_coq_example =
-  Str.regexp "\\\\begin{coq_\\(example\\|example\\*\\|example\\#\\)}[ \t]*$"
-let begin_coq_eval = Str.regexp "\\\\begin{coq_eval}[ \t]*$"
-let end_coq_example = Str.regexp "\\\\end{coq_\\(example\\|example\\*\\|example\\#\\)}[ \t]*$"
-let end_coq_eval = Str.regexp "\\\\end{coq_eval}[ \t]*$"
-let dot_end_line = Str.regexp "\\(\\.\\|}\\)[ \t]*\\((\\*.*\\*)\\)?[ \t]*$"
-
-let has_match r s =
-  try let _ = Str.search_forward r s 0 in true with Not_found -> false
-
-let percent = Str.regexp "%"
-let bang    = Str.regexp "!"
-let expos   = Str.regexp "^"
-
 let tex_escaped s =
-  let dollar = "\\$" and  backslash = "\\\\" and expon = "\\^" in
-  let delims = Str.regexp ("[_{}&%#" ^ dollar ^ backslash ^ expon ^"~ <>'`]") in
+  let delims = Str.regexp "[_{}&%#$\\^~ <>'`]" in
   let adapt_delim = function
-    | "_" | "{" | "}" | "&" | "%" | "#" | "$" as c -> "\\"^c
+    | "{" | "}" | "&" | "%" | "#" | "$" as c -> "\\"^c
+    | "_" -> "{\\char`\\_}"
     | "\\" -> "{\\char'134}"
     | "^" -> "{\\char'136}"
     | "~" -> "{\\char'176}"
@@ -111,99 +97,106 @@ let insert texfile coq_output result =
   let c_tex = open_in texfile in
   let c_coq = open_in coq_output in
   let c_out = open_out result in
-  (* next_block k : this function reads the next block of Coq output
-   * removing the k leading prompts.
-   * it returns the block as a list of string) *)
-  let last_read = ref "" in
-  let next_block k =
-    if !last_read = "" then last_read := input_line c_coq;
-    (* skip k prompts *)
-    for _i = 1 to k do
-      last_read := remove_prompt !last_read;
-    done;
+  (* read lines until a prompt is found (starting from the second line),
+     purge prompts on the first line and return their number *)
+  let last_read = ref (input_line c_coq) in
+  let read_output () =
+    let first = !last_read in
+    let nb = ref 0 in
+    (* remove the leading prompts *)
+    let rec skip_prompts pos =
+      if Str.string_match any_prompt first pos then
+        let () = incr nb in
+        skip_prompts (Str.match_end ())
+      else pos in
+    let first =
+      let start = skip_prompts 0 in
+      String.sub first start (String.length first - start) in
     (* read and return the following lines until a prompt is found *)
     let rec read_lines () =
       let s = input_line c_coq in
       if Str.string_match any_prompt s 0 then begin
 	last_read := s; []
       end else
-	s :: (read_lines ())
-    in
-    let first = !last_read in first :: (read_lines ())
-  in
-  (* we are just after \end{coq_...} block *)
-  let rec just_after () =
+	s :: read_lines () in
+    (first :: read_lines (), !nb) in
+  let unhandled_output = ref None in
+  let read_output () =
+    match !unhandled_output with
+    | Some some -> unhandled_output := None; some
+    | None -> read_output () in
+  (* we are inside a \begin{coq_...} ... \end{coq_...} block
+   * show_... tell what kind of block it is *)
+  let rec inside show_answers show_questions not_first discarded =
     let s = input_line c_tex in
-    if Str.string_match begin_coq_example s 0 then begin
-      inside (Str.matched_group 1 s <> "example*")
-             (Str.matched_group 1 s <> "example#") 0 false
-    end
-    else begin
-      if !hrule then output_string c_out "\\hrulefill\\\\\n";
-      output_string c_out "\\end{flushleft}\n";
-      if !small then output_string c_out "\\end{small}\n";
-      if Str.string_match begin_coq_eval s 0 then
-	eval 0
+    if s = "" then
+      inside show_answers show_questions not_first (discarded + 1)
+    else if not (Str.string_match end_coq s 0) then begin
+      let (bl,n) = read_output () in
+      assert (n > discarded);
+      let n = n - discarded in
+      if not_first then output_string c_out "\\medskip\n";
+      if !verbose then Printf.printf "Coq < %s\n" s;
+      if show_questions then encapsule false c_out ("Coq < " ^ s);
+      let rec read_lines k =
+        if k = 0 then []
+        else
+          let s = input_line c_tex in
+          if Str.string_match end_coq s 0 then []
+          else s :: read_lines (k - 1) in
+      let al = read_lines (n - 1) in
+      if !verbose then List.iter (Printf.printf "      %s\n") al;
+      if show_questions then
+        List.iter (fun s -> encapsule false c_out ("      " ^ s)) al;
+      let la = n - 1 - List.length al in
+      if la <> 0 then
+        (* this happens when the block ends with a comment; the output
+           is for the command at the beginning of the next block *)
+        unhandled_output := Some (bl, la)
       else begin
-	output_string c_out (s ^ "\n");
-	outside ()
+        if !verbose then List.iter print_endline bl;
+        if show_answers then print_block c_out bl;
+        inside show_answers show_questions (show_answers || show_questions) 0
       end
-    end
+    end else if discarded > 0 then begin
+      (* this happens when the block ends with an empty line *)
+      let (bl,n) = read_output () in
+      assert (n > discarded);
+      unhandled_output := Some (bl, n - discarded)
+    end in
   (* we are outside of a \begin{coq_...} ... \end{coq_...} block *)
-  and outside () =
-    let s = input_line c_tex in
-    if Str.string_match begin_coq_example s 0 then begin
+  let rec outside just_after =
+    let start_block () =
       if !small then output_string c_out "\\begin{small}\n";
       output_string c_out "\\begin{flushleft}\n";
+      if !hrule then output_string c_out "\\hrulefill\\\\\n" in
+    let end_block () =
       if !hrule then output_string c_out "\\hrulefill\\\\\n";
-      inside (Str.matched_group 1 s <> "example*")
-             (Str.matched_group 1 s <> "example#") 0 true
-    end else if Str.string_match begin_coq_eval s 0 then
-      eval 0
-    else begin
-      output_string c_out (s ^ "\n");
-      outside ()
-    end
-  (* we are inside a \begin{coq_example?} ... \end{coq_example?} block
-   * show_answers tells what kind of block it is
-   * k is the number of lines read until now *)
-  and inside show_answers  show_questions k first_block =
+      output_string c_out "\\end{flushleft}\n";
+      if !small then output_string c_out "\\end{small}\n" in
     let s = input_line c_tex in
-    if Str.string_match end_coq_example s 0 then begin
-      just_after ()
+    if Str.string_match begin_coq s 0 then begin
+      let kind = Str.matched_group 1 s in
+      if kind = "eval" then begin
+        if just_after then end_block ();
+        inside false false false 0;
+        outside false
+      end else begin
+        let show_answers   = kind <> "example*" in
+        let show_questions = kind <> "example#" in
+        if not just_after then start_block ();
+        inside show_answers show_questions just_after 0;
+        outside true
+      end
     end else begin
-      let prompt = if k = 0 then "Coq < " else "      " in
-      if !verbose then Printf.printf "%s%s\n" prompt s;
-      if (not first_block) && k=0 then output_string c_out "\\medskip\n";
-      if show_questions then encapsule false c_out (prompt ^ s);
-      if has_match dot_end_line s then begin
-	let bl = next_block (succ k) in
-	if !verbose then List.iter print_endline bl;
-	if show_answers then print_block c_out bl;
-	inside show_answers  show_questions 0 false
-      end else
-	inside show_answers  show_questions (succ k) first_block
-    end
-  (* we are inside a \begin{coq_eval} ... \end{coq_eval} block
-   * k is the number of lines read until now *)
-  and eval k =
-    let s = input_line c_tex in
-    if Str.string_match end_coq_eval s 0 then
-      outside ()
-    else begin
-      if !verbose then Printf.printf "Coq < %s\n" s;
-      if has_match dot_end_line s then
-	let bl = next_block (succ k) in
-	if !verbose then List.iter print_endline bl;
-	eval 0
-      else
-	eval (succ k)
-    end
-  in
+      if just_after then end_block ();
+      output_string c_out (s ^ "\n");
+      outside false
+    end in
   try
-    let _ = next_block 0 in (* to skip the Coq banner *)
-    let _ = next_block 0 in (* to skip the Coq answer to Set Printing Width *)
-    outside ()
+    let _ = read_output () in (* to skip the Coq banner *)
+    let _ = read_output () in (* to skip the Coq answer to Set Printing Width *)
+    outside false
   with End_of_file -> begin
     close_in c_tex;
     close_in c_coq;
@@ -212,7 +205,7 @@ let insert texfile coq_output result =
 
 (* Process of one TeX file *)
 
-let rm f = try Sys.remove f with any -> ()
+let rm f = try Sys.remove f with _ -> ()
 
 let one_file texfile =
   let inputv = Filename.temp_file "coq_tex" ".v" in
@@ -281,7 +274,7 @@ let find_coqtop () =
     "coqtop"
   end
 
-let main () =
+let _ =
   parse_cl ();
   if !image = "" then image := Filename.quote (find_coqtop ());
   if !boot then image := !image ^ " -boot";
@@ -294,5 +287,3 @@ let main () =
     flush stdout
   end;
   List.iter one_file (List.rev !files)
-
-let _ = Printexc.catch main ()
diff --git a/tools/coqdoc/main.ml b/tools/coqdoc/main.ml
index 9531cd2b0..2554ed495 100644
--- a/tools/coqdoc/main.ml
+++ b/tools/coqdoc/main.ml
@@ -557,10 +557,8 @@ let produce_output fl =
 (*s \textbf{Main program.} Print the banner, parse the command line,
     read the files and then call [produce_document] from module [Web]. *)
 
-let main () =
+let _ =
   let files = parse () in
     Index.init_coqlib_library ();
     if not !quiet then banner ();
     if files <> [] then produce_output files
-
-let _ = Printexc.catch main ()
diff --git a/tools/coqwc.mll b/tools/coqwc.mll
index 417ec5355..9a42553da 100644
--- a/tools/coqwc.mll
+++ b/tools/coqwc.mll
@@ -276,7 +276,7 @@ let rec parse = function
 
 (*s Main program. *)
 
-let main () =
+let _ =
   let files = parse (List.tl (Array.to_list Sys.argv)) in
   if not (!spec_only || !proof_only) then
     printf "     spec    proof comments\n";
@@ -285,8 +285,6 @@ let main () =
     | [f] -> process_file f
     | _ -> List.iter process_file files; print_totals ()
 
-let _ = Printexc.catch main ()
-
 (*i*)}(*i*)
 
 
diff --git a/tools/gallina.ml b/tools/gallina.ml
index 279919c58..5ce19e7f8 100644
--- a/tools/gallina.ml
+++ b/tools/gallina.ml
@@ -39,7 +39,7 @@ let traite_stdin () =
   with Sys_error _ ->
     ()
 
-let gallina () =
+let _ =
   let lg_command = Array.length Sys.argv in
   if lg_command < 2 then begin
     output_string stderr "Usage: gallina [-] [-stdout] file1 file2 ...\n";
@@ -59,6 +59,3 @@ let gallina () =
     traite_stdin ()
   else
     List.iter traite_fichier !vfiles
-
-let _ = Printexc.catch gallina ()
-