class type main_window_extension_points =object..end
method toplevel : main_window_extension_points : unit -> Menu_manager.menu_managermethod file_tree : Filetree.tmethod file_tree_view : GTree.viewmethod main_window : GWindow.windowmethod annot_window : Wtext.textpretty_information.method pretty_information : 'a. ?scroll:bool -> ('a, Format.formatter, unit) Pervasives.format -> 'aannot_window,
optionally scrolling it to the beginning of the message.method lower_notebook : GPack.notebookmethod source_viewer : GSourceView2.source_viewGText.view showing the AST.method source_viewer_scroll : GBin.scrolled_windowGText.view showing the AST.method reactive_buffer : reactive_buffermethod original_source_viewer : Source_manager.tmethod launcher : unit -> unitmethod error : 'a.
?parent:GWindow.window_skel ->
?reset:bool -> ('a, Format.formatter, unit) Pervasives.format -> 'areset 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) ->
unitmethod register_source_highlighter : (reactive_buffer ->
Pretty_source.localizable -> start:int -> stop:int -> unit) ->
unitGtext.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_buffermethod register_panel : (main_window_extension_points ->
string * GObj.widget * (unit -> unit) option) ->
unitregister_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 -> unitmethod rehighlight : unit -> unitregister_source_highlighter have been
updated.method redisplay : unit -> unitmethod 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 optionf ().
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 -> 'amethod pop_info : unit -> unitmethod show_ids : booltrue, 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