Rewrite the main loop of coq-tex.

Before this commit, coq-tex was reading the .v file and was guessing how
many lines from the coqtop output it should display. Now, it reads the
coqtop output and it guesses how many lines from the .v file it should
display. That way, coq-tex no longer needs to embed a parser; it relies
on coqtop for parsing.

This is much more robust and makes it possible to properly handle script
such as the following one:

  Goal { True }
     + { False }.
  { left. exact I. }

As before, if there is a way for a script to produce something that looks
like a prompt (that is, a line that starts with "foo < "), coq-tex will be
badly confused.

0 files changed, 0 insertions, 0 deletions