add UTop.exec_in_gui
Ignore-this: dc3c14404cb338f609e1d486664a1676 darcs-hash:20110921130911-c41ad-72bec8de684d12f9c16c0ae5a0e56a6627230021
This commit is contained in:
parent
c511fa0f02
commit
66a816fe72
|
@ -23,6 +23,8 @@ type ui = UTop_private.ui = Console | GTK | Emacs
|
||||||
|
|
||||||
let get_ui () = S.value UTop_private.ui
|
let get_ui () = S.value UTop_private.ui
|
||||||
|
|
||||||
|
let exec_in_gui f = !UTop_private.exec_in_gui f
|
||||||
|
|
||||||
(* +-----------------------------------------------------------------+
|
(* +-----------------------------------------------------------------+
|
||||||
| Keywords |
|
| Keywords |
|
||||||
+-----------------------------------------------------------------+ *)
|
+-----------------------------------------------------------------+ *)
|
||||||
|
|
|
@ -24,6 +24,17 @@ type ui = Console | GTK | Emacs
|
||||||
val get_ui : unit -> ui
|
val get_ui : unit -> ui
|
||||||
(** Returns the user interface in use. *)
|
(** Returns the user interface in use. *)
|
||||||
|
|
||||||
|
(** {6 GTK specific utilities} *)
|
||||||
|
|
||||||
|
val exec_in_gui : (unit -> unit) -> unit
|
||||||
|
(** [exec_in_gui f] executes [f] in the thread that handle the
|
||||||
|
UI. The only use of this function is to call [window#show ()] on
|
||||||
|
Windows:
|
||||||
|
|
||||||
|
Since windows are attached to a thread on Windows and utop
|
||||||
|
handle the UI in a separate thread, doing [window#show ()] in
|
||||||
|
the toplevel UI will not work. *)
|
||||||
|
|
||||||
(** {6 Console/GTK specific configuration} *)
|
(** {6 Console/GTK specific configuration} *)
|
||||||
|
|
||||||
type profile = Dark | Light
|
type profile = Dark | Light
|
||||||
|
|
|
@ -22,3 +22,5 @@ let count, set_count = S.create(-1)
|
||||||
type ui = Console | GTK | Emacs
|
type ui = Console | GTK | Emacs
|
||||||
|
|
||||||
let ui, set_ui = S.create Console
|
let ui, set_ui = S.create Console
|
||||||
|
|
||||||
|
let exec_in_gui : ((unit -> unit) -> unit) ref = ref (fun f -> f ())
|
||||||
|
|
|
@ -86,12 +86,30 @@ let init_history () =
|
||||||
return ()
|
return ()
|
||||||
|
|
||||||
(* +-----------------------------------------------------------------+
|
(* +-----------------------------------------------------------------+
|
||||||
| GTK ui |
|
| Glib main loop |
|
||||||
+-----------------------------------------------------------------+ *)
|
+-----------------------------------------------------------------+ *)
|
||||||
|
|
||||||
(* Initializes GTK. *)
|
(* Initializes GTK. *)
|
||||||
let _ = GMain.init ~setlocale:false ()
|
let _ = GMain.init ~setlocale:false ()
|
||||||
|
|
||||||
|
let () =
|
||||||
|
UTop_private.exec_in_gui :=
|
||||||
|
(fun job ->
|
||||||
|
ignore (Glib.Timeout.add ~ms:0 ~callback:(fun () -> job (); false)))
|
||||||
|
|
||||||
|
(* The glib main loop. *)
|
||||||
|
let main () =
|
||||||
|
while true do
|
||||||
|
Lwt_glib.iter true
|
||||||
|
done
|
||||||
|
|
||||||
|
(* Start the glib main loop in another thread. *)
|
||||||
|
let _ = Thread.create main ()
|
||||||
|
|
||||||
|
(* +-----------------------------------------------------------------+
|
||||||
|
| GTK ui |
|
||||||
|
+-----------------------------------------------------------------+ *)
|
||||||
|
|
||||||
(* Create the main window. *)
|
(* Create the main window. *)
|
||||||
let window = GWindow.window ~title:"utop" ~width:800 ~height:600 ~allow_shrink:true ()
|
let window = GWindow.window ~title:"utop" ~width:800 ~height:600 ~allow_shrink:true ()
|
||||||
|
|
||||||
|
@ -463,15 +481,5 @@ let () =
|
||||||
| None ->
|
| None ->
|
||||||
edit#misc#modify_base [(`NORMAL, default_background ())]
|
edit#misc#modify_base [(`NORMAL, default_background ())]
|
||||||
|
|
||||||
(* The glib main loop. *)
|
(* Show the window in the GUI thread, this is needed for windows. *)
|
||||||
let main () =
|
let () = UTop.exec_in_gui window#show
|
||||||
(* For some reason, this must happen in the dispatcher thread on
|
|
||||||
windows. *)
|
|
||||||
window#show ();
|
|
||||||
|
|
||||||
while true do
|
|
||||||
Lwt_glib.iter ()
|
|
||||||
done
|
|
||||||
|
|
||||||
(* Start the glib main loop in another thread. *)
|
|
||||||
let _ = Thread.create main ()
|
|
||||||
|
|
Loading…
Reference in New Issue