Module GuiSource

module GuiSource: sig .. end

type selection = 
| S_none
| S_fun of Kernel_function.t
| S_prop of Property.t
| S_call of call
type call = {
   s_caller : Kernel_function.t;
   s_called : Kernel_function.t;
   s_stmt : Cil_datatype.Stmt.t;
}
val selection_of_localizable : Pretty_source.localizable -> selection
val kind_of_property : Property.identified_property -> string
val is_rte_generated : Cil_types.kernel_function -> bool
val is_rte_precond : Cil_types.kernel_function -> bool
class popup : unit -> object .. end
module PATH: Cil_datatype.Stmt.Set
module DEPS: Property.Set
val apply_tag : string ->
GText.tag_property list -> GSourceView2.source_buffer -> int -> int -> unit
val apply_goal : GSourceView2.source_buffer -> int -> int -> unit
val apply_effect : GSourceView2.source_buffer -> int -> int -> unit
val apply_path : GSourceView2.source_buffer -> int -> int -> unit
val apply_depend : GSourceView2.source_buffer -> int -> int -> unit
val instructions : PATH.t -> PATH.t
val lemmas : LogicUsage.logic_lemma list -> DEPS.t
class highlighter : Design.main_window_extension_points -> object .. end