]> matita.cs.unibo.it Git - helm.git/commitdiff
*** empty log message ***
authorLuca Padovani <luca.padovani@unito.it>
Wed, 20 Dec 2000 13:39:13 +0000 (13:39 +0000)
committerLuca Padovani <luca.padovani@unito.it>
Wed, 20 Dec 2000 13:39:13 +0000 (13:39 +0000)
helm/DEVEL/lablgtk_gtkmathview/lablgtk-20000829_gtkmathview-0.2.1/gMathView.ml
helm/DEVEL/lablgtk_gtkmathview/lablgtk-20000829_gtkmathview-0.2.1/gtkMathView.ml
helm/DEVEL/lablgtk_gtkmathview/lablgtk-20000829_gtkmathview-0.2.1/minidom/Makefile
helm/DEVEL/lablgtk_gtkmathview/lablgtk-20000829_gtkmathview-0.2.1/minidom/ominidom.ml
helm/DEVEL/lablgtk_gtkmathview/lablgtk-20000829_gtkmathview-0.2.1/ml_gtk_mathview.c
helm/DEVEL/lablgtk_gtkmathview/lablgtk-20000829_gtkmathview-0.2.1/test/test.ml

index 9108b866d4b2ead341825f9bd30d08801a082ac4..951b8d46ccc8822861407c7b75e54af5a00cb3fe 100644 (file)
@@ -23,10 +23,8 @@ class math_view obj = object
  method load ~filename =
   if not (MathView.load obj ~filename) then raise (ErrorLoadingFile filename)
  method unload = MathView.unload obj
- method has_selection = MathView.has_selection obj
  method get_selection = MathView.get_selection obj
- method set_selection node = MathView.set_selection obj node
- method reset_selection = MathView.reset_selection obj
+ method set_selection (node : Ominidom.o_mDOMNode option) = MathView.set_selection obj node
  method get_width = MathView.get_width obj
  method get_height = MathView.get_height obj
  method get_top = MathView.get_top obj
@@ -47,16 +45,19 @@ class math_view obj = object
  method get_kerning = MathView.get_kerning obj
  method set_log_verbosity = MathView.set_log_verbosity obj
  method get_log_verbosity = MathView.get_log_verbosity obj
- method export_to_postscript ~width ~height ~x_margin ~y_margin ~disable_colors ~filename =
-  if not (MathView.export_to_postscript obj ~width ~height ~x_margin ~y_margin ~disable_colors ~filename) then
-   raise (ErrorWritingFile filename)
+ method export_to_postscript
+       ?(width = 595) ?(height = 822) ?(x_margin = 72) ?(y_margin = 72)
+       ?(disable_colors = false) ~filename () =
+  let result = MathView.export_to_postscript obj
+       ~width ~height ~x_margin ~y_margin ~disable_colors ~filename
+  in
+  if not result then raise (ErrorWritingFile filename)
  method get_font_manager_type = MathView.get_font_manager_type obj
  method set_font_manager_type ~fm_type = MathView.set_font_manager_type obj ~fm_type
 end
 
-let math_view ?adjustmenth ?adjustmentv ?border_width
- ?width ?height ?packing ?show ()
-=
+let math_view ?adjustmenth ?adjustmentv ?font_size ?font_manager ?border_width
+ ?width ?height ?packing ?show () =
  let w =
    MathView.create
     ?adjustmenth:(may_map ~f:GData.as_adjustment adjustmenth)
@@ -64,5 +65,15 @@ let math_view ?adjustmenth ?adjustmentv ?border_width
     ()
  in
   Container.set w ?border_width ?width ?height;
-  pack_return (new math_view w) ~packing ~show
+ let mathview = pack_return (new math_view w) ~packing ~show in
+ begin
+    match font_size with
+    | Some size -> mathview#set_font_size size
+    | None      -> ()
+  end;
+  begin
+    match font_manager with
+    | Some manager -> mathview#set_font_manager_type ~fm_type:manager
+    | None         -> ()
+  end;
 ;;
index 2bedc2f1a341c638ed55c8d4c69ad5816f122354..4c893fab407a8d984d17175c7b1ec3401ccc1974 100644 (file)
@@ -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
index 97ae32053b115e8301a80f5877d25c865fe86fb8..6fe73af6a3a311569826b4349e1c1ec01b529177 100644 (file)
@@ -20,6 +20,9 @@ minidom.cmo: minidom.ml minidom.cmi
 minidom.cmx: minidom.ml minidom.cmi
        ocamlopt -c $<
 
