reductions_menu_item#set_submenu reductions;
tactics_menu_item#set_submenu tactics;
let normalize = add_menu_item ~menu:reductions ~label:"Normalize" () in
- let reduce = add_menu_item ~menu:reductions ~label:"Reduce" () in
let simplify = add_menu_item ~menu:reductions ~label:"Simplify" () in
let whd = add_menu_item ~menu:reductions ~label:"Weak head" () in
menu#append (GMenu.separator_item ());
let copy = add_menu_item ~stock:`COPY () in
let gui = get_gui () in
List.iter (fun item -> item#misc#set_sensitive gui#canCopy)
- [ copy; check; normalize; reduce; simplify; whd ];
+ [ copy; check; normalize; simplify; whd ];
let reduction_action kind () =
let pat = self#tactic_text_pattern_of_selection in
let statement =
(MatitaScript.current ())#advance ~statement () in
connect_menu_item copy gui#copy;
connect_menu_item normalize (reduction_action `Normalize);
- connect_menu_item reduce (reduction_action `Reduce);
connect_menu_item simplify (reduction_action `Simpl);
connect_menu_item whd (reduction_action `Whd);
menu#popup ~button:right_button ~time
ApplyTransformation.txt_of_cic_sequent_conclusion ~map_unicode_to_tex
~output_type text_width metasenv cic_sequent
- method private pattern_of term context unsh_sequent =
- let context_len = List.length context in
+ method private pattern_of term father_hyp unsh_sequent =
let _, unsh_context, conclusion = unsh_sequent in
- try
- (match
- List.nth unsh_context (List.length unsh_context - context_len - 1)
- with
- | None -> assert false (* can't select a restricted hypothesis *)
- | Some (name, Cic.Decl ty) ->
- ProofEngineHelpers.pattern_of ~term:ty [term]
- | Some (name, Cic.Def (bo, _)) ->
- ProofEngineHelpers.pattern_of ~term:bo [term])
- with Failure _ | Invalid_argument _ ->
- ProofEngineHelpers.pattern_of ~term:conclusion [term]
+ let where =
+ match father_hyp with
+ None -> conclusion
+ | Some name ->
+ let rec aux =
+ function
+ [] -> assert false
+ | Some (Cic.Name name', Cic.Decl ty)::_ when name' = name -> ty
+ | Some (Cic.Name name', Cic.Def (bo,_))::_ when name' = name-> bo
+ | _::tl -> aux tl
+ in
+ aux unsh_context
+ in
+ ProofEngineHelpers.pattern_of ~term:where [term]
method private get_cic_info id =
match self#cic_info with
let cic_info, unsh_sequent = self#get_cic_info id in
let cic_sequent =
match self#get_term_by_id cic_info id with
- | SelTerm (t, _father_hyp) ->
+ | SelTerm (t, father_hyp) ->
+(*
+IDIOTA: PRIMA SI FA LA LOCATE, POI LA PATTERN_OF. MEGLIO UN'UNICA pattern_of CHE PRENDA IN INPUT UN TERMINE E UN SEQUENTE. PER IL MOMENTO RISOLVO USANDO LA father_hyp PER RITROVARE L'IPOTESI PERDUTA
+*)
let occurrences =
ProofEngineHelpers.locate_in_conjecture t unsh_sequent in
(match occurrences with
| [ context, _t ] ->
(match paste_kind with
| `Term -> ~-1, context, t
- | `Pattern -> ~-1, [], self#pattern_of t context unsh_sequent)
+ | `Pattern -> ~-1, [], self#pattern_of t father_hyp unsh_sequent)
| _ ->
HLog.error (sprintf "found %d occurrences while 1 was expected"
(List.length occurrences));
method load_logo =
notebook#set_show_tabs false;
- notebook#append_page logo
+ ignore(notebook#append_page logo)
method load_logo_with_qed =
notebook#set_show_tabs false;
- notebook#append_page logo_with_qed
+ ignore(notebook#append_page logo_with_qed)
method reset =
cicMathView#remove_selections;
let add_tab markup goal_switch =
let goal = Stack.goal_of_switch goal_switch in
if not (List.mem goal !added_goals) then begin
- notebook#append_page ~tab_label:(tab_label markup) (win goal_switch);
+ ignore(notebook#append_page
+ ~tab_label:(tab_label markup) (win goal_switch));
page2goal <- (!page, goal_switch) :: page2goal;
goal2page <- (goal_switch, !page) :: goal2page;
incr page;
ignore (win#toplevel#event#connect#delete (fun _ ->
let my_id = Oo.id self in
cicBrowsers := List.filter (fun b -> Oo.id b <> my_id) !cicBrowsers;
- if !cicBrowsers = [] &&
- Helm_registry.get "matita.mode" = "cicbrowser"
- then
- GMain.quit ();
false));
ignore(win#whelpResultTreeview#connect#row_activated
~callback:(fun _ _ ->
match self#currentCicUri with
| Some uri -> self#load (`Metadata (`Deps (`Back, uri)))
| None -> ());
+ (* remove hbugs *)
+ (*
connect_menu_item win#hBugsTutorsMenuItem (fun () ->
self#load (`HBugs `Tutors));
+ *)
+ win#hBugsTutorsMenuItem#misc#hide ();
connect_menu_item win#browserUrlMenuItem (fun () ->
win#browserUri#entry#misc#grab_focus ());
| `About `Coercions -> self#coerchgraph true ()
| `Check term -> self#_loadCheck term
| `Cic (term, metasenv) -> self#_loadTermCic term metasenv
- | `Development d -> self#_showDevelDeps d
| `Dir dir -> self#_loadDir dir
| `HBugs `Tutors -> self#_loadHBugsTutors
| `Metadata (`Deps ((`Fwd | `Back) as dir, uri)) ->
win#browserUri#entry#set_text (MatitaTypes.string_of_entry entry);
current_entry <- entry
- method private _showDevelDeps d =
- match MatitamakeLib.development_for_name d with
- | None -> ()
- | Some devel ->
- (match MatitamakeLib.dot_for_development devel with
- | None -> ()
- | Some fname ->
- gviz#load_graph_from_file ~gviz_cmd:"tred | dot" fname;
- self#_showGviz)
-
method private _loadObj obj =
(* showMath must be done _before_ loading the document, since if the
* widget is not mapped (hidden by the notebook) the document is not