diff options
| author | vgross | 2010-03-23 14:48:03 +0000 |
|---|---|---|
| committer | vgross | 2010-03-23 14:48:03 +0000 |
| commit | 96cbb1ef0a7bcc23e8fe29fe4b6e226acc5b16e5 (patch) | |
| tree | 18719e8b043513c5619de9e701235b63aabb862a /ide/proof.ml | |
| parent | a03aabb8819997fe6de3538bc3a7cf12c0dfe407 (diff) | |
Goal generation deported into ide/coq.ml, single function to obtain
all current goals.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12878 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'ide/proof.ml')
| -rw-r--r-- | ide/proof.ml | 17 |
1 files changed, 9 insertions, 8 deletions
diff --git a/ide/proof.ml b/ide/proof.ml index b91233e293..700b5a7295 100644 --- a/ide/proof.ml +++ b/ide/proof.ml @@ -38,16 +38,17 @@ let hook_tag_cb tag menu_content sel_cb hover_cb = let mode_tactic sel_cb (proof:GText.view) = function | [] -> assert false - | (hyps,cur_goal,cur_goal_menu)::rem_goals -> + | (hyps,(cur_goal,cur_goal_menu))::rem_goals -> let on_hover sel_start sel_stop = - proof#buffer#remove_tag_by_name - "highlight" + proof#buffer#remove_tag ~start:proof#buffer#start_iter - ~stop:sel_start; - proof#buffer#remove_tag_by_name - "highlight" + ~stop:sel_start + Tags.Proof.highlight; + proof#buffer#remove_tag ~start:sel_stop ~stop:proof#buffer#end_iter + Tags.Proof.highlight; + proof#buffer#apply_tag ~start:sel_start ~stop:sel_stop Tags.Proof.highlight in let goals_cnt = List.length rem_goals + 1 in let head_str = Printf.sprintf "%d subgoal%s\n" goals_cnt (if 1 < goals_cnt then "" else "s") in @@ -70,7 +71,7 @@ let mode_tactic sel_cb (proof:GText.view) = function proof#buffer#insert head_str; List.iter insert_hyp hyps; insert_goal cur_goal cur_goal_menu 1 goals_cnt; - Util.list_fold_left_i (fun i _ (_,g,_) -> insert_goal g [] i goals_cnt) 2 () rem_goals; + Util.list_fold_left_i (fun i _ (_,(g,_)) -> insert_goal g [] i goals_cnt) 2 () rem_goals; ignore (proof#scroll_to_iter ((proof#buffer#get_iter_at_mark `INSERT)#backward_lines (3*goals_cnt - 2))) @@ -85,7 +86,7 @@ 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 display mode view goals = +let display mode (view:GText.view) goals = view#buffer#set_text ""; match goals with | Coq.Message msg -> |