+ominidom.cmi: ominidom.mli
+       ocamlc -c $<
+
 ominidom.cmo: ominidom.ml
        ocamlc -c $<
 
index 2d8dcb17e97688fdaed2412857426298d6e35dff..85ad2e4eddd039f5a48087f22f689b8b1d00b9d0 100644 (file)
@@ -1,8 +1,14 @@
 
-exception Minidom_exception of string;;
+exception Node_has_no_parent;;
+exception Node_has_no_sibling of string;;
+exception Node_has_no_children;;
+exception Node_has_no_attributes;;
+exception Attribute_has_no_sibling of string;;
+exception Attribute_has_no_parent;;
+exception Undefined_entity;;
 
 let option_to_exception v e =
-  match (v) with
+  match v with
     Some x -> x
   | None   -> raise e
 ;;
@@ -16,20 +22,35 @@ class o_mDOMString (str: Minidom.mDOMString) =
 let o_mDOMString_of_string str =
   new o_mDOMString (Minidom.mDOMString_of_string str)
 
+class o_mDOMEntity (ent : Minidom.mDOMEntity) =
+  object
+    method get_dom_entity = ent
+    method get_content =
+      new o_mDOMString (Minidom.entity_get_content ent)
+  end
+;;
+
 class o_mDOMDoc (doc : Minidom.mDOMDoc) =
   object
     method get_dom_doc = doc
 
