From d9dbff8b8e421406cf76526e39e9504779cbadf0 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Mon, 28 Apr 2014 16:04:59 +0200
Subject: Reduce the amount of "Coq <" prompts generated by coq_tex. (Partial
 fix for bug #2964)

---
 tools/coq_tex.ml | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

(limited to 'tools/coq_tex.ml')

diff --git a/tools/coq_tex.ml b/tools/coq_tex.ml
index e2d66b4abc..78cd801a48 100644
--- a/tools/coq_tex.ml
+++ b/tools/coq_tex.ml
@@ -171,9 +171,10 @@ let insert texfile coq_output result =
     if Str.string_match end_coq_example s 0 then begin
       just_after ()
     end else begin
-      if !verbose then Printf.printf "Coq < %s\n" s;
+      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 ("Coq < " ^ s);
+      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;
-- 
cgit v1.2.3