module Gtk_helper:sig
..end
Generic Gtk helpers.
val framac_logo : GdkPixbuf.pixbuf option
val framac_icon : GdkPixbuf.pixbuf option
module Icon:sig
..end
Some generic icon management tools.
module Configuration:sig
..end
Configuration module for the GUI: all magic visual constants should use this mechanism (window width, ratios, ...).
val make_tag : < create_tag : ?name:string -> GText.tag_property list -> GText.tag;
tag_table : Gtk.text_tag_table; .. > ->
name:string -> GText.tag_property list -> GText.tag
val apply_tag : GSourceView2.source_buffer -> GText.tag -> int -> int -> unit
val remove_tag : GSourceView2.source_buffer -> GText.tag -> int -> int -> unit
val cleanup_tag : GSourceView2.source_buffer -> GText.tag -> unit
GSourceView2.source_buffer -> unit
: val make_formatter : ?flush:(unit -> unit) -> #GText.buffer -> Format.formatter
Build a formatter that redirects its output to the given buffer.
flush
is called whenever the formatter is flushed.
val log_redirector : ?flush:(unit -> unit) -> (string -> unit) -> unit
Redirects all strings written to the terminal and call the given function on each.
val redirect : Format.formatter -> #GText.buffer -> unit
Redirect the given formatter to the given buffer
val spawn_command : ?timeout:int ->
?stdout:Buffer.t ->
?stderr:Buffer.t ->
string -> string array -> (Unix.process_status -> unit) -> unit
Launches the given command and calls the given
function when the process terminates.
If timeout is > 0 (the default) then the process will be killed if it does
not end before timeout seconds.
In this case the returned process status will be
Unix.WSIGNALED Sys.sigalrm
.
val gui_unlocked : bool Pervasives.ref
This is a mutex you may use to prevent running some code while the GUI is locked.
val register_locking_machinery : ?lock_last:bool ->
lock:(bool -> unit) -> unlock:(unit -> unit) -> unit -> unit
Add hooks to the locking mechanism of the GUI.
lock_last
must be set to true if lock
must be executed after all the
others locking actions and unlock
must be executed before all the others
unlocking actions. Default is false
. At least one "lock_last" action is
allowed.
lock_last
and new
argument ()
2 Tooltips
val do_tooltip : ?tooltip:string -> < coerce : GObj.widget; .. > -> unit
Add the given tooltip to the given widget. It has no effect if no tooltip is given.
type'a
chooser =GPack.box -> string -> (unit -> 'a) -> ('a -> unit) -> unit -> unit
The created widget is packed in the box. The two following functions are supposed to be accessors(get and set) for the value to be displayed. The returned closure may be called to resynchronize the value in the widget from the get function.
val on_bool : ?tooltip:string -> ?use_markup:bool -> bool chooser
Pack a check button
val range_selector : ?tooltip:string ->
?use_markup:bool ->
GPack.box ->
label:string ->
lower:int -> upper:int -> (int -> unit) -> (unit -> int) -> unit -> unit
val on_int : ?tooltip:string ->
?use_markup:bool ->
?lower:int ->
?upper:int ->
?sensitive:(unit -> bool) -> ?width:int -> int chooser
Pack a spin button. By default, sensitivity is set to true when this function is called.
val on_string : ?tooltip:string ->
?use_markup:bool ->
?validator:(string -> bool) -> ?width:int -> string chooser
Pack a string chooser
val on_string_set : ?tooltip:string ->
?use_markup:bool -> ?width:int -> string chooser
Pack a string-set chooser
val on_string_completion : ?tooltip:string ->
?use_markup:bool ->
?validator:(string -> bool) -> string list -> string chooser
val on_combo : string list ->
?tooltip:string ->
?use_markup:bool -> ?width:int -> string chooser
Pack a string-selector
class type host =object
..end
A utility class to catch exceptions and report proper error messages.
class error_manager :?reset:unit -> unit -> GWindow.window_skel ->
host
A utility class to catch exceptions and report proper error messages.
class type source_files_chooser_host =object
..end
val source_files_chooser : source_files_chooser_host ->
string list -> (string list -> unit) -> unit
Open a dialog box for choosing C source files and performing an action on them.
val refresh_gui : unit -> unit
Process some pending events in the main Glib loop.
This is intended to be called only when !gui_unlocked == false
.
val string_selector : string list -> (GObj.widget -> unit) -> GEdit.entry
val expand_to_path : GTree.view -> Gtk.tree_path -> unit
val make_string_list : packing:(GObj.widget -> unit) ->
(string -> unit) * (unit -> unit) * (unit -> string list)
val place_paned : GPack.paned -> float -> unit
Sets the position of the paned widget to the given ratio
val save_paned_ratio : string -> GPack.paned -> unit
Saves the current ratio of the panel associated to the given key.
val old_gtk_compat : ('a -> unit) -> 'a -> unit
Catch exception Not_found
and do nothing
val trace_event : GObj.event_ops -> unit
Trace all events on stderr for the given object. This is a debugging function: it should not be called during normal execution.
val make_text_page : ?pos:int -> GPack.notebook -> string -> (GPack.notebook -> unit) * GText.view
Insert a GText.view in a new page of the notebook with the given title,
at position pos
if specified, or last if not.
It returns a new GText.view together with a function to reparent the
inserted page in another notebook.
The tab label of the created page will be highlighted whenever its
contents changes.
val open_in_external_viewer : ?line:int -> string -> unit
Opens file
in an external viewer, optionally centered on line line
(if supported by the viewer). The viewer is executed in the
background (i.e. it does not block the execution of Frama-C).
The external viewer is given by the environment variable EDITOR
.
If undefined, a default viewer is used.
module MAKE_CUSTOM_LIST:
A functor to build custom Gtk lists.
val input_string : parent:GWindow.window ->
title:string ->
?ok:string -> ?cancel:string -> ?text:string -> string -> string option
Copied from lablgtk GToolbox.input_string
. See the lablgtk API for more
details.
val graph_window : parent:GWindow.window ->
title:string ->
(packing:(GObj.widget -> unit) -> unit -> < adapt_zoom : unit -> unit; .. >) ->
unit
Create a new window displaying a graph.
val graph_window_through_dot : parent:GWindow.window -> title:string -> (Format.formatter -> unit) -> unit
Create a new window displaying a graph, by printing dot commands.