--- /dev/null
+*.cmi *.cmo *.cmx *.cma *.cmxa config.make
--- /dev/null
+gMathView.cmo: gtkMathView.cmo gtk_mathview.cmo
+gMathView.cmx: gtkMathView.cmx gtk_mathview.cmx
+gtkMathView.cmo: gtk_mathview.cmo
+gtkMathView.cmx: gtk_mathview.cmx
--- /dev/null
+This library is made available under the LGPL.
+You should have got a copy of the LGPL with Objective Caml.
+The LGPL applies to all the files in this directory, but not in
+subdirectories.
+
+For the test subdirectory, there is no specific licensing policy,
+but you may freely take inspiration from the code, and copy parts of
+it in your application.
+
+Author:
+ Claudio Sacerdoti Coen <sacerdot@cs.unibo.it>
--- /dev/null
+# Makefile for lablgtk_mathview.
+
+LABLGTKDIR = /usr/lib/ocaml/lablgtk
+MINIDOMDIR = ./minidom
+TESTDIR = ./test
+MLFLAGS += -I $(LABLGTKDIR) -I $(MINIDOMDIR)
+
+TARGETS = ml_gtk_mathview.o lablgtkmathview.cma
+
+all: Minidom $(TARGETS)
+
+opt: Minidom.opt lablgtkmathviewopt
+
+Minidom:
+ cd $(MINIDOMDIR); make
+
+Minidom.opt:
+ cd $(MINIDOMDIR); make opt
+
+configure:
+ @rm -f config.make
+ @$(MAKE) --no-print-directory -f configure.mk
+
+depend:
+ @rm -f .depend
+ @$(MAKE) --no-print-directory -f configure.mk .depend
+
+.depend config.make:
+ @$(MAKE) --no-print-directory -f configure.mk
+
+COMPILER = $(CAMLC) $(MLFLAGS) -w s -labels -c
+LINKER = $(CAMLC) $(MLFLAGS)
+COMPOPT = $(CAMLOPT) $(MLFLAGS) -w s -labels -c
+LINKOPT = $(CAMLOPT) $(MLFLAGS)
+
+include config.make
+
+INSTALLDIR = $(LIBDIR)/lablgtk/mathview
+
+MLLIBS = lablgtkmathview.cma
+CLIBS =
+MLLINK = unix.cma str.cma
+
+ifdef DEBUG
+CFLAGS = -g $(GTKCFLAGS)
+MLLINK += -cclib -lcamlrund
+MLFLAGS += -g
+else
+CFLAGS = -O -DGTK_NO_CHECK_CASTS -DGTK_DISABLE_COMPAT_H $(GTKCFLAGS)
+endif
+CFLAGS += $(MINIDOMCFLAGS) $(GTKMATHVIEWCFLAGS)
+
+THFLAGS = -thread
+THLINK = unix.cma threads.cma
+
+ifdef USE_CC
+CCOMPILER = $(CC) -c -I$(LIBDIR) $(CFLAGS)
+else
+CCOMPILER = ocamlc -c -ccopt "$(CFLAGS)"
+endif
+
+# Rules
+.SUFFIXES: .ml .mli .cmo .cmi .cmx .c .o .var .h .opt .def
+.c.o:
+ $(CCOMPILER) $<
+.ml.cmo:
+ $(COMPILER) $<
+.mli.cmi:
+ $(COMPILER) $<
+.ml.cmx:
+ $(COMPOPT) $<
+.var.h:
+ ./var2def < $< > $@
+.var.c:
+ ./var2conv < $< > $@
+
+# Targets
+COBJS = ml_gtk_mathview.o
+MLOBJS = gtk_mathview.cmo gtkMathView.cmo gMathView.cmo
+ALLOBJS = $(MLOBJS)
+
+lablgtkmathviewopt: $(CLIBS) $(MLLIBS:.cma=.cmxa)
+
+install:
+ if test -d $(INSTALLDIR); then : ; else mkdir -p $(INSTALLDIR); fi
+ cp $(ALLOBJS:.cmo=.cmi) $(INSTALLDIR)
+ if test -f *.mli ; then cp *.mli $(INSTALLDIR) ; fi
+ cp $(ALLOBJS:.cmo=.ml) $(INSTALLDIR)
+ cp $(MLLIBS) $(INSTALLDIR)
+ cp $(COBJS) $(INSTALLDIR)
+ if test ! -z "$(CLIBS)" ; then cp $(CLIBS) $(INSTALLDIR) ; fi
+ if test -f lablgtkmathview.cmxa; then \
+ cp $(MLLIBS:.cma=.cmxa) $(MLLIBS:.cma=.a) \
+ $(INSTALLDIR); fi
+
+lablgtkmathview.cma: $(MLOBJS)
+ $(LINKER) -a -custom -o $@ $(MLOBJS) $(GTKLIBS) -cclib "$(GTKMATHVIEWLIBS)" -cclib "$(MINIDOMLIBS)"
+lablgtkmathview.cmxa: $(MLOBJS:.cmo=.cmx)
+ $(LINKOPT) -a -o $@ $(MLOBJS:.cmo=.cmx) $(GTKLIBS) -cclib "$(GTKMATHVIEWLIBS)" -cclib "$(MINIDOMLIBS)"
+
+ml_gtk.o: $(LABLGTKDIR)/gtk_tags.c $(LABLGTKDIR)/gtk_tags.h \
+ $(LABLGTKDIR)/ml_gtk.h $(LABLGTKDIR)/ml_gdk.h $(LABLGTKDIR)/wrappers.h
+
+clean:
+ rm -f *.cm* *.o *.a *_tags.[ch] $(TARGETS)
+ cd $(MINIDOMDIR); make clean
+ cd $(TESTDIR); make clean
+
+include .depend
--- /dev/null
+# makefile for configuring lablGTK_mathview
+
+# Default compilers
+CAMLC = ocamlc
+CAMLOPT = ocamlopt
+
+# Default installation directories
+BINDIR = `$(GETBINDIR)`
+INSTALLDIR = $(LIBDIR)/lablgtk/mathview
+
+# Autoconf
+GETLIBDIR = ocamlc -v | grep "^Standard" | sed 's/^.*: *//'
+LIBDIR = `$(GETLIBDIR)`
+GETBINDIR = $(GETLIBDIR) | sed -e 's|/lib/[^/]*$$|/bin|' -e 's|/lib$$|/bin|'
+GETRANLIB = which ranlib 2>/dev/null | sed -e 's|.*/ranlib$$|!|' -e 's/^[^!]*$$/:/' -e 's/!/ranlib/'
+
+ifdef USE_GNOME
+GTKGETCFLAGS = gtk-config --cflags`" -I"`gnome-config --includedir
+GNOMELIBS = `gnome-config --libs gtkxmhtml`
+else
+GTKGETCFLAGS = gtk-config --cflags
+endif
+
+GTKGETLIBS = gtk-config --libs
+
+configure: .depend config.make
+
+.depend:
+ ocamldep *.ml *.mli > .depend
+
+config.make:
+ @echo CAMLC=$(CAMLC) > config.make
+ @echo CAMLOPT=$(CAMLOPT) >> config.make
+ @echo USE_GL=$(USE_GL) >> config.make
+ @echo USE_GNOME=$(USE_GNOME) >> config.make
+ @echo USE_CC=$(USE_CC) >> config.make
+ @echo DEBUG=$(DEBUG) >> config.make
+ @echo CC=$(CC) >> config.make
+ @echo RANLIB=`$(GETRANLIB)` >> config.make
+ @echo LIBDIR=$(LIBDIR) >> config.make
+ @echo BINDIR=`$(GETBINDIR)` >> config.make
+ @echo INSTALLDIR=$(INSTALLDIR) >> config.make
+# Luca: was
+# @echo GTKCFLAGS=`$(GTKGETCFLAGS)` -I/usr/lib/ocaml/lablgtk >> config.make
+# Luca: now
+ @echo GTKCFLAGS=`$(GTKGETCFLAGS)` -I$(LIBDIR)/lablgtk >> config.make
+ @echo GTKLIBS=`$(GTKGETLIBS)` | \
+ sed -e 's/-l/-cclib &/g' -e 's/-[LRWr][^ ]*/-ccopt &/g' \
+ >> config.make
+<<<<<<< configure.mk
+# Luca: GtkMathView configuration
+ @echo GTKMATHVIEWCFLAGS=`gtkmathview-config --cflags` >> config.make
+ @echo MINIDOMCFLAGS=`minidom-config --cflags` >> config.make
+ @echo GTKMATHVIEWLIBS=`gtkmathview-config --libs` >> config.make
+ @echo MINIDOMLIBS=`minidom-config --libs` >> config.make
+# Luca: end of GtkMathView configuration
+=======
+ #<CSC>
+ echo GTKMATHVIEWLIBS="-ccopt \""`gtkmathview-config --libs`"\"" >> config.make
+ #</CSC>
+>>>>>>> 1.2
+ @echo GNOMELIBS=$(GNOMELIBS) | \
+ sed -e 's/-l/-cclib &/g' -e 's/-[LRWr][^ ]*/-ccopt &/g' \
+ >> config.make
+ cat config.make
--- /dev/null
+open Gaux
+open Gtk
+open Gtk_mathview
+open GtkBase
+open GtkMathView
+open GObj
+
+exception ErrorLoadingFile of string;;
+exception ErrorWritingFile of string;;
+exception NoSelection;;
+
+class math_view_signals obj = object
+ inherit GContainer.container_signals obj
+ method clicked = GtkSignal.connect ~sgn:MathView.Signals.clicked obj ~after
+ method jump = GtkSignal.connect ~sgn:MathView.Signals.jump obj ~after
+ method selection_changed =
+ GtkSignal.connect ~sgn:MathView.Signals.selection_changed obj ~after
+end
+
+class math_view obj = object
+ inherit GContainer.container (obj : Gtk_mathview.math_view obj)
+ method connect = new math_view_signals obj
+ 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 get_width = MathView.get_width obj
+ method get_height = MathView.get_height obj
+ method get_top = MathView.get_top obj
+ method set_top = MathView.set_top obj
+ method set_adjustments =
+ fun adj1 adj2 ->
+ MathView.set_adjustments obj (GData.as_adjustment adj1)
+ (GData.as_adjustment adj2)
+ method get_hadjustment = new GData.adjustment (MathView.get_hadjustment obj)
+ method get_vadjustment = new GData.adjustment (MathView.get_vadjustment obj)
+ method get_buffer = MathView.get_buffer obj
+ method get_frame = new GBin.frame (MathView.get_frame obj)
+ method set_font_size = MathView.set_font_size obj
+ method get_font_size = MathView.get_font_size obj
+ method set_anti_aliasing = MathView.set_anti_aliasing obj
+ method get_anti_aliasing = MathView.get_anti_aliasing obj
+ method set_kerning = MathView.set_kerning obj
+ 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 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 w =
+ MathView.create
+ ?adjustmenth:(may_map ~f:GData.as_adjustment adjustmenth)
+ ?adjustmentv:(may_map ~f:GData.as_adjustment adjustmentv)
+ ()
+ in
+ Container.set w ?border_width ?width ?height;
+ pack_return (new math_view w) ~packing ~show
+;;
--- /dev/null
+open Gtk
+open Gtk_mathview
+open Tags
+open GtkBase
+open Gpointer
+
+external mDOMNode_of_boxed_option :
+ Gpointer.boxed option -> Minidom.mDOMNode =
+ "ml_gtk_math_view_mDOMNode_of_bodex_option"
+
+external mDOMNode_option_of_boxed_option :
+ Gpointer.boxed option -> Minidom.mDOMNode option =
+ "ml_gtk_math_view_mDOMNode_option_of_bodex_option"
+
+let o_mDOMNode_of_mDOMNode node = new Ominidom.o_mDOMNode node
+
+let o_mDOMNode_option_of_mDOMNode_option =
+ function
+ | Some x -> Some (o_mDOMNode_of_mDOMNode x)
+ | 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"
+ let create ~adjustmenth ~adjustmentv () =
+ create (optboxed adjustmenth) (optboxed adjustmentv)
+ external load : [>`math_view] obj -> filename:string -> bool =
+ "ml_gtk_math_view_load"
+ external unload : [>`math_view] obj -> unit =
+ "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
+ 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
+ external get_width : [>`math_view] obj -> int =
+ "ml_gtk_math_view_get_width"
+ external get_height : [>`math_view] obj -> int =
+ "ml_gtk_math_view_get_height"
+ external get_top : [>`math_view] obj -> (int * int) =
+ "ml_gtk_math_view_get_top"
+ external set_top : [>`math_view] obj -> int -> int -> unit =
+ "ml_gtk_math_view_set_top"
+ external set_adjustments : [>`math_view] obj -> Gtk.adjustment obj -> Gtk.adjustment obj -> unit =
+ "ml_gtk_math_view_set_adjustments"
+ external get_hadjustment : [>`math_view] obj -> Gtk.adjustment obj =
+ "ml_gtk_math_view_get_hadjustment"
+ external get_vadjustment : [>`math_view] obj -> Gtk.adjustment obj =
+ "ml_gtk_math_view_get_vadjustment"
+ external get_buffer : [>`math_view] obj -> Gdk.pixmap =
+ "ml_gtk_math_view_get_buffer"
+ external get_frame : [>`math_view] obj -> [`frame] obj =
+ "ml_gtk_math_view_get_frame"
+ external set_font_size : [>`math_view] obj -> int -> unit =
+ "ml_gtk_math_view_set_font_size"
+ external get_font_size : [>`math_view] obj -> int =
+ "ml_gtk_math_view_get_font_size"
+ external set_anti_aliasing : [>`math_view] obj -> bool -> unit =
+ "ml_gtk_math_view_set_anti_aliasing"
+ external get_anti_aliasing : [>`math_view] obj -> bool =
+ "ml_gtk_math_view_get_anti_aliasing"
+ external set_kerning : [>`math_view] obj -> bool -> unit =
+ "ml_gtk_math_view_set_kerning"
+ external get_kerning : [>`math_view] obj -> bool =
+ "ml_gtk_math_view_get_kerning"
+ external set_log_verbosity : [>`math_view] obj -> int -> unit =
+ "ml_gtk_math_view_set_log_verbosity"
+ 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 =
+ "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 =
+ "ml_gtk_math_view_get_font_manager_type"
+ external set_font_manager_type : [>`math_view] obj -> fm_type:font_manager_id -> unit =
+ "ml_gtk_math_view_set_font_manager_type"
+
+ module Signals = struct
+ open GtkSignal
+
+ let clicked : ([>`math_view],_) t =
+ let marshal_clicked f _ =
+ function
+ [GtkArgv.POINTER node] -> f (o_mDOMNode_of_mDOMNode (mDOMNode_of_boxed_option node))
+ | _ -> invalid_arg "GtkMathView.MathView.Signals.marshal_clicked"
+ in
+ { name = "clicked"; marshaller = marshal_clicked }
+
+ let jump : ([>`math_view],_) t =
+ let marshal_jump f _ =
+ function
+ [GtkArgv.POINTER node] -> f (o_mDOMNode_of_mDOMNode (mDOMNode_of_boxed_option node))
+ | _ -> invalid_arg "GtkMathView.MathView.Signals.marshal_jump"
+ in
+ { name = "jump"; marshaller = marshal_jump }
+
+ let selection_changed : ([>`math_view],_) t =
+ let marshal_selection_changed f _ =
+ function
+ [GtkArgv.POINTER node] -> f (o_mDOMNode_option_of_mDOMNode_option (mDOMNode_option_of_boxed_option node))
+ | _ -> invalid_arg "GtkMathView.MathView.Signals.marshal_selection_changed"
+ in
+ { name = "selection_changed"; marshaller = marshal_selection_changed }
+ end
+end
--- /dev/null
+type math_view = [`widget|`container|`bin|`eventbox|`math_view]
--- /dev/null
+*.cmi *.cmo *.cmx test test.opt
--- /dev/null
+LIBDIR = /usr/lib/ocaml
+INSTALLDIR = $(LIBDIR)/minidom
+OBJECTS = minidom.cmi minidom.cmo ml_minidom.o ominidom.cmo
+OBJECTS_OPT = minidom.cmx ominidom.cmx
+INST = minidom.o ominidom.o ml_minidom.h minidom.mli
+
+all: $(OBJECTS) test
+
+opt: $(OBJECTS_OPT) test.opt
+
+ml_minidom.o: ml_minidom.c
+ gcc -c -I/usr/lib/ocaml/caml/ `glib-config --cflags` `minidom-config --cflags` $<
+
+minidom.cmi: minidom.mli
+ ocamlc -c $<
+
+minidom.cmo: minidom.ml minidom.cmi
+ ocamlc -c $<
+
+minidom.cmx: minidom.ml minidom.cmi
+ ocamlopt -c $<
+
+ominidom.cmo: ominidom.ml
+ ocamlc -c $<
+
+ominidom.cmx: ominidom.ml
+ ocamlopt -c $<
+
+test.cmo: test.ml minidom.cmo
+ ocamlc -c test.ml
+
+test.cmx: test.ml minidom.cmx
+ ocamlopt -c test.ml
+
+test: test.cmo minidom.cmo ml_minidom.o
+ ocamlc -custom -o test minidom.cmo test.cmo ml_minidom.o \
+ -cclib "`glib-config --libs` `minidom-config --libs`"
+
+test.opt: test.cmx minidom.cmx ml_minidom.o
+ ocamlopt -o test.opt minidom.cmx test.cmx ml_minidom.o \
+ -cclib "`glib-config --libs` `minidom-config --libs`"
+
+install:
+ if test -d $(INSTALLDIR); then : ; else mkdir -p $(INSTALLDIR); fi
+ cp $(OBJECTS) $(OBJECTS_OPT) $(INSTALLDIR)
+
+clean:
+ rm -f *.o *.cm? test test.opt
--- /dev/null
+
+type mDOMString
+type mDOMDoc
+type mDOMNode
+type mDOMAttr
+type mDOMEntity
+
+external string_of_mDOMString : mDOMString -> string = "ml_string_of_mDOMString"
+external mDOMString_of_string : string -> mDOMString = "ml_mDOMString_of_string"
+external mDOMString_eq : string -> string -> bool = "ml_mDOMString_eq"
+
+external doc_load : string -> mDOMDoc = "ml_doc_load"
+external doc_unload : mDOMDoc -> unit = "ml_doc_unload"
+
+external doc_new : mDOMString -> mDOMDoc = "ml_doc_new"
+external doc_get_root_node : mDOMDoc -> mDOMNode = "ml_doc_get_root_node"
+
+external doc_add_entity : mDOMDoc -> mDOMString -> mDOMString -> mDOMEntity = "ml_doc_add_entity"
+external doc_get_entity : mDOMDoc -> mDOMString -> mDOMEntity option = "ml_doc_get_entity"
+external doc_get_predefined_entity : mDOMDoc -> mDOMString -> mDOMEntity option = "ml_doc_get_predefined_entity"
+external entity_get_content : mDOMEntity -> mDOMString = "ml_entity_get_content"
+
+external node_is_text : mDOMNode -> bool = "ml_node_is_text"
+external node_is_element : mDOMNode -> bool = "ml_node_is_element"
+external node_is_blank : mDOMNode -> bool = "ml_node_is_blank"
+external node_is_entity_ref : mDOMNode -> bool = "ml_node_is_entity_ref"
+external node_get_type : mDOMNode -> int = "ml_node_get_type"
+external node_get_name : mDOMNode -> mDOMString option = "ml_node_get_name"
+external node_get_ns_uri : mDOMNode -> mDOMString option = "ml_node_get_ns_uri"
+external node_get_attribute : mDOMNode -> mDOMString -> mDOMString option = "ml_node_get_attribute"
+external node_get_attribute_ns : mDOMNode -> mDOMString -> mDOMString -> mDOMString option = "ml_node_get_attribute_ns"
+external node_get_content : mDOMNode -> mDOMString option = "ml_node_get_content"
+external node_get_parent : mDOMNode -> mDOMNode option = "ml_node_get_parent"
+external node_get_prev_sibling : mDOMNode -> mDOMNode option = "ml_node_get_prev_sibling"
+external node_get_next_sibling : mDOMNode -> mDOMNode option = "ml_node_get_next_sibling"
+external node_get_first_child : mDOMNode -> mDOMNode option = "ml_node_get_first_child"
+external node_get_first_attribute : mDOMNode -> mDOMAttr option = "ml_node_get_first_attribute"
+external node_is_first : mDOMNode -> bool = "ml_node_is_first"
+external node_is_last : mDOMNode -> bool = "ml_node_is_last"
+
+external attr_get_name : mDOMAttr -> mDOMString option = "ml_attr_get_name"
+external attr_get_ns_uri : mDOMAttr -> mDOMString option = "ml_attr_get_ns_uri"
+external attr_get_value : mDOMAttr -> mDOMString option = "ml_attr_get_value"
+external attr_get_prev_sibling : mDOMAttr -> mDOMAttr option = "ml_attr_get_prev_sibling"
+external attr_get_next_sibling : mDOMAttr -> mDOMAttr option = "ml_attr_get_next_sibling"
+external attr_get_parent : mDOMAttr -> mDOMNode option = "ml_attr_get_parent"
+
+let rec node_list_of_node_first =
+ function None -> []
+ | Some node -> node :: (node_list_of_node_first (node_get_next_sibling node))
+
+let rec attr_list_of_attr_first =
+ function None -> []
+ | Some attr -> attr :: (attr_list_of_attr_first (attr_get_next_sibling attr))
+
+let node_get_children node =
+ (node_list_of_node_first (node_get_first_child node))
+
+let node_get_attributes node =
+ (attr_list_of_attr_first (node_get_first_attribute node))
+
--- /dev/null
+
+type mDOMString
+type mDOMDoc
+type mDOMNode
+type mDOMAttr
+type mDOMEntity
+
+external string_of_mDOMString : mDOMString -> string = "ml_string_of_mDOMString"
+external mDOMString_of_string : string -> mDOMString = "ml_mDOMString_of_string"
+external mDOMString_eq : string -> string -> bool = "ml_mDOMString_eq"
+
+external doc_load : string -> mDOMDoc = "ml_doc_load"
+external doc_unload : mDOMDoc -> unit = "ml_doc_unload"
+
+external doc_new : mDOMString -> mDOMDoc = "ml_doc_new"
+external doc_get_root_node : mDOMDoc -> mDOMNode = "ml_doc_get_root_node"
+
+external doc_add_entity : doc:mDOMDoc -> name:mDOMString -> content:mDOMString -> mDOMEntity = "ml_doc_add_entity"
+external doc_get_entity : doc:mDOMDoc -> name:mDOMString -> mDOMEntity option = "ml_doc_get_entity"
+external doc_get_predefined_entity : doc:mDOMDoc -> name:mDOMString -> mDOMEntity option = "ml_doc_get_predefined_entity"
+external entity_get_content : mDOMEntity -> mDOMString = "ml_entity_get_content"
+
+external node_is_text : mDOMNode -> bool = "ml_node_is_text"
+external node_is_element : mDOMNode -> bool = "ml_node_is_element"
+external node_is_blank : mDOMNode -> bool = "ml_node_is_blank"
+external node_is_entity_ref : mDOMNode -> bool = "ml_node_is_entity_ref"
+external node_get_type : mDOMNode -> int = "ml_node_get_type"
+external node_get_name : mDOMNode -> mDOMString option = "ml_node_get_name"
+external node_get_ns_uri : mDOMNode -> mDOMString option = "ml_node_get_ns_uri"
+external node_get_attribute : node:mDOMNode -> name:mDOMString -> mDOMString option = "ml_node_get_attribute"
+external node_get_attribute_ns : node:mDOMNode -> name:mDOMString -> ns_uri:mDOMString -> mDOMString option = "ml_node_get_attribute_ns"
+external node_get_content : mDOMNode -> mDOMString option = "ml_node_get_content"
+external node_get_parent : mDOMNode -> mDOMNode option = "ml_node_get_parent"
+external node_get_prev_sibling : mDOMNode -> mDOMNode option = "ml_node_get_prev_sibling"
+external node_get_next_sibling : mDOMNode -> mDOMNode option = "ml_node_get_next_sibling"
+external node_get_first_child : mDOMNode -> mDOMNode option = "ml_node_get_first_child"
+external node_get_first_attribute : mDOMNode -> mDOMAttr option = "ml_node_get_first_attribute"
+external node_is_first : mDOMNode -> bool = "ml_node_is_first"
+external node_is_last : mDOMNode -> bool = "ml_node_is_last"
+
+external attr_get_name : mDOMAttr -> mDOMString option = "ml_attr_get_name"
+external attr_get_ns_uri : mDOMAttr -> mDOMString option = "ml_attr_get_ns_uri"
+external attr_get_value : mDOMAttr -> mDOMString option = "ml_attr_get_value"
+external attr_get_prev_sibling : mDOMAttr -> mDOMAttr option = "ml_attr_get_prev_sibling"
+external attr_get_next_sibling : mDOMAttr -> mDOMAttr option = "ml_attr_get_next_sibling"
+external attr_get_parent : mDOMAttr -> mDOMNode option = "ml_attr_get_parent"
+
+val node_get_children : mDOMNode -> mDOMNode list
+val node_get_attributes : mDOMNode -> mDOMAttr list
+
--- /dev/null
+
+#include <assert.h>
+#include <mlvalues.h>
+#include <memory.h>
+
+#include "minidom.h"
+
+#define Val_ptr(p) ((value) (p))
+#define Val_option(p,f) ((p != NULL) ? ml_some(f(p)) : Val_unit)
+#define Val_mDOMString(s) (copy_string((char*) (s)))
+#define mDOMString_val(v) ((mDOMStringRef) String_val(v))
+
+static value
+ml_some(value v)
+{
+ CAMLparam1(v);
+ value ret = alloc_small(1,0);
+ Field(ret,0) = v;
+ CAMLreturn(ret);
+}
+
+value
+ml_string_of_mDOMString(value s)
+{
+ CAMLparam1(s);
+ CAMLreturn(s);
+}
+
+value
+ml_mDOMString_of_string(value s)
+{
+ CAMLparam1(s);
+ CAMLreturn(s);
+}
+
+value
+ml_doc_load(value file_name)
+{
+ mDOMDocRef doc_ref;
+
+ CAMLparam1(file_name);
+
+ doc_ref = mdom_load(String_val(file_name), FALSE, NULL);
+ if (doc_ref == NULL) failwith("minidom: could not load document");
+
+ CAMLreturn((value) doc_ref);
+}
+
+value
+ml_doc_unload(value doc)
+{
+ CAMLparam1(doc);
+
+ mdom_unload((mDOMDocRef) doc);
+
+ CAMLreturn(Val_unit);
+}
+
+value
+ml_doc_new(value s)
+{
+ mDOMDocRef doc_ref;
+
+ CAMLparam1(s);
+
+ doc_ref = mdom_doc_new(mDOMString_val(s));
+ if (doc_ref == NULL) failwith("minidom: could not create new document");
+
+ CAMLreturn((value) doc_ref);
+}
+
+
+value
+ml_doc_get_root_node(value doc)
+{
+ mDOMNodeRef root;
+
+ CAMLparam1(doc);
+ root = mdom_doc_get_root_node((mDOMDocRef) doc);
+ if (root == NULL) failwith("minidom: document has no root node!");
+
+ CAMLreturn((value) root);
+}
+
+value
+ml_doc_add_entity(value doc, value name, value content)
+{
+ mDOMEntityRef ent;
+
+ CAMLparam3(doc, name, content);
+ ent = mdom_doc_add_entity((mDOMDocRef) doc, mDOMString_val(name), mDOMString_val(content));
+ if (ent == NULL) failwith("minidom: could not add entity");
+
+ CAMLreturn((value) ent);
+}
+
+value
+ml_doc_get_entity(value doc, value name)
+{
+ mDOMEntityRef ent;
+
+ CAMLparam2(doc, name);
+ ent = mdom_doc_get_entity((mDOMDocRef) doc, mDOMString_val(name));
+
+ CAMLreturn(Val_option(ent, Val_ptr));
+}
+
+value
+ml_doc_get_predefined_entity(value name)
+{
+ mDOMEntityRef ent;
+
+ CAMLparam1(name);
+ ent = mdom_get_predefined_entity(mDOMString_val(name));
+
+ CAMLreturn(Val_option(ent, Val_ptr));
+}
+
+value
+ml_entity_get_content(value ent)
+{
+ CAMLparam1(ent);
+ CAMLreturn(Val_mDOMString(mdom_entity_get_content((mDOMEntityRef) ent)));
+}
+
+value
+ml_node_is_text(value node)
+{
+ CAMLparam1(node);
+ CAMLreturn(Val_bool(mdom_node_is_text((mDOMNodeRef) node)));
+}
+
+value
+ml_node_is_element(value node)
+{
+ CAMLparam1(node);
+ CAMLreturn(Val_bool(mdom_node_is_element((mDOMNodeRef) node)));
+}
+
+value
+ml_node_is_blank(value node)
+{
+ CAMLparam1(node);
+ CAMLreturn(Val_bool(mdom_node_is_blank((mDOMNodeRef) node)));
+}
+
+value
+ml_node_is_entity_ref(value node)
+{
+ CAMLparam1(node);
+ CAMLreturn(Val_bool(mdom_node_is_entity_ref((mDOMNodeRef) node)));
+}
+
+value
+ml_node_get_type(value node)
+{
+ CAMLparam1(node);
+ CAMLreturn(Val_int(mdom_node_get_type((mDOMNodeRef) node)));
+}
+
+value
+ml_node_get_name(value node)
+{
+ CAMLparam1(node);
+ CAMLreturn(Val_option(mdom_node_get_name((mDOMNodeRef) node), Val_mDOMString));
+}
+
+value
+ml_node_get_content(value node)
+{
+ CAMLparam1(node);
+ CAMLreturn(Val_option(mdom_node_get_content((mDOMNodeRef) node), Val_mDOMString));
+}
+
+value
+ml_node_get_ns_uri(value node)
+{
+ CAMLparam1(node);
+ CAMLreturn(Val_option(mdom_node_get_ns_uri((mDOMNodeRef) node), Val_mDOMString));
+}
+
+value
+ml_node_get_attribute(value node, value name)
+{
+ CAMLparam2(node,name);
+ CAMLreturn(Val_option(mdom_node_get_attribute((mDOMNodeRef) node, String_val(name)), Val_mDOMString));
+}
+
+value
+ml_node_get_attribute_ns(value node, value name, value ns_uri)
+{
+ CAMLparam2(node,name);
+ CAMLreturn(Val_option(mdom_node_get_attribute_ns((mDOMNodeRef) node,
+ String_val(name),
+ String_val(ns_uri)), Val_mDOMString));
+}
+
+value
+ml_node_get_parent(value node)
+{
+ CAMLparam1(node);
+ CAMLreturn(Val_option(mdom_node_get_parent((mDOMNodeRef) node), Val_ptr));
+}
+
+value
+ml_node_get_prev_sibling(value node)
+{
+ CAMLparam1(node);
+ CAMLreturn(Val_option(mdom_node_get_prev_sibling((mDOMNodeRef) node), Val_ptr));
+}
+
+value
+ml_node_get_next_sibling(value node)
+{
+ CAMLparam1(node);
+ CAMLreturn(Val_option(mdom_node_get_next_sibling((mDOMNodeRef) node), Val_ptr));
+}
+
+value
+ml_node_get_first_child(value node)
+{
+ CAMLparam1(node);
+ CAMLreturn(Val_option(mdom_node_get_first_child((mDOMNodeRef) node), Val_ptr));
+}
+
+value
+ml_node_get_first_attribute(value node)
+{
+ CAMLparam1(node);
+ CAMLreturn(Val_option(mdom_node_get_first_attribute((mDOMNodeRef) node), Val_ptr));
+}
+
+value
+ml_node_is_first(value node)
+{
+ CAMLparam1(node);
+ CAMLreturn(Val_bool(mdom_node_is_first((mDOMNodeRef) node)));
+}
+
+value
+ml_node_is_last(value node)
+{
+ CAMLparam1(node);
+ CAMLreturn(Val_bool(mdom_node_is_last((mDOMNodeRef) node)));
+}
+
+value
+ml_attr_get_name(value attr)
+{
+ CAMLparam1(attr);
+ CAMLreturn(Val_option(mdom_attr_get_name((mDOMAttrRef) attr), Val_mDOMString));
+}
+
+value
+ml_attr_get_ns_uri(value attr)
+{
+ CAMLparam1(attr);
+ CAMLreturn(Val_option(mdom_attr_get_ns_uri((mDOMAttrRef) attr), Val_mDOMString));
+}
+
+value
+ml_attr_get_value(value attr)
+{
+ CAMLparam1(attr);
+ CAMLreturn(Val_option(mdom_attr_get_value((mDOMAttrRef) attr), Val_mDOMString));
+}
+
+value
+ml_attr_get_prev_sibling(value attr)
+{
+ CAMLparam1(attr);
+ CAMLreturn(Val_option(mdom_attr_get_prev_sibling((mDOMAttrRef) attr), Val_ptr));
+}
+
+value
+ml_attr_get_next_sibling(value attr)
+{
+ CAMLparam1(attr);
+ CAMLreturn(Val_option(mdom_attr_get_next_sibling((mDOMAttrRef) attr), Val_ptr));
+}
+
+value
+ml_attr_get_parent(value attr)
+{
+ CAMLparam1(attr);
+ CAMLreturn(Val_option(mdom_attr_get_parent((mDOMAttrRef) attr), Val_ptr));
+}
+
--- /dev/null
+
+#ifndef ml_minidom_h
+#define ml_minidom_h
+
+#define Val_ptr(p) ((value) (p))
+#ifndef Val_option
+#define Val_option(p,f) ((p != NULL) ? ml_some(f(p)) : Val_unit)
+#endif /* Val_option */
+#define Val_mDOMString(s) (copy_string((char*) (s)))
+#define mDOMString_val(v) ((mDOMStringRef) String_val(v))
+#define mDOMNode_val(v) ((mDOMNodeRef) v)
+
+#define mDOMNode_option_mDOMNodeRef(p) (((p) != NULL) ? ml_some((value) (p)) : Val_unit)
+#define mDOMNodeRef_mDOMNode_option(v) ((v == Val_unit) ? NULL : (mDOMNodeRef)Field((v),0))
+#define Val_mDOMNodeRef(p) (mDOMNode_option_mDOMNodeRef(p))
+#define mDOMNodeRef_val(v) (mDOMNodeRef_mDOMNode_option(v))
+
+#endif /* ml_minidom_h */
--- /dev/null
+
+exception Minidom_exception of string;;
+
+let option_to_exception v e =
+ match (v) with
+ Some x -> x
+ | None -> raise e
+;;
+
+class o_mDOMString (str: Minidom.mDOMString) =
+ object
+ method get_dom_string = str
+ method get_string = Minidom.string_of_mDOMString str
+ end;;
+
+let o_mDOMString_of_string str =
+ new o_mDOMString (Minidom.mDOMString_of_string str)
+
+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) content =
+ Minidom.doc_add_entity doc (name#get_dom_string) content
+ method get_entity (name : o_mDOMString) =
+ Minidom.doc_get_entity doc (name#get_dom_string)
+ method get_predefined_entity (name : o_mDOMString) =
+ Minidom.doc_get_predefined_entity doc (name#get_dom_string)
+ end;;
+
+class o_mDOMNode (node : Minidom.mDOMNode) =
+ object
+ method get_dom_node = node
+
+ method is_text = Minidom.node_is_text node
+ method is_element = Minidom.node_is_element node
+ method is_blank = Minidom.node_is_blank node
+ method is_entity_ref = Minidom.node_is_entity_ref node
+
+ 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"))
+ method get_ns_uri =
+ new o_mDOMString
+ (option_to_exception (Minidom.node_get_ns_uri node) (Minidom_exception "node has no associated namepsace"))
+ 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")
+ )
+ 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")
+ )
+ method get_content =
+ new o_mDOMString
+ (option_to_exception (Minidom.node_get_content node) (Minidom_exception "node has no content"))
+ method get_parent =
+ new o_mDOMNode
+ (option_to_exception (Minidom.node_get_parent node) (Minidom_exception "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"))
+ method get_next_sibling =
+ new o_mDOMNode
+ (option_to_exception (Minidom.node_get_next_sibling node) (Minidom_exception "node has no next sibling"))
+ method get_first_child =
+ new o_mDOMNode
+ (option_to_exception (Minidom.node_get_first_child node) (Minidom_exception "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"))
+ 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)
+ 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"))
+ method get_ns_uri =
+ new o_mDOMString
+ (option_to_exception (Minidom.attr_get_ns_uri attr) (Minidom_exception "attribute has no associated namespace"))
+ method get_value =
+ new o_mDOMString
+ (option_to_exception (Minidom.attr_get_value attr) (Minidom_exception "attribute has no value"))
+
+ method get_prev_sibling =
+ new o_mDOMAttr
+ (option_to_exception (Minidom.attr_get_prev_sibling attr) (Minidom_exception "attribute has no previous sibling"))
+ method get_next_sibling =
+ new o_mDOMAttr
+ (option_to_exception (Minidom.attr_get_next_sibling attr) (Minidom_exception "attribute has no next sibling"))
+ method get_parent =
+ new o_mDOMNode
+ (option_to_exception (Minidom.attr_get_parent attr) (Minidom_exception "attribute has no parent"))
+ end
+;;
+
--- /dev/null
+
+let doc = Minidom.doc_load "test.xml"
+
+let root = Minidom.doc_get_root_node doc
+
+let check_attribute_ns attr =
+ Printf.printf "\n\n";
+ let ns_uri = Minidom.attr_get_ns_uri attr
+ and attr_name = Minidom.attr_get_name attr
+ and attr_value = Minidom.attr_get_value attr
+ and parent = Minidom.attr_get_parent attr
+ in
+ match parent,ns_uri,attr_name,attr_value with
+ Some parent_node,Some uri,Some attribute_name,Some attribute_value ->
+ let attr_value = Minidom.node_get_attribute_ns parent_node attribute_name uri
+ in begin
+ match attr_value with
+ Some attr1 ->
+ Printf.printf "found the attribute with ns %s (was %s)\n"
+ (Minidom.string_of_mDOMString attr1) (Minidom.string_of_mDOMString attribute_value)
+ | None ->
+ Printf.printf "attribute not found (uri was %s)!!!!\n" (Minidom.string_of_mDOMString uri)
+ end
+ | _ ->
+ Printf.printf "parent_node == NULL || uri == NULL || attribute_name == NULL || attribute_value == NULL\n"
+;;
+
+let print_attribute attr =
+ check_attribute_ns attr;
+ let ns_uri = Minidom.attr_get_ns_uri attr
+ in
+ begin
+ match ns_uri with
+ Some uri -> Printf.printf " %s:" (Minidom.string_of_mDOMString uri);
+ | None -> ()
+ end;
+ match ((Minidom.attr_get_name attr), (Minidom.attr_get_value attr)) with
+ (Some attr_name, Some attr_value) ->
+ Printf.printf " %s=\"%s\"" (Minidom.string_of_mDOMString attr_name) (Minidom.string_of_mDOMString attr_value)
+ | (Some attr_name, _) ->
+ Printf.printf " ??? attribute %s has no value !!!" (Minidom.string_of_mDOMString attr_name)
+ | (_,_) ->
+ Printf.printf " ??? very strange attribute !!!"
+;;
+
+let rec print_node n node =
+ if Minidom.node_is_blank node then ()
+ else if Minidom.node_is_element node then begin
+ match Minidom.node_get_name node with
+ Some node_name ->
+ begin
+ let children = Minidom.node_get_children node
+ and attributes = Minidom.node_get_attributes node
+ and ns_uri = Minidom.node_get_ns_uri node
+ and is_first,is_last = (Minidom.node_is_first node), (Minidom.node_is_last node)
+ in
+ for i = 1 to n do print_char ' ' done;
+ Printf.printf "<";
+ begin
+ match ns_uri with
+ Some uri -> Printf.printf "%s:" (Minidom.string_of_mDOMString uri)
+ | None -> ()
+ end;
+ Printf.printf "%s" (Minidom.string_of_mDOMString node_name);
+ List.iter print_attribute attributes;
+ Printf.printf ">\n";
+ List.iter (print_node (n + 2)) children;
+ for i = 1 to n do print_char ' ' done;
+ Printf.printf "</%s>\n" (Minidom.string_of_mDOMString node_name)
+ end
+ | None -> Printf.printf "??? this node has no name !!!\n"
+ end else if Minidom.node_is_text node then begin
+ match Minidom.node_get_content node with
+ Some node_content ->
+ for i = 1 to n do print_char ' ' done;
+ Printf.printf "%s\n" (Minidom.string_of_mDOMString node_content)
+ | None -> Printf.printf "??? this node has no content !!!\n"
+ end else begin
+ Printf.printf "don't know how to manage a node with type %d\n" (Minidom.node_get_type node)
+ end
+;;
+
+print_node 0 root;;
+
--- /dev/null
+<?xml version="1.0" encoding="iso-8859-1"?>
+<?cocoon-format type="text/xhtml"?>
+<m:math xmlns:helm="http://www.cs.unibo.it/helm" xmlns:m="http://www.w3.org/1998/Math/MathML">
+ <m:mtable helm:xref="i0" columnalign="left" equalrows="false" align="baseline 1">
+ <m:mtr>
+ <m:mtd>
+ <m:mrow>
+ <m:mtext>DEFINITION and_ind() OF TYPE</m:mtext>
+ </m:mrow>
+ </m:mtd>
+ </m:mtr>
+ <m:mtr>
+ <m:mtd>
+ <m:mrow>
+ <m:mphantom>
+ <m:mtext>__</m:mtext>
+ </m:mphantom>
+ <m:semantics xmlns:xlink="http://www.w3.org/1999/xlink">
+ <m:mrow helm:xref="i22">
+ <m:mtable columnalign="left" equalrows="false" align="baseline 1">
+ <m:mtr>
+ <m:mtd>
+ <m:mrow>
+ <m:mo stretchy="false">(</m:mo>
+ <m:mrow helm:xref="i23">
+ <m:mtable columnalign="left" equalrows="false" align="baseline 1">
+ <m:mtr>
+ <m:mtd>
+ <m:mo color="Blue">Π</m:mo>
+ <m:mi>A</m:mi>
+ <m:mo>:</m:mo>
+ <m:mrow helm:xref="i24">
+ <m:mo>Prop</m:mo>
+ </m:mrow>
+ </m:mtd>
+ </m:mtr>
+ <m:mtr>
+ <m:mtd>
+ <m:mrow>
+ <m:mo>.</m:mo>
+ <m:mrow helm:xref="i25">
+ <m:mtable columnalign="left" equalrows="false" align="baseline 1">
+ <m:mtr>
+ <m:mtd>
+ <m:mo color="Blue">Π</m:mo>
+ <m:mi>B</m:mi>
+ <m:mo>:</m:mo>
+ <m:mrow helm:xref="i26">
+ <m:mo>Prop</m:mo>
+ </m:mrow>
+ </m:mtd>
+ </m:mtr>
+ <m:mtr>
+ <m:mtd>
+ <m:mrow>
+ <m:mo>.</m:mo>
+ <m:mrow helm:xref="i27">
+ <m:mtable columnalign="left" equalrows="false" align="baseline 1">
+ <m:mtr>
+ <m:mtd>
+ <m:mo color="Blue">Π</m:mo>
+ <m:mi>P</m:mi>
+ <m:mo>:</m:mo>
+ <m:mrow helm:xref="i28">
+ <m:mo>Prop</m:mo>
+ </m:mrow>
+ </m:mtd>
+ </m:mtr>
+ <m:mtr>
+ <m:mtd>
+ <m:mrow>
+ <m:mo>.</m:mo>
+ <m:mrow helm:xref="i29">
+ <m:mtable columnalign="left" equalrows="false" align="baseline 1">
+ <m:mtr>
+ <m:mtd>
+ <m:mo color="Blue">Π</m:mo>
+ <m:mi>f</m:mi>
+ <m:mo>:</m:mo>
+ <m:mrow helm:xref="i30">
+ <m:mo stretchy="false">(</m:mo>
+ <m:mi helm:xref="i31">A</m:mi>
+ <m:mo color="Blue">→</m:mo>
+ <m:mrow helm:xref="i32">
+ <m:mo stretchy="false">(</m:mo>
+ <m:mi helm:xref="i33">B</m:mi>
+ <m:mo color="Blue">→</m:mo>
+ <m:mi helm:xref="i34">P</m:mi>
+ <m:mo stretchy="false">)</m:mo>
+ </m:mrow>
+ <m:mo stretchy="false">)</m:mo>
+ </m:mrow>
+ </m:mtd>
+ </m:mtr>
+ <m:mtr>
+ <m:mtd>
+ <m:mrow>
+ <m:mo>.</m:mo>
+ <m:mrow helm:xref="i35">
+ <m:mo color="Blue">Π</m:mo>
+ <m:mi>a</m:mi>
+ <m:mo>:</m:mo>
+ <m:mrow helm:xref="i36">
+ <m:mo stretchy="false">(</m:mo>
+ <m:mi xlink:href="cic:/coq/INIT/Logic/Conjunction/and.ind" helm:xref="i37">and</m:mi>
+ <m:mphantom>
+ <m:mtext>_</m:mtext>
+ </m:mphantom>
+ <m:mi helm:xref="i38">A</m:mi>
+ <m:mphantom>
+ <m:mtext>_</m:mtext>
+ </m:mphantom>
+ <m:mi helm:xref="i39">B</m:mi>
+ <m:mo stretchy="false">)</m:mo>
+ </m:mrow>
+ <m:mo>.</m:mo>
+ <m:mi helm:xref="i40">P</m:mi>
+ </m:mrow>
+ </m:mrow>
+ </m:mtd>
+ </m:mtr>
+ </m:mtable>
+ </m:mrow>
+ </m:mrow>
+ </m:mtd>
+ </m:mtr>
+ </m:mtable>
+ </m:mrow>
+ </m:mrow>
+ </m:mtd>
+ </m:mtr>
+ </m:mtable>
+ </m:mrow>
+ </m:mrow>
+ </m:mtd>
+ </m:mtr>
+ </m:mtable>
+ </m:mrow>
+ </m:mrow>
+ </m:mtd>
+ </m:mtr>
+ <m:mtr>
+ <m:mtd>
+ <m:mrow>
+ <m:mo color="#b03060">:></m:mo>
+ <m:mrow helm:xref="i41">
+ <m:mo>Prop</m:mo>
+ </m:mrow>
+ </m:mrow>
+ </m:mtd>
+ </m:mtr>
+ <m:mtr>
+ <m:mtd>
+ <m:mrow>
+ <m:mo stretchy="false">)</m:mo>
+ </m:mrow>
+ </m:mtd>
+ </m:mtr>
+ </m:mtable>
+ </m:mrow>
+ <m:annotation-xml encoding="MathML">
+ <m:apply helm:xref="i22">
+ <m:csymbol>cast</m:csymbol>
+ <m:apply helm:xref="i23">
+ <m:csymbol>prod</m:csymbol>
+ <m:bvar>
+ <m:ci>A</m:ci>
+ <m:type>
+ <m:apply helm:xref="i24">
+ <m:csymbol>Prop</m:csymbol>
+ </m:apply>
+ </m:type>
+ </m:bvar>
+ <m:apply helm:xref="i25">
+ <m:csymbol>prod</m:csymbol>
+ <m:bvar>
+ <m:ci>B</m:ci>
+ <m:type>
+ <m:apply helm:xref="i26">
+ <m:csymbol>Prop</m:csymbol>
+ </m:apply>
+ </m:type>
+ </m:bvar>
+ <m:apply helm:xref="i27">
+ <m:csymbol>prod</m:csymbol>
+ <m:bvar>
+ <m:ci>P</m:ci>
+ <m:type>
+ <m:apply helm:xref="i28">
+ <m:csymbol>Prop</m:csymbol>
+ </m:apply>
+ </m:type>
+ </m:bvar>
+ <m:apply helm:xref="i29">
+ <m:csymbol>prod</m:csymbol>
+ <m:bvar>
+ <m:ci>f</m:ci>
+ <m:type>
+ <m:apply helm:xref="i30">
+ <m:csymbol>arrow</m:csymbol>
+ <m:ci helm:xref="i31">A</m:ci>
+ <m:apply helm:xref="i32">
+ <m:csymbol>arrow</m:csymbol>
+ <m:ci helm:xref="i33">B</m:ci>
+ <m:ci helm:xref="i34">P</m:ci>
+ </m:apply>
+ </m:apply>
+ </m:type>
+ </m:bvar>
+ <m:apply helm:xref="i35">
+ <m:csymbol>prod</m:csymbol>
+ <m:bvar>
+ <m:ci>a</m:ci>
+ <m:type>
+ <m:apply helm:xref="i36">
+ <m:csymbol>app</m:csymbol>
+ <m:ci definitionURL="cic:/coq/INIT/Logic/Conjunction/and.ind" helm:xref="i37">and</m:ci>
+ <m:ci helm:xref="i38">A</m:ci>
+ <m:ci helm:xref="i39">B</m:ci>
+ </m:apply>
+ </m:type>
+ </m:bvar>
+ <m:ci helm:xref="i40">P</m:ci>
+ </m:apply>
+ </m:apply>
+ </m:apply>
+ </m:apply>
+ </m:apply>
+ <m:apply helm:xref="i41">
+ <m:csymbol>Prop</m:csymbol>
+ </m:apply>
+ </m:apply>
+ </m:annotation-xml>
+ </m:semantics>
+ </m:mrow>
+ </m:mtd>
+ </m:mtr>
+ <m:mtr>
+ <m:mtd>
+ <m:mrow>
+ <m:mtext>AS</m:mtext>
+ </m:mrow>
+ </m:mtd>
+ </m:mtr>
+ <m:mtr>
+ <m:mtd>
+ <m:mrow>
+ <m:mphantom>
+ <m:mtext>__</m:mtext>
+ </m:mphantom>
+ <m:semantics xmlns:xlink="http://www.w3.org/1999/xlink">
+ <m:mrow helm:xref="i1">
+ <m:mtable columnalign="left" equalrows="false" align="baseline 1">
+ <m:mtr>
+ <m:mtd>
+ <m:mo color="Red">λ</m:mo>
+ <m:mi>A</m:mi>
+ <m:mo>:</m:mo>
+ <m:mrow helm:xref="i2">
+ <m:mo>Prop</m:mo>
+ </m:mrow>
+ </m:mtd>
+ </m:mtr>
+ <m:mtr>
+ <m:mtd>
+ <m:mrow>
+ <m:mo>.</m:mo>
+ <m:mrow helm:xref="i3">
+ <m:mtable columnalign="left" equalrows="false" align="baseline 1">
+ <m:mtr>
+ <m:mtd>
+ <m:mo color="Red">λ</m:mo>
+ <m:mi>B</m:mi>
+ <m:mo>:</m:mo>
+ <m:mrow helm:xref="i4">
+ <m:mo>Prop</m:mo>
+ </m:mrow>
+ </m:mtd>
+ </m:mtr>
+ <m:mtr>
+ <m:mtd>
+ <m:mrow>
+ <m:mo>.</m:mo>
+ <m:mrow helm:xref="i5">
+ <m:mtable columnalign="left" equalrows="false" align="baseline 1">
+ <m:mtr>
+ <m:mtd>
+ <m:mo color="Red">λ</m:mo>
+ <m:mi>P</m:mi>
+ <m:mo>:</m:mo>
+ <m:mrow helm:xref="i6">
+ <m:mo>Prop</m:mo>
+ </m:mrow>
+ </m:mtd>
+ </m:mtr>
+ <m:mtr>
+ <m:mtd>
+ <m:mrow>
+ <m:mo>.</m:mo>
+ <m:mrow helm:xref="i7">
+ <m:mtable columnalign="left" equalrows="false" align="baseline 1">
+ <m:mtr>
+ <m:mtd>
+ <m:mo color="Red">λ</m:mo>
+ <m:mi>f</m:mi>
+ <m:mo>:</m:mo>
+ <m:mrow helm:xref="i8">
+ <m:mo stretchy="false">(</m:mo>
+ <m:mi helm:xref="i9">A</m:mi>
+ <m:mo color="Blue">→</m:mo>
+ <m:mrow helm:xref="i10">
+ <m:mo stretchy="false">(</m:mo>
+ <m:mi helm:xref="i11">B</m:mi>
+ <m:mo color="Blue">→</m:mo>
+ <m:mi helm:xref="i12">P</m:mi>
+ <m:mo stretchy="false">)</m:mo>
+ </m:mrow>
+ <m:mo stretchy="false">)</m:mo>
+ </m:mrow>
+ </m:mtd>
+ </m:mtr>
+ <m:mtr>
+ <m:mtd>
+ <m:mrow>
+ <m:mo>.</m:mo>
+ <m:mrow helm:xref="i13">
+ <m:mtable columnalign="left" equalrows="false" align="baseline 1">
+ <m:mtr>
+ <m:mtd>
+ <m:mo color="Red">λ</m:mo>
+ <m:mi>a</m:mi>
+ <m:mo>:</m:mo>
+ <m:mrow helm:xref="i14">
+ <m:mo stretchy="false">(</m:mo>
+ <m:mi xlink:href="cic:/coq/INIT/Logic/Conjunction/and.ind" helm:xref="i15">and</m:mi>
+ <m:mphantom>
+ <m:mtext>_</m:mtext>
+ </m:mphantom>
+ <m:mi helm:xref="i16">A</m:mi>
+ <m:mphantom>
+ <m:mtext>_</m:mtext>
+ </m:mphantom>
+ <m:mi helm:xref="i17">B</m:mi>
+ <m:mo stretchy="false">)</m:mo>
+ </m:mrow>
+ </m:mtd>
+ </m:mtr>
+ <m:mtr>
+ <m:mtd>
+ <m:mrow>
+ <m:mo>.</m:mo>
+ <m:mrow helm:xref="i18">
+ <m:mo><</m:mo>
+ <m:mi helm:xref="i19">P</m:mi>
+ <m:mo>></m:mo>
+ <m:mo>CASES</m:mo>
+ <m:mphantom>
+ <m:mtext>_</m:mtext>
+ </m:mphantom>
+ <m:mi helm:xref="i20">a</m:mi>
+ <m:mphantom>
+ <m:mtext>_</m:mtext>
+ </m:mphantom>
+ <m:mo>OF</m:mo>
+ <m:mrow>
+ <m:mo stretchy="false">(</m:mo>
+ <m:mi>conj</m:mi>
+ <m:mphantom>
+ <m:mtext>_</m:mtext>
+ </m:mphantom>
+ <m:mi>$1</m:mi>
+ <m:mphantom>
+ <m:mtext>_</m:mtext>
+ </m:mphantom>
+ <m:mi>$2</m:mi>
+ <m:mo stretchy="false">)</m:mo>
+ </m:mrow>
+ <m:mo color="Green">⇒</m:mo>
+ <m:mrow>
+ <m:mo stretchy="false">(</m:mo>
+ <m:mi helm:xref="i21">f</m:mi>
+ <m:mphantom>
+ <m:mtext>_</m:mtext>
+ </m:mphantom>
+ <m:mi>$1</m:mi>
+ <m:mphantom>
+ <m:mtext>_</m:mtext>
+ </m:mphantom>
+ <m:mi>$2</m:mi>
+ <m:mo stretchy="false">)</m:mo>
+ </m:mrow>
+ <m:mphantom>
+ <m:mtext>_</m:mtext>
+ </m:mphantom>
+ <m:mo>END</m:mo>
+ </m:mrow>
+ </m:mrow>
+ </m:mtd>
+ </m:mtr>
+ </m:mtable>
+ </m:mrow>
+ </m:mrow>
+ </m:mtd>
+ </m:mtr>
+ </m:mtable>
+ </m:mrow>
+ </m:mrow>
+ </m:mtd>
+ </m:mtr>
+ </m:mtable>
+ </m:mrow>
+ </m:mrow>
+ </m:mtd>
+ </m:mtr>
+ </m:mtable>
+ </m:mrow>
+ </m:mrow>
+ </m:mtd>
+ </m:mtr>
+ </m:mtable>
+ </m:mrow>
+ <m:annotation-xml encoding="MathML">
+ <m:lambda helm:xref="i1">
+ <m:bvar>
+ <m:ci>A</m:ci>
+ <m:type>
+ <m:apply helm:xref="i2">
+ <m:csymbol>Prop</m:csymbol>
+ </m:apply>
+ </m:type>
+ </m:bvar>
+ <m:lambda helm:xref="i3">
+ <m:bvar>
+ <m:ci>B</m:ci>
+ <m:type>
+ <m:apply helm:xref="i4">
+ <m:csymbol>Prop</m:csymbol>
+ </m:apply>
+ </m:type>
+ </m:bvar>
+ <m:lambda helm:xref="i5">
+ <m:bvar>
+ <m:ci>P</m:ci>
+ <m:type>
+ <m:apply helm:xref="i6">
+ <m:csymbol>Prop</m:csymbol>
+ </m:apply>
+ </m:type>
+ </m:bvar>
+ <m:lambda helm:xref="i7">
+ <m:bvar>
+ <m:ci>f</m:ci>
+ <m:type>
+ <m:apply helm:xref="i8">
+ <m:csymbol>arrow</m:csymbol>
+ <m:ci helm:xref="i9">A</m:ci>
+ <m:apply helm:xref="i10">
+ <m:csymbol>arrow</m:csymbol>
+ <m:ci helm:xref="i11">B</m:ci>
+ <m:ci helm:xref="i12">P</m:ci>
+ </m:apply>
+ </m:apply>
+ </m:type>
+ </m:bvar>
+ <m:lambda helm:xref="i13">
+ <m:bvar>
+ <m:ci>a</m:ci>
+ <m:type>
+ <m:apply helm:xref="i14">
+ <m:csymbol>app</m:csymbol>
+ <m:ci definitionURL="cic:/coq/INIT/Logic/Conjunction/and.ind" helm:xref="i15">and</m:ci>
+ <m:ci helm:xref="i16">A</m:ci>
+ <m:ci helm:xref="i17">B</m:ci>
+ </m:apply>
+ </m:type>
+ </m:bvar>
+ <m:apply helm:xref="i18">
+ <m:csymbol>mutcase</m:csymbol>
+ <m:ci helm:xref="i19">P</m:ci>
+ <m:ci helm:xref="i20">a</m:ci>
+ <m:apply>
+ <m:csymbol>app</m:csymbol>
+ <m:ci>conj</m:ci>
+ <m:ci>$1</m:ci>
+ <m:ci>$2</m:ci>
+ </m:apply>
+ <m:apply>
+ <m:csymbol>app</m:csymbol>
+ <m:ci helm:xref="i21">f</m:ci>
+ <m:ci>$1</m:ci>
+ <m:ci>$2</m:ci>
+ </m:apply>
+ </m:apply>
+ </m:lambda>
+ </m:lambda>
+ </m:lambda>
+ </m:lambda>
+ </m:lambda>
+ </m:annotation-xml>
+ </m:semantics>
+ </m:mrow>
+ </m:mtd>
+ </m:mtr>
+ </m:mtable>
+</m:math>
--- /dev/null
+#include <string.h>
+#include <assert.h>
+#include <gtk/gtk.h>
+#include <caml/mlvalues.h>
+#include <caml/alloc.h>
+#include <caml/memory.h>
+#include <caml/callback.h>
+#include <caml/fail.h>
+
+#include <gtkmathview/gtkmathview.h>
+#include <ml_gtk.h>
+
+#include <wrappers.h>
+#include <ml_glib.h>
+#include <ml_gdk.h>
+#include <ml_gtk.h>
+#include <gtk_tags.h>
+
+#include <minidom.h>
+#include "minidom/ml_minidom.h"
+
+/* <CSC/>: Next row should be put in a .h of lablgtk. */
+#define GtkAdjustment_val(val) check_cast(GTK_ADJUSTMENT,val)
+
+#define GtkMathView_val(val) check_cast(GTK_MATH_VIEW,val)
+
+#define FontManagerId_val(val) Int_val(val)
+#define Val_FontManagerId(val) Val_int(val)
+
+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)
+/*ML_1 (gtk_math_view_dump, GtkMathView_val, Unit)*/
+ML_1 (gtk_math_view_get_selection, GtkMathView_val, Val_mDOMNodeRef)
+ML_2 (gtk_math_view_set_selection, GtkMathView_val, mDOMNodeRef_val, Unit)
+ML_1 (gtk_math_view_get_width, GtkMathView_val, Val_int)
+ML_1 (gtk_math_view_get_height, GtkMathView_val, Val_int)
+ML_3 (gtk_math_view_set_top, GtkMathView_val, Int_val, Int_val, Unit)
+ML_3 (gtk_math_view_set_adjustments, GtkMathView_val, GtkAdjustment_val, GtkAdjustment_val, Unit)
+ML_1 (gtk_math_view_get_hadjustment, GtkMathView_val, Val_GtkWidget)
+ML_1 (gtk_math_view_get_vadjustment, GtkMathView_val, Val_GtkWidget)
+ML_1 (gtk_math_view_get_buffer, GtkMathView_val, Val_GdkPixmap)
+ML_1 (gtk_math_view_get_frame, GtkMathView_val, Val_GtkWidget)
+ML_2 (gtk_math_view_set_font_size, GtkMathView_val, Int_val, Unit)
+ML_1 (gtk_math_view_get_font_size, GtkMathView_val, Val_int)
+ML_2 (gtk_math_view_set_anti_aliasing, GtkMathView_val, Bool_val, Unit)
+ML_1 (gtk_math_view_get_anti_aliasing, GtkMathView_val, Val_bool)
+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)
+
+value
+ml_gtk_math_view_export_to_postscript_native(value arg1,
+ value w, value h, value x0, value y0, value disable_colors, value arg2)
+{
+ CAMLparam5(arg1,w,h,x0,y0);
+ CAMLxparam2(disable_colors, arg2);
+
+ char *filename;
+ FILE *fd;
+ int res;
+ filename = String_val (arg2);
+ if ((fd = fopen(filename, "w"))) {
+ gtk_math_view_export_to_postscript(GtkMathView_val (arg1),
+ Int_val(w), Int_val(h), Int_val(x0), Int_val(y0), Bool_val(disable_colors), fd);
+ fclose (fd);
+ res = 1;
+ } else {
+ fprintf(stderr, "Error opening file %s for writing\n", filename);
+ res = 0;
+ }
+ CAMLreturn (Val_bool(res));
+}
+
+value ml_gtk_math_view_export_to_postscript_bytecode (value* arg, int argn)
+{
+ return ml_gtk_math_view_export_to_postscript_native(arg[0], arg[1], arg[2], arg[3], arg[4], arg[5], arg[6]);
+}
+
+value ml_gtk_math_view_get_top (value arg1)
+{
+ CAMLparam1(arg1);
+ CAMLlocal1 (result);
+ int x, y;
+ gtk_math_view_get_top(GtkMathView_val (arg1), &x, &y);
+ result = alloc(2, 0);
+ Store_field(result, 0, Val_int(x));
+ Store_field(result, 0, Val_int(y));
+ CAMLreturn (result);
+}
+
+
+value ml_gtk_math_view_mDOMNode_of_bodex_option (value arg1)
+{
+ CAMLparam1(arg1);
+
+ mDOMNodeRef nr;
+ CAMLlocal1 (tmp);
+ CAMLlocal1 (optval);
+ CAMLlocal1 (res);
+
+ if (arg1==Val_int(0)) {
+ assert(0);
+ } else {
+ tmp = Field(arg1, 0);
+ nr = (mDOMNodeRef) Field(tmp, 1);
+ }
+ optval = Val_mDOMNodeRef(nr);
+ if (optval==Val_int(0)) {
+ assert(0);
+ } else {
+ res = Field(optval, 0);
+ }
+
+ CAMLreturn(res);
+}
+
+value ml_gtk_math_view_mDOMNode_option_of_bodex_option (value arg1)
+{
+ CAMLparam1(arg1);
+
+ mDOMNodeRef nr;
+ CAMLlocal1 (tmp);
+
+ if (arg1==Val_int(0)) {
+ nr=NULL;
+ } else {
+ tmp = Field(arg1, 0);
+ nr = (mDOMNodeRef) Field(tmp, 1);
+ }
+
+ CAMLreturn(Val_mDOMNodeRef(nr));
+}
--- /dev/null
+*.cmo *.cmi *.cmx t1lib.log test test.opt test.ps test.o
--- /dev/null
+LABLGTK_DIR = /usr/lib/ocaml/lablgtk
+LABLGTK_MATHVIEW_DIR = ..
+MINIDOM_DIR = ../minidom
+OCAMLC = ocamlc -I $(LABLGTK_DIR) -I $(LABLGTK_MATHVIEW_DIR) \
+ -I $(MINIDOM_DIR) -I mlmathview
+OCAMLOPT = ocamlopt -I $(LABLGTK_DIR) -I $(LABLGTK_MATHVIEW_DIR) \
+ -I $(MINIDOM_DIR) -I mlmathview
+
+all: test
+opt: test.opt
+
+test: test.cmo
+ $(OCAMLC) -custom -o test lablgtk.cma gtkInit.cmo \
+ $(MINIDOM_DIR)/minidom.cmo \
+ $(MINIDOM_DIR)/ominidom.cmo \
+ $(LABLGTK_MATHVIEW_DIR)/lablgtkmathview.cma \
+ -cclib "$(MINIDOM_DIR)/ml_minidom.o" \
+ test.cmo \
+ -cclib "-lstr -L/usr/lib -L/usr/X11R6/lib -lgtk -lgdk \
+ -rdynamic -lgmodule -lglib -ldl -lXi -lXext -lX11 -lm \
+ -L/usr/local/lib/gtkmathview -lgtkmathview \
+ $(LABLGTK_MATHVIEW_DIR)/ml_gtk_mathview.o"
+
+test.opt: test.cmx
+ $(OCAMLOPT) -o test.opt lablgtk.cmxa gtkInit.cmx \
+ $(MINIDOM_DIR)/minidom.cmx \
+ $(MINIDOM_DIR)/ominidom.cmx \
+ $(LABLGTK_MATHVIEW_DIR)/lablgtkmathview.cmxa \
+ -cclib "$(MINIDOM_DIR)/ml_minidom.o" \
+ test.cmx \
+ -cclib "-lstr -L/usr/lib -L/usr/X11R6/lib -lgtk -lgdk \
+ -rdynamic -lgmodule -lglib -ldl -lXi -lXext -lX11 -lm \
+ -L/usr/local/lib/gtkmathview -lgtkmathview \
+ $(LABLGTK_MATHVIEW_DIR)/ml_gtk_mathview.o"
+
+.SUFFIXES: .ml .mli .cmo .cmi .cmx
+.ml.cmo:
+ $(OCAMLC) -c $<
+.mli.cmi:
+ $(OCAMLC) -c $<
+.ml.cmx:
+ $(OCAMLOPT) -c $<
+
+clean:
+ rm -f *.cm[iox] *.o test test.opt t1lib.log test.ps
--- /dev/null
+ENCODING=.
+AFM=/usr/share/texmf/fonts/afm/
+TYPE1=/usr/share/texmf/fonts/type1/bluesky/cm/:/usr/X11R6/lib/X11/fonts/Type1/:.
--- /dev/null
+(******************************************************************************)
+(* Claudio Sacerdoti Coen <sacerdot@cs.unibo.it> *)
+(* 25/09/2000 *)
+(* *)
+(* This is a simple test for the OCaml (LablGtk indeed) binding of the *)
+(* MathView widget *)
+(******************************************************************************)
+
+(* Callbacks *)
+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
+ ) ^ "\n");
+ flush stdout
+;;
+
+let selection_changed mathview (node : Ominidom.o_mDOMNode option) =
+ let module O = Ominidom in
+ print_string ("selection_changed: " ^
+ (match node with
+ 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
+ ) ^ "\n");
+ flush stdout
+;;
+
+
+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
+ ) ^ "\n");
+ flush stdout
+;;
+
+
+let activate_t1 mathview () =
+ mathview#set_font_manager_type GtkMathView.MathView.FontManagerT1;
+ print_string "WIDGET SET WITH T1 FONTS\n" ;
+ flush stdout
+;;
+
+let activate_gtk mathview () =
+ mathview#set_font_manager_type GtkMathView.MathView.FontManagerGtk;
+ print_string "WIDGET SET WITH GTK FONTS\n" ;
+ flush stdout
+;;
+
+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"
+ end;
+ print_newline();
+ flush stdout
+;;
+
+let load mathview () =
+ mathview#load "test.xml" ;
+ print_string "load: SEEMS TO WORK\n" ;
+ flush stdout
+;;
+
+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
+ )
+ in
+ print_string ("get_selection: " ^ selection ^ "\n") ;
+ flush stdout
+;;
+
+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"
+ 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" ;
+ flush stdout
+;;
+
+let get_width mathview () =
+ print_string ("get_width: " ^ string_of_int (mathview#get_width) ^ "\n") ;
+ flush stdout
+;;
+
+let get_height mathview () =
+ print_string ("get_height: " ^ string_of_int (mathview#get_height) ^ "\n") ;
+ flush stdout
+;;
+
+let get_top mathview () =
+ let (x,y) = mathview#get_top in
+ print_string ("get_top: ("^ string_of_int x ^ "," ^ string_of_int y ^ ")\n") ;
+ flush stdout
+;;
+
+let set_top mathview () =
+ mathview#set_top 0 0;
+ print_string "set_top: SEEM TO WORK\n" ;
+ flush stdout
+;;
+
+let set_adjustments mathview () =
+ let adj1 = GData.adjustment () in
+ let adj2 = GData.adjustment () in
+ mathview#set_adjustments adj1 adj2 ;
+ adj1#set_value ((adj1#lower +. adj1#upper) /. 2.0) ;
+ adj2#set_value ((adj2#lower +. adj2#upper) /. 2.0) ;
+ print_string "set_adjustments: SEEM TO WORK\n" ;
+ flush stdout
+;;
+
+let get_hadjustment mathview () =
+ let adj = mathview#get_hadjustment in
+ adj#set_value ((adj#lower +. adj#upper) /. 2.0) ;
+ print_string "get_hadjustment: SEEM TO WORK\n" ;
+ flush stdout
+;;
+
+let get_vadjustment mathview () =
+ let adj = mathview#get_vadjustment in
+ adj#set_value ((adj#lower +. adj#upper) /. 2.0) ;
+ print_string "get_vadjustment: SEEM TO WORK\n" ;
+ flush stdout
+;;
+
+let get_buffer mathview () =
+ let buffer = mathview#get_buffer in
+ Gdk.Draw.rectangle buffer (Gdk.GC.create buffer) ~x:0 ~y:0
+ ~width:50 ~height:50 ~filled:true () ;
+ print_string "get_buffer: SEEMS TO WORK (hint: force the widget redrawing)\n";
+ flush stdout
+;;
+
+let get_frame mathview () =
+ let frame = mathview#get_frame in
+ frame#set_shadow_type `NONE ;
+ print_string "get_frame: SEEMS TO WORK\n" ;
+ flush stdout
+;;
+
+let set_font_size mathview () =
+ mathview#set_font_size 24 ;
+ print_string "set_font_size: FONT IS NOW 24\n" ;
+ flush stdout
+;;
+
+let get_font_size mathview () =
+ print_string ("get_font_size: " ^ string_of_int (mathview#get_font_size) ^ "\n") ;
+ flush stdout
+;;
+
+let set_anti_aliasing mathview () =
+ mathview#set_anti_aliasing true ;
+ print_string "set_anti_aliasing: ON\n" ;
+ flush stdout
+;;
+
+let get_anti_aliasing mathview () =
+ print_string ("get_anti_aliasing: " ^
+ (match mathview#get_anti_aliasing with true -> "ON" | false -> "OFF") ^
+ "\n") ;
+ flush stdout
+;;
+
+let set_kerning mathview () =
+ mathview#set_kerning true ;
+ print_string "set_kerning: ON\n" ;
+ flush stdout
+;;
+
+let get_kerning mathview () =
+ print_string ("get_kerning: " ^
+ (match mathview#get_kerning with true -> "ON" | false -> "OFF") ^
+ "\n") ;
+ flush stdout
+;;
+
+let set_log_verbosity mathview () =
+ mathview#set_log_verbosity 3 ;
+ print_string "set_log_verbosity: NOW IS 3\n" ;
+ flush stdout
+;;
+
+let get_log_verbosity mathview () =
+ print_string ("get_log_verbosity: " ^
+ string_of_int mathview#get_log_verbosity ^
+ "\n") ;
+ flush stdout
+;;
+
+let export_to_postscript mathview () =
+ mathview#export_to_postscript 595 822 72 72 false "test.ps" ;
+ print_string "expor_to_postscript: SEEMS TO WORK (hint: look at test.ps)\n";
+ flush stdout
+;;
+
+(* Widget creation *)
+let main_window = GWindow.window ~title:"GtkMathView test" () in
+let vbox = GPack.vbox ~packing:main_window#add () in
+let sw = GBin.scrolled_window ~width:50 ~height:50 ~packing:vbox#pack () in
+let mathview= GMathView.math_view ~packing:sw#add ~width:50 ~height:50 () in
+let table = GPack.table ~rows:6 ~columns:5 ~packing:vbox#pack () in
+let button_gtk=GButton.button ~label:"activate Gtk fonts" ~packing:(table#attach ~left:0 ~top:0) () in
+let button_load = GButton.button ~label:"load" ~packing:(table#attach ~left:1 ~top:0) () in
+let button_unload = GButton.button ~label:"unload" ~packing:(table#attach ~left:2 ~top:0) () in
+let button_get_selection = GButton.button ~label:"get_selection" ~packing:(table#attach ~left:3 ~top:0) () in
+let button_set_selection = GButton.button ~label:"set_selection" ~packing:(table#attach ~left:4 ~top:0) () in
+let button_get_width = GButton.button ~label:"get_width" ~packing:(table#attach ~left:0 ~top:1) () in
+let button_get_height = GButton.button ~label:"get_height" ~packing:(table#attach ~left:1 ~top:1) () in
+let button_get_top = GButton.button ~label:"get_top" ~packing:(table#attach ~left:2 ~top:1) () in
+let button_set_top = GButton.button ~label:"set_top" ~packing:(table#attach ~left:3 ~top:1) () in
+let button_set_adjustments = GButton.button ~label:"set_adjustments" ~packing:(table#attach ~left:4 ~top:1) () in
+let button_get_hadjustment = GButton.button ~label:"get_hadjustment" ~packing:(table#attach ~left:0 ~top:2) () in
+let button_get_vadjustment = GButton.button ~label:"get_vadjustment" ~packing:(table#attach ~left:1 ~top:2) () in
+let button_get_buffer = GButton.button ~label:"get_buffer" ~packing:(table#attach ~left:2 ~top:2) () in
+let button_get_frame = GButton.button ~label:"get_frame" ~packing:(table#attach ~left:3 ~top:2) () in
+let button_set_font_size = GButton.button ~label:"set_font_size" ~packing:(table#attach ~left:4 ~top:2) () in
+let button_get_font_size = GButton.button ~label:"get_font_size" ~packing:(table#attach ~left:0 ~top:3) () in
+let button_set_anti_aliasing = GButton.button ~label:"set_anti_aliasing" ~packing:(table#attach ~left:1 ~top:3) () in
+let button_get_anti_aliasing = GButton.button ~label:"get_anti_aliasing" ~packing:(table#attach ~left:2 ~top:3) () in
+let button_set_kerning = GButton.button ~label:"set_kerning" ~packing:(table#attach ~left:3 ~top:3) () in
+let button_get_kerning = GButton.button ~label:"get_kerning" ~packing:(table#attach ~left:4 ~top:3) () in
+let button_set_log_verbosity = GButton.button ~label:"set_log_verbosity" ~packing:(table#attach ~left:0 ~top:4) () in
+let button_get_log_verbosity = GButton.button ~label:"get_log_verbosity" ~packing:(table#attach ~left:1 ~top:4) () in
+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)) ;
+ignore(button_set_top#connect#clicked (set_top mathview)) ;
+ignore(button_set_adjustments#connect#clicked (set_adjustments mathview)) ;
+ignore(button_get_hadjustment#connect#clicked (get_hadjustment mathview)) ;
+ignore(button_get_vadjustment#connect#clicked (get_vadjustment mathview)) ;
+ignore(button_get_buffer#connect#clicked (get_buffer mathview)) ;
+ignore(button_get_frame#connect#clicked (get_frame mathview)) ;
+ignore(button_set_font_size#connect#clicked (set_font_size mathview)) ;
+ignore(button_get_font_size#connect#clicked (get_font_size mathview)) ;
+ignore(button_set_anti_aliasing#connect#clicked (set_anti_aliasing mathview)) ;
+ignore(button_get_anti_aliasing#connect#clicked (get_anti_aliasing mathview)) ;
+ignore(button_set_kerning#connect#clicked (set_kerning mathview)) ;
+ignore(button_get_kerning#connect#clicked (get_kerning mathview)) ;
+ignore(button_set_log_verbosity#connect#clicked (set_log_verbosity mathview)) ;
+ignore(button_get_log_verbosity#connect#clicked (get_log_verbosity mathview)) ;
+ignore(button_export_to_postscript#connect#clicked (export_to_postscript mathview)) ;
+ignore(button_t1#connect#clicked (activate_t1 mathview)) ;
+ignore(button_get_font_manager_type#connect#clicked (get_font_manager_type mathview)) ;
+ignore(mathview#connect#jump jump) ;
+ignore(mathview#connect#clicked clicked) ;
+ignore(mathview#connect#selection_changed (selection_changed mathview)) ;
+(* Main Loop *)
+main_window#show () ;
+GMain.Main.main ()
+;;
--- /dev/null
+<math display="block">
+ <mrow helm:xref="SELECTION OK">
+ <mo>∫</mo>
+ <mo>⁡</mo>
+ <mfrac>
+ <mrow>
+ <mrow>
+ <mi>a</mi>
+ <mo>⁢</mo>
+ <mi>x</mi>
+ </mrow>
+ <mo>+</mo>
+ <mi>b</mi>
+ </mrow>
+ <mrow>
+ <msup>
+ <mi>x</mi>
+ <mn>2</mn>
+ </msup>
+ <mo>+</mo>
+ <mrow>
+ <mi>p</mi>
+ <mo>⁢</mo>
+ <mi>x</mi>
+ </mrow>
+ <mo>+</mo>
+ <mi>q</mi>
+ </mrow>
+ </mfrac>
+ </mrow>
+ <mo fontstyle="italic">d</mo>
+ <mi>x</mi>
+ <mo>=</mo>
+ <mrow>
+ <mrow>
+ <mfrac><mi>a</mi><mn>2</mn></mfrac>
+ <mo>⁢</mo>
+ <mrow>
+ <mi>ln</mi>
+ <mo>⁡</mo>
+ <mrow>
+ <mo>(</mo>
+ <mrow>
+ <msup><mi>x</mi><mn>2</mn></msup>
+ <mo>+</mo>
+ <mrow>
+ <mi>p</mi>
+ <mo>⁢</mo>
+ <mi>x</mi>
+ </mrow>
+ <mo>+</mo>
+ <mi>q</mi>
+ </mrow>
+ <mo>)</mo>
+ </mrow>
+ </mrow>
+ </mrow>
+ <mo>+</mo>
+ <mrow>
+ <mfrac>
+ <mrow>
+ <mrow>
+ <mn>2</mn>
+ <mo>⁢</mo>
+ <mi>b</mi>
+ </mrow>
+ <mo>-</mo>
+ <mrow>
+ <mi>a</mi>
+ <mo>⁢</mo>
+ <mi>p</mi>
+ </mrow>
+ </mrow>
+ <msqrt>
+ <mrow>
+ <mrow>
+ <mn>4</mn>
+ <mo>⁢</mo>
+ <mi>q</mi>
+ </mrow>
+ <mo>-</mo>
+ <msup>
+ <mi>p</mi>
+ <mn>2</mn>
+ </msup>
+ </mrow>
+ </msqrt>
+ </mfrac>
+ <mo>⁢</mo>
+ <mrow>
+ <mi xlink:href="JUMPS WORK">arctg</mi>
+ <mo>⁡</mo>
+ <mfrac>
+ <mrow>
+ <mrow>
+ <mn>2</mn>
+ <mo>⁢</mo>
+ <mi>x</mi>
+ </mrow>
+ <mo>+</mo>
+ <mi>p</mi>
+ </mrow>
+ <msqrt>
+ <mrow>
+ <mrow>
+ <mn>4</mn>
+ <mo>⁢</mo>
+ <mi>q</mi>
+ </mrow>
+ <mo>-</mo>
+ <msup>
+ <mi>p</mi>
+ <mn>2</mn>
+ </msup>
+ </mrow>
+ </msqrt>
+ </mfrac>
+ </mrow>
+ </mrow>
+ <mo>+</mo>
+ <mi>c</mi>
+ </mrow>
+</math>
projects / helm.git / commitdiff