Handle errors where coqtop reports it failed in state 0

If the error is serious enough, coqtop reports it happened in state 0. It is
not possible to revert to state 0, because that is before the Init call. So
skip the revert completely if coqtop says state 0.

autoload/coqtop.py

@@ -463,6 +463,11 @@ def goals(self, feedback_callback):
         vp = self.call('Goal', (), feedback_callback=feedback_callback)
         if isinstance(vp, Ok):
             return vp
+        if vp.revert_state.id == 0:
+            if vp.err not in self.error_messages:
+                self.error_messages.append(vp.err)
+            # Can't revert to state 0 (which is before the Init)
+            return vp
         # An error occurred. Revert back to the state coqtop requested, and ask
         # for the goal again.
         revert_count = 0

autoload/coquille.py

@@ -264,10 +264,10 @@ def update():
         # trigger it to start processing all the commands that have been added.
         # So show_goal needs to be called before waiting for all the unchecked
         # commands finished.
-        self.show_goal(update)
-        while self.coq_top.has_unchecked_commands():
-            self.coq_top.process_response()
-            update()
+        if self.show_goal(update):
+            while self.coq_top.has_unchecked_commands():
+                self.coq_top.process_response()
+                update()
         update()
 
     def show_goal(self, feedback_callback):
@@ -282,14 +282,14 @@ def show_goal(self, feedback_callback):
             if response is None:
                 vim.command("call coquille#KillSession()")
                 print('ERROR: the Coq process died')
-                return
+                return False
 
             if isinstance(response, CT.Err):
-                return
+                return False
 
             if response.val.val is None:
                 self.goal_buffer[0] = 'No goals.'
-                return
+                return True
 
             goals = response.val.val
 
@@ -316,6 +316,7 @@ def show_goal(self, feedback_callback):
                 self.goal_buffer.append('')
         finally:
             self.goal_buffer.options["modifiable"] = modifiable
+        return True
 
     def show_info(self, message):
         # Temporarily make the info buffer modifiable