Modif de coq-tex - meilleur affichage des suite de coq_example's

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4003 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 20 insertions, 5 deletions

diff --git a/tools/coq-tex.ml4 b/tools/coq-tex.ml4
index 5c445c633..5f42c03b0 100644
--- a/tools/coq-tex.ml4
+++ b/tools/coq-tex.ml4
@@ -135,8 +135,26 @@ let insert texfile coq_output result =
     in
     let first = !last_read in first :: (read_lines ())
   in
+  (* we are just after \end{coq_...} block *)
+  let rec just_after () = 
+    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     
+      else begin
+	output_string c_out (s ^ "\n");
+	outside ()
+      end	  
+    end
   (* we are outside of a \begin{coq_...} ... \end{coq_...} block *)
-  let rec outside () =
+  and outside () =
     let s = input_line c_tex in
     if Str.string_match begin_coq_example s 0 then begin
       if !small then output_string c_out "\\begin{small}\n";
@@ -156,10 +174,7 @@ let insert texfile coq_output result =
   and inside show_answers  show_questions k first_block = 
     let s = input_line c_tex in
     if Str.string_match end_coq_example s 0 then 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";
-      outside ()
+      just_after ()
     end else begin
       if !verbose then Printf.printf "Coq < %s\n" s;
       if (not first_block) & k=0 then output_string c_out "\\medskip\n";