-    method get_root_node = Minidom.doc_get_root_node doc
-    method add_entity (name : o_mDOMString) =
-      Minidom.doc_add_entity doc (name#get_dom_string) 
+    method get_root_node =
+      new o_mDOMNode (Minidom.doc_get_root_node doc)
+    method add_entity (name : o_mDOMString) (value : o_mDOMString) =
+      new o_mDOMEntity
+        (Minidom.doc_add_entity doc
+         (name#get_dom_string) (value#get_dom_string)
+       )
     method get_entity (name : o_mDOMString) =
-      Minidom.doc_get_entity doc (name#get_dom_string)
+      match Minidom.doc_get_entity doc (name#get_dom_string) with
+      | Some x -> new o_mDOMEntity x
+      | None -> raise Undefined_entity
     method get_predefined_entity (name : o_mDOMString) =
-      Minidom.doc_get_predefined_entity doc (name#get_dom_string)
-  end;;
-
-class o_mDOMNode (node : Minidom.mDOMNode) =
+      match Minidom.doc_get_predefined_entity doc (name#get_dom_string) with
+      | Some x -> new o_mDOMEntity x
+      | None -> raise Undefined_entity
+  end
+and o_mDOMNode (node : Minidom.mDOMNode) =
   object
     method get_dom_node = node
 
@@ -40,70 +61,96 @@ class o_mDOMNode (node : Minidom.mDOMNode) =
 
     method get_type = Minidom.node_get_type node
     method get_name = 
-      new o_mDOMString
-        (option_to_exception (Minidom.node_get_name node) (Minidom_exception "node has no name"))
+      match Minidom.node_get_name node with
+      | Some x -> Some (new o_mDOMString x)
+      | None   -> None
     method get_ns_uri =
-      new o_mDOMString
-        (option_to_exception (Minidom.node_get_ns_uri node) (Minidom_exception "node has no associated namepsace"))
+      match Minidom.node_get_ns_uri node with
+      | Some x -> Some (new o_mDOMString x)
+      | None   -> None
     method get_attribute (name : o_mDOMString) =
-      new o_mDOMString
-        (option_to_exception
-         (Minidom.node_get_attribute node (name#get_dom_string))
-         (Minidom_exception "attribute not set for this node")
-       )
+      match Minidom.node_get_attribute node (name#get_dom_string) with
+      | Some x -> Some (new o_mDOMString x)
+      | None   -> None
     method get_attribute_ns (name : o_mDOMString) (uri : o_mDOMString) =
-      new o_mDOMString
-        (option_to_exception
-        (Minidom.node_get_attribute_ns node (name#get_dom_string) (uri#get_dom_string))
-        (Minidom_exception "attribute not set for this node")
-       )
+      match 
+        Minidom.node_get_attribute_ns node
+         (name#get_dom_string) (uri#get_dom_string)
+      with
+      | Some x -> Some (new o_mDOMString x)
+      | None   -> None
     method get_content =
-      new o_mDOMString
-        (option_to_exception (Minidom.node_get_content node) (Minidom_exception "node has no content"))
+      match Minidom.node_get_content node with
+      | Some x -> Some (new o_mDOMString x)
+      | None   -> None
     method get_parent =
       new o_mDOMNode
-       (option_to_exception (Minidom.node_get_parent node) (Minidom_exception "node has no parent"))
+       (option_to_exception (Minidom.node_get_parent node) Node_has_no_parent)
     method get_prev_sibling =
       new o_mDOMNode
-       (option_to_exception (Minidom.node_get_prev_sibling node) (Minidom_exception "node has no previous sibling"))
+       (option_to_exception
+        (Minidom.node_get_prev_sibling node)
+        (Node_has_no_sibling "left")
+       )
     method get_next_sibling =
       new o_mDOMNode
-       (option_to_exception (Minidom.node_get_next_sibling node) (Minidom_exception "node has no next sibling"))
+       (option_to_exception
+        (Minidom.node_get_next_sibling node)
+        (Node_has_no_sibling "right")
+       )
     method get_first_child =
       new o_mDOMNode
-       (option_to_exception (Minidom.node_get_first_child node) (Minidom_exception "node has no children"))
+       (option_to_exception
+        (Minidom.node_get_first_child node)
+        (Node_has_no_children)
+       )
     method get_first_attribute =
       new o_mDOMAttr
-       (option_to_exception (Minidom.node_get_first_attribute node) (Minidom_exception "node has no attributes"))
+       (option_to_exception
+         (Minidom.node_get_first_attribute node)
+         (Node_has_no_attributes)
+       )
     method is_first = Minidom.node_is_first node
     method is_last = Minidom.node_is_last node
 
-    method get_children = List.map (function x -> new o_mDOMNode x) (Minidom.node_get_children node)
-    method get_attributes = List.map (function x -> new o_mDOMAttr x) (Minidom.node_get_attributes node)
+    method get_children =
+      List.map (function x -> new o_mDOMNode x) (Minidom.node_get_children node)
+    method get_attributes = List.map
+      (function x -> new o_mDOMAttr x) (Minidom.node_get_attributes node)
   end
 and o_mDOMAttr (attr : Minidom.mDOMAttr) =
   object
     method get_dom_attr = attr
 
     method get_name =
-      new o_mDOMString
-        (option_to_exception (Minidom.attr_get_name attr) (Minidom_exception "attribute has no name"))
+      match Minidom.attr_get_name attr with
+      | Some x -> Some (new o_mDOMString x)
+      | None   -> None
     method get_ns_uri =
-      new o_mDOMString
-        (option_to_exception (Minidom.attr_get_ns_uri attr) (Minidom_exception "attribute has no associated namespace"))
+      match Minidom.attr_get_ns_uri attr with
+      | Some x -> Some (new o_mDOMString x)
+      | None   -> None
     method get_value =
-      new o_mDOMString
-        (option_to_exception (Minidom.attr_get_value attr) (Minidom_exception "attribute has no value"))
-
+      match Minidom.attr_get_value attr with
+      | Some x -> Some (new o_mDOMString x)
+      | None   -> None
     method get_prev_sibling =
       new o_mDOMAttr
-        (option_to_exception (Minidom.attr_get_prev_sibling attr) (Minidom_exception "attribute has no previous sibling"))
+        (option_to_exception
+         (Minidom.attr_get_prev_sibling attr)
+         (Attribute_has_no_sibling "left")
+       )
     method get_next_sibling =
       new o_mDOMAttr
-        (option_to_exception (Minidom.attr_get_next_sibling attr) (Minidom_exception "attribute has no next sibling"))
+        (option_to_exception
+         (Minidom.attr_get_next_sibling attr)
+         (Attribute_has_no_sibling "right")
+       )
     method get_parent =
       new o_mDOMNode
-        (option_to_exception (Minidom.attr_get_parent attr) (Minidom_exception "attribute has no parent"))
+        (option_to_exception
+         (Minidom.attr_get_parent attr) Attribute_has_no_parent
+       )
   end
 ;;
     
index 63ea13bf17a26735d22f56de79706fd3e26e513e..3c86f0057b806f22b2ac12883a2db9fdf37c10fb 100644 (file)
@@ -1,3 +1,4 @@
+#include <assert.h>
 #include <string.h>
 #include <assert.h>
 #include <gtk/gtk.h>
 #define FontManagerId_val(val) Int_val(val)
 #define Val_FontManagerId(val) Val_int(val)
 
+FontManagerId
+font_manager_id_of_value(value v)
+{
+  if (v == hash_variant("font_manager_gtk")) return FONT_MANAGER_GTK;
+  else if (v == hash_variant("font_manager_t1")) return FONT_MANAGER_T1;
+  else assert(0);
+}
+
+value
+value_of_font_manager_id(FontManagerId id)
+{
+  switch (id) {
+  case FONT_MANAGER_GTK:
+    return hash_variant("font_manager_gtk");
+  case FONT_MANAGER_T1:
+    return hash_variant("font_manager_t1");
+  default:
+    assert(0);
+    break;
+  }
+}
+
 ML_2 (gtk_math_view_new,GtkAdjustment_val, GtkAdjustment_val, Val_GtkWidget_sink)
 ML_2 (gtk_math_view_load, GtkMathView_val, String_val, Val_bool)
 ML_1 (gtk_math_view_unload, GtkMathView_val, Unit)
@@ -49,8 +72,8 @@ ML_2 (gtk_math_view_set_kerning, GtkMathView_val, Bool_val, Unit)
 ML_1 (gtk_math_view_get_kerning, GtkMathView_val, Val_bool)
 ML_2 (gtk_math_view_set_log_verbosity, GtkMathView_val, Int_val, Unit)
 ML_1 (gtk_math_view_get_log_verbosity, GtkMathView_val, Val_int)
-ML_2 (gtk_math_view_set_font_manager_type, GtkMathView_val, FontManagerId_val, Unit)
-ML_1 (gtk_math_view_get_font_manager_type, GtkMathView_val, Val_FontManagerId)
+ML_2 (gtk_math_view_set_font_manager_type, GtkMathView_val, font_manager_id_of_value, Unit)
+ML_1 (gtk_math_view_get_font_manager_type, GtkMathView_val, value_of_font_manager_id)
 
 value
 ml_gtk_math_view_export_to_postscript_native(value arg1,
index a8e184bc43e084888349e072253d73f981fb346b..dd66d3885d66d0ec2ab3f49e2a6979c4993b67a5 100644 (file)
 let jump (node : Ominidom.o_mDOMNode) =
  let module O = Ominidom in
   print_string ("jump: " ^
-   (try 
-      let href = node#get_attribute (O.o_mDOMString_of_string "href") in
-      href#get_string
-    with
-      O.Minidom_exception s -> "EXCEPTION: " ^ s
+   (match node#get_attribute (O.o_mDOMString_of_string "href") with
+    | Some x -> x#get_string
+    | None   -> "NO HREF FOR THIS NODE"
    ) ^ "\n");
   flush stdout
 ;;
@@ -23,17 +21,13 @@ let selection_changed mathview (node : Ominidom.o_mDOMNode option) =
  let module O = Ominidom in
   print_string ("selection_changed: " ^
    (match node with
-       None ->
-         mathview#reset_selection;
-         "selection_changed on nothing"
+       None -> "selection_changed on nothing"
      | Some node ->
-        try
-         mathview#set_selection node ;
-         let node_name = node#get_name in
-         node_name#get_string
-       with
-         O.Minidom_exception s -> "EXCEPTION: " ^ s
+       match node#get_name with
+       | Some x -> x#get_string
+       | None   -> "on element without name"
    ) ^ "\n");
+  mathview#set_selection node;
   flush stdout
 ;;
 
@@ -41,24 +35,22 @@ let selection_changed mathview (node : Ominidom.o_mDOMNode option) =
 let clicked (node : Ominidom.o_mDOMNode) =
  let module O = Ominidom in
   print_string ("clicked: " ^
-   (try
-      let node_name = node#get_name in
-      node_name#get_string
-    with
-      O.Minidom_exception s -> "EXCEPTION: " ^ s
+   (match node#get_name with
+    | Some x -> x#get_string
+    | None   -> "no name"
    ) ^ "\n");
   flush stdout
 ;;
 
 
 let activate_t1 mathview () =
- mathview#set_font_manager_type GtkMathView.MathView.FontManagerT1;
+ mathview#set_font_manager_type `font_manager_t1;
  print_string "WIDGET SET WITH T1 FONTS\n" ;
  flush stdout
 ;;
 
 let activate_gtk mathview () =
- mathview#set_font_manager_type GtkMathView.MathView.FontManagerGtk;
+ mathview#set_font_manager_type `font_manager_gtk;
  print_string "WIDGET SET WITH GTK FONTS\n" ;
  flush stdout
 ;;
@@ -67,8 +59,8 @@ let get_font_manager_type mathview () =
  print_string "CURRENT FONT MANAGER TYPE: ";
  begin
   match mathview#get_font_manager_type with
-  | GtkMathView.MathView.FontManagerT1 -> print_string "T1"
-  | GtkMathView.MathView.FontManagerGtk -> print_string "GTK"
+  | `font_manager_t1 -> print_string "T1"
+  | `font_manager_gtk -> print_string "GTK"
  end;
  print_newline();
  flush stdout
@@ -83,13 +75,14 @@ let load mathview () =
 let get_selection mathview () =
  let module O = Ominidom in
   let selection =
-   if not mathview#has_selection then "nothing"
-   else
-     let node = mathview#get_selection in
-     (try node#get_name#get_string
-      with
-        O.Minidom_exception s -> "EXCEPTION: " ^ s
-     ) 
+    match mathview#get_selection with
+    | Some node ->
+      begin
+        match node#get_name with
+       | Some name -> name#get_string
+       | None      -> "element with no name!"
+      end
+    | None      -> "no selection!"
   in
    print_string ("get_selection: " ^ selection ^ "\n") ;
    flush stdout
@@ -98,28 +91,23 @@ let get_selection mathview () =
 let set_selection mathview () =
  let module O = Ominidom in
   begin
-   try
-    let selected_node = mathview#get_selection in
-    try
-      let parent_node = selected_node#get_parent in
-      mathview#set_selection parent_node;
-      print_string "set selection: SEEMS TO WORK\n"
-    with
-      O.Minidom_exception s ->
-        print_string ("EXCEPTION: " ^ s ^ "\n")
-   with
-    GtkMathView.MathView.NoSelection ->
-     print_string "set_selection: YOU MUST PREVIOUSLY SELECT A NON-ROOT NODE\n" 
+    match mathview#get_selection with
+    | Some node -> 
+      begin
+        try 
+          let parent_node = node#get_parent in
+          mathview#set_selection (Some parent_node);
+          print_string "set selection: SEEMS TO WORK\n"
+       with
+         _ -> print_string "EXCEPTION: no parent\n"
+      end
+    | None ->
+      mathview#set_selection None;
+      print_string "no selection\n"
   end ;
   flush stdout
 ;;
 
-let reset_selection mathview () =
- mathview#reset_selection ;
- print_string "reset_selection: SEEMS TO WORK\n" ;
- flush stdout
-;;
-
 let unload mathview () =
  mathview#unload ;
  print_string "unload: SEEMS TO WORK\n" ;
@@ -237,8 +225,8 @@ let get_log_verbosity mathview () =
  flush stdout
 ;;
 
-let export_to_postscript mathview () =
- mathview#export_to_postscript 595 822 72 72 false "test.ps" ;
+let export_to_postscript (mathview : GMathView.math_view) () =
+ mathview#export_to_postscript ~filename:"test.ps" ();
  print_string "expor_to_postscript: SEEMS TO WORK (hint: look at test.ps)\n";
  flush stdout
 ;;
@@ -274,14 +262,12 @@ let button_get_log_verbosity = GButton.button ~label:"get_log_verbosity" ~packin
 let button_export_to_postscript = GButton.button ~label:"export_to_postscript" ~packing:(table#attach ~left:2 ~top:4) () in
 let button_t1 = GButton.button ~label:"activate T1 fonts" ~packing:(table#attach ~left:3 ~top:4) () in
 let button_get_font_manager_type = GButton.button ~label:"get_font_manager" ~packing:(table#attach ~left:4 ~top:4) () in
-let button_reset_selection = GButton.button ~label:"reset_selection" ~packing:(table#attach ~left:0 ~top:5) () in
 (* Signals connection *)
 ignore(button_gtk#connect#clicked (activate_gtk mathview)) ;
 ignore(button_load#connect#clicked (load mathview)) ;
 ignore(button_unload#connect#clicked (unload mathview)) ;
 ignore(button_get_selection#connect#clicked (get_selection mathview)) ;
 ignore(button_set_selection#connect#clicked (set_selection mathview)) ;
-ignore(button_reset_selection#connect#clicked (reset_selection mathview)) ;
 ignore(button_get_width#connect#clicked (get_width mathview)) ;
 ignore(button_get_height#connect#clicked (get_height mathview)) ;
 ignore(button_get_top#connect#clicked (get_top mathview)) ;