X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2FmatitaMathView.ml;h=93a0b65eaa392b970abcf1d26108ffeb2b27c58f;hb=refs%2Fheads%2Fmaster;hp=ef7780f0c88a8b3993a2c6628007ed1e1d63d5b0;hpb=59ccad1f8e0f2da227dddbcd5214ade4744fd8ba;p=helm.git

diff --git a/matita/matita/matitaMathView.ml b/matita/matita/matitaMathView.ml
index ef7780f0c..93a0b65ea 100644
--- a/matita/matita/matitaMathView.ml
+++ b/matita/matita/matitaMathView.ml
@@ -27,9 +27,7 @@
 
 open Printf
 
-open GrafiteTypes
 open MatitaGtkMisc
-open MatitaGuiTypes
 open CicMathView
 
 module Stack = Continuationals.Stack
@@ -91,7 +89,7 @@ class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () =
           GtkSignal.disconnect notebook#as_widget id;
           switch_page_callback <- None
       | None -> ());
-      for i = 0 to pages do notebook#remove_page 0 done; 
+      for _i = 0 to pages do notebook#remove_page 0 done; 
       notebook#set_show_tabs true;
       pages <- 0;
       page2goal <- [];
@@ -99,7 +97,7 @@ class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () =
       goal2win <- [];
       _metasenv <- [],[]
 
-    method nload_sequents : 'status. #GrafiteTypes.status as 'status -> unit
+    method nload_sequents : 'status. (#GrafiteTypes.status as 'status) -> unit
     = fun (status : #GrafiteTypes.status) ->
      let _,_,metasenv,subst,_ = status#obj in
       _metasenv <- metasenv,subst;
@@ -112,12 +110,8 @@ class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () =
           scrolledWin <- Some w;
           (match cicMathView#misc#parent with
             | None -> ()
-            | Some parent ->
-               let parent =
-                match cicMathView#misc#parent with
-                   None -> assert false
-                 | Some p -> GContainer.cast_container p
-               in
+            | Some p ->
+               let parent = GContainer.cast_container p in
                 parent#remove cicMathView#coerce);
           w#add cicMathView#coerce
         in
@@ -128,8 +122,8 @@ class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () =
         let stack_goals = Stack.open_goals status#stack in
         let proof_goals = List.map fst metasenv in
         if
-          HExtlib.list_uniq (List.sort Pervasives.compare stack_goals)
-          <> List.sort Pervasives.compare proof_goals
+          HExtlib.list_uniq (List.sort compare stack_goals)
+          <> List.sort compare proof_goals
         then begin
           prerr_endline ("STACK GOALS = " ^ String.concat " " (List.map string_of_int stack_goals));
           prerr_endline ("PROOF GOALS = " ^ String.concat " " (List.map string_of_int proof_goals));
@@ -157,8 +151,8 @@ class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () =
         end
       in
       let add_switch _ _ (_, sw) = add_tab (render_switch sw) sw in
-      Stack.iter  (** populate notebook with tabs *)
-        ~env:(fun depth tag (pos, sw) ->
+      Stack.iter  (* populate notebook with tabs *)
+        ~env:(fun depth _tag (pos, sw) ->
           let markup =
             match depth, pos with
             | 0, 0 -> `Current (render_switch sw)
@@ -178,14 +172,14 @@ class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () =
           self#render_page status ~page ~goal_switch))
 
     method private render_page:
-     'status. #ApplyTransformation.status as 'status -> page:int ->
+     'status. (#ApplyTransformation.status as 'status) -> page:int ->
        goal_switch:Stack.switch -> unit
-     = fun status ~page ~goal_switch ->
+     = fun status ~page:_ ~goal_switch ->
       (match goal_switch with
       | Stack.Open goal ->
          let menv,subst = _metasenv in
           cicMathView#nload_sequent status menv subst goal
-      | Stack.Closed goal ->
+      | Stack.Closed _goal ->
           let root = Lazy.force closed_goal_mathml in
           cicMathView#load_root ~root);
       (try
@@ -210,7 +204,7 @@ class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () =
              (w#vadjustment#upper -. w#vadjustment#page_size));
       with Not_found -> assert false)
 
-    method goto_sequent: 'status. #ApplyTransformation.status as 'status -> int -> unit
+    method goto_sequent: 'status. (#ApplyTransformation.status as 'status) -> int -> unit
      = fun status goal ->
       let goal_switch, page =
         try
@@ -479,7 +473,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
       self#_showMath;
       mathView#load_root (Lazy.force empty_mathml)
 
-    method private _loadCheck term =
+    method private _loadCheck _term =
       failwith "not implemented _loadCheck";
 (*       self#_showMath *)
 
@@ -504,7 +498,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
          "the graph of dependencies amoung objects. Please install it.")
         ~parent:win#toplevel ()
 
-    method private dependencies direction uri () =
+    method private dependencies _direction _uri () =
       assert false (* MATITA 1.0
       let dbd = LibraryDb.instance () in
       let graph =
@@ -538,10 +532,10 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
           (Virtuals.get_all_eqclass ()));
       Printf.bprintf b "\n\nVirtual keys (trigger with ALT-L):\n\n";
       List.iter 
-        (fun tag, items -> 
+        (fun (tag, items) -> 
            Printf.bprintf b "  %s:\n" tag;
            List.iter 
-             (fun names, symbol ->
+             (fun (names, symbol) ->
                 Printf.bprintf b "  \t%s\t%s\n" 
                   (Glib.Utf8.from_unichar symbol)
                   (String.concat ", " names))
@@ -579,7 +573,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
       let content = Http_getter.ls ~local:false dir in
       let l =
         List.fast_sort
-          Pervasives.compare
+          compare
           (List.map
             (function 
               | Http_getter_types.Ls_section s -> "dir", s
@@ -728,7 +722,7 @@ let find_selection_owner () =
     | mv :: tl ->
         (match mv#get_selections with
         | [] -> aux tl
-        | sel :: _ -> mv)
+        | _sel :: _ -> mv)
   in
   aux (get_math_views ())