X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FDEVEL%2Flablgtk%2Flablgtk_20001129-0.1.0%2FglGtk.ml;fp=helm%2FDEVEL%2Flablgtk%2Flablgtk_20001129-0.1.0%2FglGtk.ml;h=0000000000000000000000000000000000000000;hb=869549224eef6278a48c16ae27dd786376082b38;hp=c7020a4fd71a92cb0244de07f7b18fa5cfeffa84;hpb=89262281b6e83bd2321150f81f1a0583645eb0c8;p=helm.git

diff --git a/helm/DEVEL/lablgtk/lablgtk_20001129-0.1.0/glGtk.ml b/helm/DEVEL/lablgtk/lablgtk_20001129-0.1.0/glGtk.ml
deleted file mode 100644
index c7020a4fd..000000000
--- a/helm/DEVEL/lablgtk/lablgtk_20001129-0.1.0/glGtk.ml
+++ /dev/null
@@ -1,86 +0,0 @@
-(* $Id$ *)
-
-open Gaux
-open Gtk
-
-type visual_options = [
-  | `USE_GL
-  | `BUFFER_SIZE of int
-  | `LEVEL of int
-  | `RGBA
-  | `DOUBLEBUFFER
-  | `STEREO
-  | `AUX_BUFFERS of int
-  | `RED_SIZE of int
-  | `GREEN_SIZE of int
-  | `BLUE_SIZE of int
-  | `ALPHA_SIZE of int
-  | `DEPTH_SIZE of int
-  | `STENCIL_SIZE of int
-  | `ACCUM_GREEN_SIZE of int
-  | `ACCUM_ALPHA_SIZE of int
-]
-
-type gl_area = [`widget|`drawing|`glarea]
-
-module Raw = struct
-  external create :
-    visual_options list -> share:[>`glarea] optobj -> gl_area obj
-    = "ml_gtk_gl_area_new"
-
-  external swap_buffers : [>`glarea] obj -> unit
-    = "ml_gtk_gl_area_swapbuffers"
-
-  external make_current : [>`glarea] obj -> bool
-    = "ml_gtk_gl_area_make_current"
-end
-
-class area_signals obj =
-object (connect)
-  inherit GObj.widget_signals obj
-  method display ~callback =
-    (new GObj.event_signals ~after obj)#expose ~callback:
-      begin fun ev ->
-	if GdkEvent.Expose.count ev = 0 then
-	  if Raw.make_current obj then callback ()
-	  else prerr_endline "GlGtk-WARNING **: could not make current";
-	true
-      end
-  method reshape ~callback =
-    (new GObj.event_signals ~after obj)#configure ~callback:
-      begin fun ev ->
-	if Raw.make_current obj then begin
-	  callback ~width:(GdkEvent.Configure.width ev)
-	    ~height:(GdkEvent.Configure.height ev)
-	end
-	else prerr_endline "GlGtk-WARNING **: could not make current";
-	true
-      end
-  method realize ~callback =
-    let connect = new GObj.misc_signals ~after (GtkBase.Widget.coerce obj) in
-    connect#realize ~callback:
-      begin fun ev ->
-	if Raw.make_current obj then callback ()
-	else prerr_endline "GlGtk-WARNING **: could not make current"
-      end
-end
-
-class area obj = object (self)
-  inherit GObj.widget (obj : gl_area obj)
-  method as_area = obj
-  method event = new GObj.event_ops obj
-  method connect = new area_signals obj
-  method set_size = GtkMisc.DrawingArea.size obj
-  method swap_buffers () = Raw.swap_buffers obj
-  method make_current () =
-    if not (Raw.make_current obj) then
-      raise (Gl.GLerror "make_current")
-end
-
-let area options ?share ?(width=0) ?(height=0) ?packing ?show () =
-  let share =
-    match share with Some (x : area) -> Some x#as_area | None -> None in
-  let w = Raw.create options ~share:(Gpointer.optboxed share) in
-  if width <> 0 || height <> 0 then GtkMisc.DrawingArea.size w ~width ~height;
-  GtkBase.Widget.add_events w [`EXPOSURE];
-  GObj.pack_return (new area w) ~packing ~show