From c6b37a33ddf78119cfaf8994b32dd9aea6aeed36 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 | 21 ++++++++++++++++++--- 1 file changed, 18 insertions(+), 3 deletions(-) diff --git a/autoload/coquille.py b/autoload/coquille.py index feb0981..14eb618 100644 --- a/autoload/coquille.py +++ b/autoload/coquille.py @@ -303,21 +303,36 @@ def show_goal(self, feedback_callback): goals = response.val.val sub_goals = goals.fg + msg_format = '{0} subgoal{1}' + show_hyps = True + if not sub_goals: + show_hyps = False + 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): _id = sub_goal.id hyps = sub_goal.hyp ccl = sub_goal.ccl - if idx == 0: + if show_hyps: # we print the environment only for the current subgoal for hyp in hyps: lst = map(lambda s: s.encode('utf-8'), hyp.split('\n')) self.goal_buffer.append(list(lst)) + show_hyps = False self.goal_buffer.append('') self.goal_buffer.append('======================== ( %d / %d )' % (idx+1 , nb_subgoals)) lines = map(lambda s: s.encode('utf-8'), ccl.split('\n'))