diff options
author | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2014-04-28 16:04:59 +0200 |
---|---|---|
committer | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2014-04-28 16:04:59 +0200 |
commit | d9dbff8b8e421406cf76526e39e9504779cbadf0 (patch) | |
tree | 5c8fc32a23220cfd585964b3b0e8c081dc9410c6 | |
parent | 056a969e5d4cd5752bfccf7797ba46c4bcf0b70d (diff) |
Reduce the amount of "Coq <" prompts generated by coq_tex. (Partial fix for bug #2964)
-rw-r--r-- | tools/coq_tex.ml | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/tools/coq_tex.ml b/tools/coq_tex.ml index e2d66b4ab..78cd801a4 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; |