Module Pretty_source

module Pretty_source: sig .. end
Utilities to pretty print source with located elements in a Gtk TextBuffer.

type localizable = Printer_tag.localizable = 
| PStmt of (Cil_types.kernel_function * Cil_types.stmt)
| PStmtStart of (Cil_types.kernel_function * Cil_types.stmt)
| PLval of (Cil_types.kernel_function option * Cil_types.kinstr * Cil_types.lval)
| PExp of (Cil_types.kernel_function option * Cil_types.kinstr * Cil_types.exp)
| PTermLval of (Cil_types.kernel_function option * Cil_types.kinstr * Property.t *
Cil_types.term_lval)
| PVDecl of (Cil_types.kernel_function option * Cil_types.kinstr * Cil_types.varinfo) (*
Declaration and definition of variables and function. Check the type of the varinfo to distinguish between the various possibilities. If the varinfo is a global or a local, the kernel_function is the one in which the variable is declared. The kinstr argument is given for local variables with an explicit initializer.
*)
| PGlobal of Cil_types.global (*
all globals but variable declarations and function definitions.
*)
| PIP of Property.t
module Locs: sig .. end
val fold_preconds_at_callsite : Cil_types.stmt -> unit
val are_preconds_unfolded : Cil_types.stmt -> bool
val display_source : Cil_types.global list ->
GSourceView.source_buffer ->
host:Gtk_helper.host ->
highlighter:(localizable -> start:int -> stop:int -> unit) ->
selector:(button:int -> localizable -> unit) ->
Locs.state -> unit
The selector and the highlighter are always host#protected. The selector will not be called when not !Gtk_helper.gui_unlocked. This clears the Locs.state passed as argument, then fills it.
val hilite : Locs.state -> unit
val stmt_start : Locs.state -> Cil_types.stmt -> int
Offset at which the current statement starts in the buffer corresponding to state, _without_ ACSL assertions/contracts, etc.
val locate_localizable : Locs.state -> localizable -> (int * int) option
Returns Some (start,stop) in offset from start of buffer if the given localizable has been displayed according to Locs.locs.
val kf_of_localizable : localizable -> Cil_types.kernel_function option
val ki_of_localizable : localizable -> Cil_types.kinstr
val varinfo_of_localizable : localizable -> Cil_types.varinfo option
val localizable_from_locs : Locs.state ->
file:Datatype.Filepath.t -> line:int -> localizable list
Returns the lists of localizable in file at line visible in the current Locs.state. This function is inefficient as it iterates on all the current Locs.state.
val loc_to_localizable : ?precise_col:bool -> Filepath.position -> localizable option
return the (hopefully) most precise localizable that contains the given Filepath.position. If precise_col is true, takes the column number into account (possibly a more precise, but costly, result).
Since Nitrogen-20111001