Module History

module History: sig .. end

Source code navigation history.


Since Nitrogen-20111001

type history_elt = 
| Global of Cil_types.global
| Localizable of Pretty_source.localizable
val is_empty : unit -> bool
Does the history contain an event.
val can_go_back : unit -> bool
Are there past events in the history.
val can_go_forward : unit -> bool
Are there events to redo in the history.
val back : unit -> unit
If possible, go back one step in the history.
val forward : unit -> unit
If possible (ie. if back has been called), go forward one step in the history.
val push : history_elt -> unit

Add the element to the current history; clears the forward history, and push the old current element to the past history.
val show_current : unit -> unit
Redisplay the current history point, if available. Useful to refresh the gui.
val on_current_history : unit -> (unit -> unit) -> unit
on_current_history () returns a closure at such that at f will execute f in a context in which the history will be the one relevant when on_current_history was executed.
val apply_on_selected : (Pretty_source.localizable -> unit) -> unit
apply_on_selected f applies f to the currently selected Pretty_source.localizable. Does nothing if nothing is selected.