Module GuiNavigator

module GuiNavigator: sig .. end

type filter = [ `All | `Module | `Select ] 
type card = [ `Goal | `List ] 
type focus = [ `All
| `Call of GuiSource.call
| `Index of Wpo.index
| `Property of Property.t ]
val index_of_lemma : string * 'a * 'b * 'c * 'd -> Wpo.index
val focus_of_selection : GuiSource.selection ->
[< `All | `Module | `Select ] ->
[> `All
| `Call of GuiSource.call
| `Index of Wpo.index
| `Property of Property.t ]
exception FIRST of Wpo.t
val first : ((Wpo.t -> 'a) -> 'b) -> Wpo.t option
val iter_kf : Cil_types.kernel_function -> (Wpo.t -> unit) -> unit
val iter_ip : Property.t -> (Wpo.t -> unit) -> unit
val iter_ips : Property.t list -> (Wpo.t -> unit) -> unit
val calls : GuiSource.call -> Property.t list
val goal_of_selection : GuiSource.selection -> Wpo.t option
class behavior : main:Design.main_window_extension_points -> filter:filter Toolbox.selector -> next:Toolbox.button -> prev:Toolbox.button -> index:Toolbox.button -> clear:Toolbox.button -> card:card Toolbox.selector -> list:GuiList.pane -> goal:GuiGoal.pane -> source:GuiSource.highlighter -> popup:GuiSource.popup -> object .. end
val make : Design.main_window_extension_points -> unit