class type main_window_extension_points =object
..end
method toplevel : main_window_extension_points
unit -> Menu_manager.menu_manager
: method file_tree : Filetree.t
method file_tree_view : GTree.view
method main_window : GWindow.window
method annot_window : Wtext.text
pretty_information
.method pretty_information : 'a. ?scroll:bool -> ('a, Format.formatter, unit) Pervasives.format -> 'a
annot_window
,
optionally scrolling it to the beginning of the message.method lower_notebook : GPack.notebook
method source_viewer : GSourceView2.source_view
GText.view
showing the AST.method source_viewer_scroll : GBin.scrolled_window
GText.view
showing the AST.method reactive_buffer : reactive_buffer
method original_source_viewer : Source_manager.t
method launcher : unit -> unit
method error : 'a.
?parent:GWindow.window_skel ->
?reset:bool -> ('a, Format.formatter, unit) Pervasives.format -> 'a
reset
is true
(default is false), the gui is reset after the dialog has been
displayed.method register_source_selector : (GMenu.menu GMenu.factory ->
main_window_extension_points ->
button:int -> Pretty_source.localizable -> unit) ->
unit
method register_source_highlighter : (reactive_buffer ->
Pretty_source.localizable -> start:int -> stop:int -> unit) ->
unit
Gtext.tags
is used to decide which tag is rendered on
top of the other.Design.main_window_extension_points.reactive_buffer
instead
of a GSourceView2.source_buffer
method register_panel : (main_window_extension_points ->
string * GObj.widget * (unit -> unit) option) ->
unit
register_panel (name, widget, refresh)
registers a panel in GUI.
The arguments are the name of the panel to create,
the widget containing the panel and a function to be called on
refresh.method reset : unit -> unit
method rehighlight : unit -> unit
register_source_highlighter
have been
updated.method redisplay : unit -> unit
method protect : cancelable:bool -> ?parent:GWindow.window_skel -> (unit -> unit) -> unit
Set cancelable to true
if the protected action should be cancellable
by the user through button `Stop'.
method full_protect : 'a.
cancelable:bool -> ?parent:GWindow.window_skel -> (unit -> 'a) -> 'a option
f ()
.
The parent window must be set if this method is not called directly
by the main window: it will ensure that error dialogs are transient
for the right window.
Set cancelable to true
if the protected action should be cancellable
by the user through button `Stop'.
method push_info : 'a. ('a, Format.formatter, unit) Pervasives.format -> 'a
method pop_info : unit -> unit
method show_ids : bool
true
, the messages shown in the GUI can mention internal ids
(vid, sid, etc.). If false
, other means of identification should
be used (line numbers, etc.).method help_message : 'c 'b.
(< event : GObj.event_ops; .. > as 'c) ->
('b, Format.formatter, unit) Pervasives.format -> 'b