module History:sig
..end
type
history_elt =
| |
Global of |
| |
Localizable of |
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 set_forward : history_elt list -> unit
Replaces the forward history with the given elements.
val get_current : unit -> history_elt option
return the current history point, if available
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 selected_localizable : unit -> Pretty_source.localizable option
selected_localizable ()
returns the localizable currently
selected, or None
if nothing or an entire global is selected.
val translate_history_elt : history_elt -> history_elt option
try to translate the history_elt of one project to the current one