diff options
Diffstat (limited to 'ide/ideproof.ml')
| -rw-r--r-- | ide/ideproof.ml | 40 |
1 files changed, 24 insertions, 16 deletions
diff --git a/ide/ideproof.ml b/ide/ideproof.ml index b79d6469..697e7f4f 100644 --- a/ide/ideproof.ml +++ b/ide/ideproof.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -109,31 +109,39 @@ let mode_cesar (proof:GText.view) = function proof#buffer#insert ("thesis := \n "^cur_goal^"\n"); ignore (proof#scroll_to_iter (proof#buffer#get_iter_at_mark `INSERT)) +let rec flatten = function +| [] -> [] +| (lg, rg) :: l -> + let inner = flatten l in + List.rev_append lg inner @ rg + let display mode (view:GText.view) goals hints evars = let () = view#buffer#set_text "" in match goals with | None -> () (* No proof in progress *) - | Some { Interface.fg_goals = []; Interface.bg_goals = [] } -> - (* A proof has been finished, but not concluded *) - begin match evars with - | Some evs when evs <> [] -> + | Some { Interface.fg_goals = []; Interface.bg_goals = bg } -> + let bg = flatten (List.rev bg) in + let evars = match evars with None -> [] | Some evs -> evs in + begin match (bg, evars) with + | [], [] -> + view#buffer#insert "No more subgoals." + | [], _ :: _ -> + (* A proof has been finished, but not concluded *) view#buffer#insert "No more subgoals but non-instantiated existential variables:\n\n"; let iter evar = let msg = Printf.sprintf "%s\n" evar.Interface.evar_info in view#buffer#insert msg in - List.iter iter evs - | _ -> - view#buffer#insert "No more subgoals." + List.iter iter evars + | _, _ -> + (* No foreground proofs, but still unfocused ones *) + view#buffer#insert "This subproof is complete, but there are still unfocused goals:\n\n"; + let iter goal = + let msg = Printf.sprintf "%s\n" goal.Interface.goal_ccl in + view#buffer#insert msg + in + List.iter iter bg end - | Some { Interface.fg_goals = []; Interface.bg_goals = bg } -> - (* No foreground proofs, but still unfocused ones *) - view#buffer#insert "This subproof is complete, but there are still unfocused goals:\n\n"; - let iter goal = - let msg = Printf.sprintf "%s\n" goal.Interface.goal_ccl in - view#buffer#insert msg - in - List.iter iter bg | Some { Interface.fg_goals = fg } -> mode view fg hints |