Bertrand's conjecture (weak), some work in progress

[helm.git] / helm / software / matita / matitaMathView.ml

diff --git a/helm/software/matita/matitaMathView.ml b/helm/software/matita/matitaMathView.ml
index f17d2f35673a85a4cd33fff658260224b68b205e..ff79f54ed05ee8d59a7bcfde9a1bff29538eef76 100644 (file)
--- a/helm/software/matita/matitaMathView.ml
+++ b/helm/software/matita/matitaMathView.ml
@@ -451,20 +451,22 @@ object (self)
     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
@@ -478,14 +480,17 @@ object (self)
     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));
@@ -615,11 +620,11 @@ class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () =
 
     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;
@@ -693,7 +698,8 @@ class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () =
       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;
@@ -898,10 +904,6 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
       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 _ _ ->
@@ -926,8 +928,12 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
         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 ());
 
@@ -1035,7 +1041,6 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
           | `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)) ->
@@ -1126,16 +1131,6 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
       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