sig
  class type reactive_buffer =
    object
      method buffer : GSourceView.source_buffer
      method error :
        ?parent:GWindow.window_skel ->
        ?reset:bool -> ('a, Format.formatter, unit) format -> 'a
      method full_protect :
        cancelable:bool ->
        ?parent:GWindow.window_skel -> (unit -> 'a) -> 'a option
      method locs : Pretty_source.Locs.state
      method protect :
        cancelable:bool ->
        ?parent:GWindow.window_skel -> (unit -> unit) -> unit
      method redisplay : unit
      method rehighlight : unit
      method private set_reset : (unit -> unit) -> unit
    end
  class type view_code =
    object
      method display_globals : Cil_types.global list -> unit
      method scroll : Pretty_source.localizable -> unit
      method select_or_display_global : Cil_types.global -> unit
      method view_original : Cil_types.location -> unit
      method view_original_stmt : Cil_types.stmt -> Cil_types.location
      method view_stmt : Cil_types.stmt -> unit
    end
  class protected_menu_factory :
    Gtk_helper.host -> GMenu.menu -> [GMenu.menu] GMenu.factory
  class type main_window_extension_points =
    object
      method annot_window : Wtext.text
      method display_globals : Cil_types.global list -> unit
      method error :
        ?parent:GWindow.window_skel ->
        ?reset:bool -> ('a, Format.formatter, unit) Pervasives.format -> 'a
      method file_tree : Filetree.t
      method file_tree_view : GTree.view
      method full_protect :
        cancelable:bool ->
        ?parent:GWindow.window_skel -> (unit -> 'a) -> 'a option
      method help_message :
        < event : GObj.event_ops; .. > ->
        ('b, Format.formatter, unit) Pervasives.format -> 'b
      method launcher : unit -> unit
      method lower_notebook : GPack.notebook
      method main_window : GWindow.window
      method menu_manager : unit -> Menu_manager.menu_manager
      method original_source_viewer : Source_manager.t
      method pop_info : unit -> unit
      method pretty_information :
        ?scroll:bool -> ('a, Format.formatter, unit) Pervasives.format -> 'a
      method protect :
        cancelable:bool ->
        ?parent:GWindow.window_skel -> (unit -> unit) -> unit
      method push_info : ('a, Format.formatter, unit) Pervasives.format -> 'a
      method reactive_buffer : Design.reactive_buffer
      method redisplay : unit -> unit
      method register_panel :
        (Design.main_window_extension_points ->
         string * GObj.widget * (unit -> unit) option) ->
        unit
      method register_source_highlighter :
        (Design.reactive_buffer ->
         Pretty_source.localizable -> start:int -> stop:int -> unit) ->
        unit
      method register_source_selector :
        (GMenu.menu GMenu.factory ->
         Design.main_window_extension_points ->
         button:int -> Pretty_source.localizable -> unit) ->
        unit
      method rehighlight : unit -> unit
      method reset : unit -> unit
      method scroll : Pretty_source.localizable -> unit
      method select_or_display_global : Cil_types.global -> unit
      method show_ids : bool
      method source_viewer : GSourceView.source_view
      method source_viewer_scroll : GBin.scrolled_window
      method toplevel : Design.main_window_extension_points
      method view_original : Cil_types.location -> unit
      method view_original_stmt : Cil_types.stmt -> Cil_types.location
      method view_stmt : Cil_types.stmt -> unit
    end
  class main_window : unit -> main_window_extension_points
  val register_extension :
    (Design.main_window_extension_points -> unit) -> unit
  val register_reset_extension :
    (Design.main_window_extension_points -> unit) -> unit
  val reactive_buffer :
    Design.main_window_extension_points ->
    ?parent_window:GWindow.window ->
    Cil_types.global list -> Design.reactive_buffer
  module Feedback :
    sig
      val declare_markers : GSourceView.source_view -> unit
      val mark :
        GSourceView.source_buffer ->
        ?call_site:Cil_types.stmt ->
        offset:int -> Property_status.Feedback.t -> unit
    end
end