From c4e8f5014fbc340a2fd15a6a4b4881d5a6e700b5 Mon Sep 17 00:00:00 2001 From: Kyle Stemen Date: Mon, 2 Oct 2017 23:22:12 -0700 Subject: [PATCH] If there are no focused goals, print the unfocused goals Match the coqide's goal message format. This is important for indicating whether an unfocused goal needs to be focused or the proof is done. --- autoload/coquille.py | 16 ++++++++++++++-- 1 file changed, 14 insertions(+), 2 deletions(-) diff --git a/autoload/coquille.py b/autoload/coquille.py index feb0981..2910a92 100644 --- a/autoload/coquille.py +++ b/autoload/coquille.py @@ -303,10 +303,22 @@ def show_goal(self, feedback_callback): goals = response.val.val sub_goals = goals.fg + msg_format = '{0} subgoal{1}' + if not sub_goals: + sub_goals = [] + for (before, after) in goals.bg: + sub_goals.extend(reversed(before)) + sub_goals.extend(after) + if sub_goals: + msg_format = ('This subproof is complete, but there {2} {0}' + ' unfocused goal{1}') + if not sub_goals: + msg_format = 'No more subgoals.' nb_subgoals = len(sub_goals) - plural_opt = '' if nb_subgoals == 1 else 's' - self.goal_buffer[0] = '%d subgoal%s' % (nb_subgoals, plural_opt) + self.goal_buffer[0] = msg_format.format(nb_subgoals, + '' if nb_subgoals == 1 else 's', + 'is' if nb_subgoals == 1 else 'are') self.goal_buffer.append(['']) for idx, sub_goal in enumerate(sub_goals):