From 9952f1a90566f4ad5ba029a082e758b9a0bc8ee4 Mon Sep 17 00:00:00 2001 From: aspiwack Date: Mon, 5 Apr 2010 15:12:27 +0000 Subject: Changement de ide/proofs.ml en ide/ideproofs.ml pour éviter un conflit avec le futur commit de la nouvelle machinerie de preuve. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12901 85f007b7-540e-0410-9357-904b9bb8a0f7 --- ide/coqide.ml | 14 ++++----- ide/ide.mllib | 2 +- ide/ideproof.ml | 95 +++++++++++++++++++++++++++++++++++++++++++++++++++++++++ ide/proof.ml | 95 --------------------------------------------------------- 4 files changed, 103 insertions(+), 103 deletions(-) create mode 100644 ide/ideproof.ml delete mode 100644 ide/proof.ml diff --git a/ide/coqide.ml b/ide/coqide.ml index 6e80c9ae68..4fa0c28f51 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -735,9 +735,9 @@ object(self) match Decl_mode.get_current_mode () with Decl_mode.Mode_none -> () | Decl_mode.Mode_tactic -> - Proof.display (Proof.mode_tactic (fun _ _ -> ())) proof_view (Coq.goals Coq.dummy_coqtop) + Ideproof.display (Ideproof.mode_tactic (fun _ _ -> ())) proof_view (Coq.goals Coq.dummy_coqtop) | Decl_mode.Mode_proof -> - Proof.display Proof.mode_cesar proof_view (Coq.goals Coq.dummy_coqtop) + Ideproof.display Ideproof.mode_cesar proof_view (Coq.goals Coq.dummy_coqtop) with e -> prerr_endline ("Don't worry be happy despite: "^Printexc.to_string e) @@ -750,12 +750,12 @@ object(self) match Decl_mode.get_current_mode () with Decl_mode.Mode_none -> () | Decl_mode.Mode_tactic -> - Proof.display - (Proof.mode_tactic (fun s () -> ignore (self#insert_this_phrase_on_success + Ideproof.display + (Ideproof.mode_tactic (fun s () -> ignore (self#insert_this_phrase_on_success true true false ("progress "^s) s))) proof_view (Coq.goals Coq.dummy_coqtop) | Decl_mode.Mode_proof -> - Proof.display Proof.mode_cesar proof_view (Coq.goals Coq.dummy_coqtop) + Ideproof.display Ideproof.mode_cesar proof_view (Coq.goals Coq.dummy_coqtop) with e -> prerr_endline (Printexc.to_string e) end @@ -2442,10 +2442,10 @@ let main files = ignore (templates_factory#add_item menu_text ~callback ?key) in add_complex_template - ("_Lemma __", "Lemma new_lemma : .\nProof.\n\nSave.\n", + ("_Lemma __", "Lemma new_lemma : .\nIdeproof.\n\nSave.\n", 19, 9, Some GdkKeysyms._L); add_complex_template - ("_Theorem __", "Theorem new_theorem : .\nProof.\n\nSave.\n", + ("_Theorem __", "Theorem new_theorem : .\nIdeproof.\n\nSave.\n", 19, 11, Some GdkKeysyms._T); add_complex_template ("_Definition __", "Definition ident := .\n", diff --git a/ide/ide.mllib b/ide/ide.mllib index fe91cf3391..1ead88c8ec 100644 --- a/ide/ide.mllib +++ b/ide/ide.mllib @@ -13,7 +13,7 @@ Config_lexer Utf8_convert Preferences Ideutils -Proof +Ideproof Coq_lex Gtk_parsing Undo diff --git a/ide/ideproof.ml b/ide/ideproof.ml new file mode 100644 index 0000000000..700b5a7295 --- /dev/null +++ b/ide/ideproof.ml @@ -0,0 +1,95 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* + let iter = new GText.iter it in + let start = iter#backward_to_tag_toggle (Some tag) in + let stop = iter#forward_to_tag_toggle (Some tag) in + match GdkEvent.get_type evt with + | `BUTTON_PRESS -> + let ev = GdkEvent.Button.cast evt in + if (GdkEvent.Button.button ev) <> 3 then false else begin + let ctxt_menu = GMenu.menu () in + let factory = new GMenu.factory ctxt_menu in + List.iter + (fun (text,cmd) -> ignore (factory#add_item text ~callback:(sel_cb cmd))) + menu_content; + ctxt_menu#popup ~button:3 ~time:(GdkEvent.Button.time ev); + true + end + | `MOTION_NOTIFY -> + hover_cb start stop; false + | _ -> false)) + +let mode_tactic sel_cb (proof:GText.view) = function + | [] -> assert false + | (hyps,(cur_goal,cur_goal_menu))::rem_goals -> + let on_hover sel_start sel_stop = + proof#buffer#remove_tag + ~start:proof#buffer#start_iter + ~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 + let insert_hyp (h,menu) = + let tag = proof#buffer#create_tag [] in + hook_tag_cb tag menu sel_cb on_hover; + proof#buffer#insert ~tags:[tag] (h^"\n") + in + let insert_goal g menu index total = + let tags = if menu <> [] then + let tag = proof#buffer#create_tag [] in + hook_tag_cb tag menu sel_cb on_hover; + [tag] + else [] + in + proof#buffer#insert (Printf.sprintf + "\n______________________________________(%d/%d)\n" index total); + proof#buffer#insert ~tags (g^"\n") + in + 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; + ignore (proof#scroll_to_iter + ((proof#buffer#get_iter_at_mark `INSERT)#backward_lines (3*goals_cnt - 2))) + +let mode_cesar (proof:GText.view) = function + | [] -> assert false + | (hyps,(cur_goal,cur_goal_menu))::_ -> + proof#buffer#insert " *** Declarative Mode ***\n"; + List.iter + (fun (hyp,_) -> proof#buffer#insert (hyp^"\n")) + hyps; + proof#buffer#insert "______________________________________\n"; + proof#buffer#insert ("thesis := \n "^cur_goal^"\n"); + ignore (proof#scroll_to_iter (proof#buffer#get_iter_at_mark `INSERT)) + +let display mode (view:GText.view) goals = + view#buffer#set_text ""; + match goals with + | Coq.Message msg -> + view#buffer#insert msg + | Coq.Goals g -> + mode view g diff --git a/ide/proof.ml b/ide/proof.ml deleted file mode 100644 index 700b5a7295..0000000000 --- a/ide/proof.ml +++ /dev/null @@ -1,95 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* - let iter = new GText.iter it in - let start = iter#backward_to_tag_toggle (Some tag) in - let stop = iter#forward_to_tag_toggle (Some tag) in - match GdkEvent.get_type evt with - | `BUTTON_PRESS -> - let ev = GdkEvent.Button.cast evt in - if (GdkEvent.Button.button ev) <> 3 then false else begin - let ctxt_menu = GMenu.menu () in - let factory = new GMenu.factory ctxt_menu in - List.iter - (fun (text,cmd) -> ignore (factory#add_item text ~callback:(sel_cb cmd))) - menu_content; - ctxt_menu#popup ~button:3 ~time:(GdkEvent.Button.time ev); - true - end - | `MOTION_NOTIFY -> - hover_cb start stop; false - | _ -> false)) - -let mode_tactic sel_cb (proof:GText.view) = function - | [] -> assert false - | (hyps,(cur_goal,cur_goal_menu))::rem_goals -> - let on_hover sel_start sel_stop = - proof#buffer#remove_tag - ~start:proof#buffer#start_iter - ~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 - let insert_hyp (h,menu) = - let tag = proof#buffer#create_tag [] in - hook_tag_cb tag menu sel_cb on_hover; - proof#buffer#insert ~tags:[tag] (h^"\n") - in - let insert_goal g menu index total = - let tags = if menu <> [] then - let tag = proof#buffer#create_tag [] in - hook_tag_cb tag menu sel_cb on_hover; - [tag] - else [] - in - proof#buffer#insert (Printf.sprintf - "\n______________________________________(%d/%d)\n" index total); - proof#buffer#insert ~tags (g^"\n") - in - 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; - ignore (proof#scroll_to_iter - ((proof#buffer#get_iter_at_mark `INSERT)#backward_lines (3*goals_cnt - 2))) - -let mode_cesar (proof:GText.view) = function - | [] -> assert false - | (hyps,(cur_goal,cur_goal_menu))::_ -> - proof#buffer#insert " *** Declarative Mode ***\n"; - List.iter - (fun (hyp,_) -> proof#buffer#insert (hyp^"\n")) - hyps; - proof#buffer#insert "______________________________________\n"; - proof#buffer#insert ("thesis := \n "^cur_goal^"\n"); - ignore (proof#scroll_to_iter (proof#buffer#get_iter_at_mark `INSERT)) - -let display mode (view:GText.view) goals = - view#buffer#set_text ""; - match goals with - | Coq.Message msg -> - view#buffer#insert msg - | Coq.Goals g -> - mode view g -- cgit v1.2.3