Porting to ocaml 5

[helm.git] / matita / matita / cicMathView.ml

diff --git a/matita/matita/cicMathView.ml b/matita/matita/cicMathView.ml
index e06e0055d6da93d8ea9531fceca880048f5d3609..8f6bd620423c8dce67bfeec6db229cbf2dbe2d23 100644 (file)
--- a/matita/matita/cicMathView.ml
+++ b/matita/matita/cicMathView.ml
@@ -25,10 +25,8 @@
 
 open Printf
 
-open GrafiteTypes
-open MatitaGtkMisc
 open MatitaGuiTypes
-open GtkSourceView2
+open GtkSourceView3
 
 let matita_script_current = ref (fun _ -> (assert false : < advance: ?statement:string -> unit -> unit; status: GrafiteTypes.status >));;
 let register_matita_script_current f = matita_script_current := f;;
@@ -174,9 +172,9 @@ let string_of_dom_node node =
 *)
 
 class clickableMathView obj =
-let text_width = 80 in
+(*let text_width = 80 in*)
 object (self)
-  inherit GSourceView2.source_view obj
+  inherit GSourceView3.source_view obj
 
   method strings_of_selection = (assert false : (paste_kind * string) list)
 
@@ -197,7 +195,7 @@ object (self)
     self#buffer#apply_tag all_tag ~start:(self#buffer#get_iter `START)
      ~stop:(self#buffer#get_iter `END);
     ignore(all_tag#connect#event
-      ~callback:(fun ~origin event pos ->
+      ~callback:(fun ~origin:_ event _pos ->
         match GdkEvent.get_type event with
          | `MOTION_NOTIFY -> 
              Gdk.Window.set_cursor
@@ -209,12 +207,12 @@ object (self)
          | _ -> false));
      let hyperlink_tag = self#buffer#create_tag [] in
      ignore(hyperlink_tag#connect#event
-       ~callback:(fun ~origin event pos ->
+       ~callback:(fun ~origin:_ event pos ->
          let offset = (new GText.iter pos)#offset in
          let _,_,href =
           try
            List.find
-            (fun (start,stop,href) -> start <= offset && offset <= stop
+            (fun (start,stop,_href) -> start <= offset && offset <= stop
             ) hyperlinks
           with
            Not_found -> assert false
@@ -235,7 +233,7 @@ object (self)
               false
           | _ -> false));
      List.iter
-      ( fun (start,stop,(href : string)) ->
+      ( fun (start,stop,(_href : string)) ->
           self#buffer#apply_tag hyperlink_tag
            ~start:(self#buffer#get_iter_at_char start)
            ~stop:(self#buffer#get_iter_at_char (stop+1));
@@ -639,7 +637,7 @@ object (self)
   val mutable current_mathml = None
 
   method nload_sequent:
-   'status. #ApplyTransformation.status as 'status -> NCic.metasenv ->
+   'status. (#ApplyTransformation.status as 'status) -> NCic.metasenv ->
      NCic.substitution -> int -> unit
    = fun status metasenv subst metano ->
     let sequent = List.assoc metano metasenv in
@@ -656,7 +654,7 @@ object (self)
     self#load_root ~root:txt
 
   method load_nobject :
-   'status. #ApplyTransformation.status as 'status -> NCic.obj -> unit
+   'status. (#ApplyTransformation.status as 'status) -> NCic.obj -> unit
    = fun status obj ->
     let txt = ApplyTransformation.ntxt_of_cic_object ~map_unicode_to_tex:false
     80 status obj in
@@ -677,7 +675,7 @@ object (self)
           ignore (domImpl#saveDocumentToFile ~name ~doc:mathml ())
         end;*)
         self#load_root ~root:txt;
-        (*current_mathml <- Some mathml*)(*)*);
+        (*current_mathml <- Some mathml*)(* ) *);
 end
 
  (** constructors *)
@@ -688,9 +686,9 @@ let cicMathView (*?auto_indent ?highlight_current_line ?indent_on_tab ?indent_wi
       GContainer.pack_container ~create:(fun pl ->
         let obj = SourceView.new_ () in
         Gobject.set_params (Gobject.try_cast obj "GtkSourceView") pl;
-        new _cicMathView obj)(*)) ?auto_indent ?highlight_current_line ?indent_on_tab ?indent_width ?insert_spaces_instead_of_tabs ?right_margin_position ?show_line_marks ?show_line_numbers ?show_right_margin ?smart_home_end ?tab_width ?editable ?cursor_visible ?justification ?wrap_mode ?accepts_tab ?border_width*) [] ?width ?height ?packing ?show () :> cicMathView)
+        new _cicMathView obj)(* )) ?auto_indent ?highlight_current_line ?indent_on_tab ?indent_width ?insert_spaces_instead_of_tabs ?right_margin_position ?show_line_marks ?show_line_numbers ?show_right_margin ?smart_home_end ?tab_width ?editable ?cursor_visible ?justification ?wrap_mode ?accepts_tab ?border_width*) [] ?width ?height ?packing ?show () :> cicMathView)
 
-let screenshot status sequents metasenv subst (filename as ofn) =
+let screenshot _status _sequents _metasenv _subst (_filename (*as ofn*)) =
  () (*MATITA 1.0
   let w = GWindow.window ~title:"screenshot" () in
   let width = 500 in