diff options
| author | aspiwack | 2011-02-10 10:10:58 +0000 |
|---|---|---|
| committer | aspiwack | 2011-02-10 10:10:58 +0000 |
| commit | ac776b4660e95577eb6742200d882b8cf683cc10 (patch) | |
| tree | 40cd96020ddd0a3f23f2580c2921d27001186161 /plugins/decl_mode/decl_mode.ml | |
| parent | daf397883f9b7f79eeddc6cc4580ecdc5ec793f5 (diff) | |
Started to fix the declarative proof mode (C-zar).
Everything seems to work fine in CoqIDE (except escape/return and the daimon which are not entirely ported).
However, there is some problem causing proof general to fail when using goto or evaluate buffer (evaluate next phrase works fine though), as well as coqc.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13817 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/decl_mode/decl_mode.ml')
| -rw-r--r-- | plugins/decl_mode/decl_mode.ml | 23 |
1 files changed, 19 insertions, 4 deletions
diff --git a/plugins/decl_mode/decl_mode.ml b/plugins/decl_mode/decl_mode.ml index 232edda0fd..af6aa4bf59 100644 --- a/plugins/decl_mode/decl_mode.ml +++ b/plugins/decl_mode/decl_mode.ml @@ -66,7 +66,7 @@ type command_mode = | Mode_none let mode_of_pftreestate pts = - (* spiwack: it was "top_goal_..." but this should be fine *) + (* spiwack: it used to be "top_goal_..." but this should be fine *) let { it = goals ; sigma = sigma } = Proof.V82.subgoals pts in let goal = List.hd goals in if info.get (Goal.V82.extra sigma goal) = None then @@ -96,10 +96,25 @@ let get_stack pts = let info = get_info sigma (List.hd goals) in info.pm_stack + +let proof_focus = Proof.new_focus_kind () +let proof_cond = Proof.no_cond proof_focus + +let focus p = + let inf = get_stack p in + Proof.focus proof_cond inf 1 p + +let unfocus = Proof.unfocus proof_focus + +let maximal_unfocus = Proof_global.maximal_unfocus proof_focus + let get_top_stack pts = - let { it = gl ; sigma = sigma } = Proof.V82.top_goal pts in - let info = get_info sigma gl in - info.pm_stack + try + Proof.get_at_focus proof_focus pts + with Proof.NoSuchFocus -> + let { it = gl ; sigma = sigma } = Proof.V82.top_goal pts in + let info = get_info sigma gl in + info.pm_stack let get_last env = try |