diff options
| author | ppedrot | 2011-12-15 18:30:46 +0000 |
|---|---|---|
| committer | ppedrot | 2011-12-15 18:30:46 +0000 |
| commit | b076264235980e60d51a5d0b8d3a4e9c3f4d82eb (patch) | |
| tree | 78a9d74850834a6fc4a413304ef6ec034e4763f2 /ide/coqide.ml | |
| parent | 97c848795c1c26e6413737e9b8150eb9335946ed (diff) | |
Cleaned up a bit goal handling in Coqtop interface. Now we have two queries : goal description, with focused and unfocused goals, and list of currently declared evars.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14793 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'ide/coqide.ml')
| -rw-r--r-- | ide/coqide.ml | 24 |
1 files changed, 15 insertions, 9 deletions
diff --git a/ide/coqide.ml b/ide/coqide.ml index 2c6e96218b..7a1d184856 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -825,17 +825,23 @@ object(self) else (fun _ _ -> ()) in try - match Coq.goals !mycoqtop with - | Interface.Fail (l,str) -> + begin match Coq.goals !mycoqtop with + | Interface.Fail (l, str) -> self#set_message ("Error in coqtop :\n"^str) | Interface.Good goals -> - let hints = match Coq.hints !mycoqtop with - | Interface.Fail (_, _) -> None - | Interface.Good hints -> hints - in - Ideproof.display - (Ideproof.mode_tactic menu_callback) - proof_view goals hints + begin match Coq.evars !mycoqtop with + | Interface.Fail (l, str) -> + self#set_message ("Error in coqtop :\n"^str) + | Interface.Good evs -> + let hints = match Coq.hints !mycoqtop with + | Interface.Fail (_, _) -> None + | Interface.Good hints -> hints + in + Ideproof.display + (Ideproof.mode_tactic menu_callback) + proof_view goals hints evs + end + end with | e -> prerr_endline (Printexc.to_string e) end |