X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FDEVEL%2Flablgtk_gtkmathview%2Flablgtk-20000829_gtkmathview-0.2.1%2FgtkMathView.ml;h=4c893fab407a8d984d17175c7b1ec3401ccc1974;hb=1c7fb836e2af4f2f3d18afd0396701f2094265ff;hp=2bedc2f1a341c638ed55c8d4c69ad5816f122354;hpb=378d6138523fcbfdb2d6b3ef0acad648ca17ff26;p=helm.git

diff --git a/helm/DEVEL/lablgtk_gtkmathview/lablgtk-20000829_gtkmathview-0.2.1/gtkMathView.ml b/helm/DEVEL/lablgtk_gtkmathview/lablgtk-20000829_gtkmathview-0.2.1/gtkMathView.ml
index 2bedc2f1a..4c893fab4 100644
--- a/helm/DEVEL/lablgtk_gtkmathview/lablgtk-20000829_gtkmathview-0.2.1/gtkMathView.ml
+++ b/helm/DEVEL/lablgtk_gtkmathview/lablgtk-20000829_gtkmathview-0.2.1/gtkMathView.ml
@@ -19,11 +19,14 @@ let o_mDOMNode_option_of_mDOMNode_option =
   | Some x -> Some (o_mDOMNode_of_mDOMNode x)
   | None   -> None
 
+let mDOMNode_option_of_o_mDOMNode_option =
+  function
+  | Some x -> Some (x#get_dom_node)
+  | None   -> None
+
 module MathView = struct
   exception NoSelection
 
-  type font_manager_id = FontManagerGtk | FontManagerT1
-  
   let cast w : math_view obj = Object.try_cast w "GtkMathView"
   external create : Gtk.adjustment optobj -> Gtk.adjustment optobj -> 
    math_view obj = "ml_gtk_math_view_new"
@@ -35,18 +38,12 @@ module MathView = struct
    "ml_gtk_math_view_unload"
   external raw_get_selection : [>`math_view] obj -> Minidom.mDOMNode option =
    "ml_gtk_math_view_get_selection"
-  let has_selection obj =
-    match raw_get_selection obj with
-    | None -> false
-    | _ -> true
   let get_selection obj =
-    match raw_get_selection obj with
-    | Some x -> o_mDOMNode_of_mDOMNode x
-    | None -> raise NoSelection
+   o_mDOMNode_option_of_mDOMNode_option (raw_get_selection obj)
   external raw_set_selection : [>`math_view] obj -> Minidom.mDOMNode option -> unit=
    "ml_gtk_math_view_set_selection"
-  let set_selection obj (node : Ominidom.o_mDOMNode) = raw_set_selection obj (Some (node#get_dom_node))
-  let reset_selection obj = raw_set_selection obj None
+  let set_selection obj node =
+   raw_set_selection obj (mDOMNode_option_of_o_mDOMNode_option node)
   external get_width : [>`math_view] obj -> int =
    "ml_gtk_math_view_get_width"
   external get_height : [>`math_view] obj -> int =
@@ -82,12 +79,13 @@ module MathView = struct
   external get_log_verbosity : [>`math_view] obj -> int =
    "ml_gtk_math_view_get_log_verbosity"
   external export_to_postscript :
-   [>`math_view] obj -> width:int -> height:int -> x_margin:int -> y_margin:int -> disable_colors:bool
-   -> filename:string -> bool =
+   [>`math_view] obj -> width:int -> height:int -> x_margin:int -> y_margin:int -> disable_colors:bool -> filename:string -> bool =
    "ml_gtk_math_view_export_to_postscript_bytecode" "ml_gtk_math_view_export_to_postscript_native"
-  external get_font_manager_type : [>`math_view] obj -> font_manager_id =
+  external get_font_manager_type : [>`math_view] obj ->
+   [`font_manager_gtk | `font_manager_t1] =
    "ml_gtk_math_view_get_font_manager_type"
-  external set_font_manager_type : [>`math_view] obj -> fm_type:font_manager_id -> unit =
+  external set_font_manager_type : [>`math_view] obj ->
+    fm_type:[`font_manager_gtk | `font_manager_t1] -> unit =
    "ml_gtk_math_view_set_font_manager_type"
   
   module Signals = struct