module type Callbacks =
sig
+ (* input widgets *)
val sequent_viewer : unit -> TermViewer.sequent_viewer
val term_editor : unit -> TermEditor.term_editor
- val get_current_scratch_infos :
+ val scratch_window :
unit ->
- (Cic.term *
- (Cic.id, Cic.term) Hashtbl.t *
- (Cic.id, Cic.id option) Hashtbl.t *
- (string, Cic.hypothesis) Hashtbl.t
- ) option
- val set_current_scratch_infos :
- (Cic.term *
- (Cic.id, Cic.term) Hashtbl.t *
- (Cic.id, Cic.id option) Hashtbl.t *
- (string, Cic.hypothesis) Hashtbl.t
- ) option -> unit
+ < sequent_viewer: TermViewer.sequent_viewer ;
+ show: unit -> unit ;
+ term: Cic.term ;
+ set_term : Cic.term -> unit ;
+ metasenv: Cic.metasenv ;
+ set_metasenv : Cic.metasenv -> unit ;
+ context: Cic.context ;
+ set_context : Cic.context -> unit >
+ (* output messages *)
+ val output_html : string -> unit
+ (* GUI refresh functions *)
val refresh_proof : unit -> unit
val refresh_goals : unit -> unit
+ (* callbacks for user-tactics interaction *)
val decompose_uris_choice_callback :
(UriManager.uri * int * 'a) list ->
(UriManager.uri * int * 'b list) list
val mk_fresh_name_callback :
Cic.context -> Cic.name -> typ:Cic.term -> Cic.name
- val output_html : string -> unit
end
module Make (C : Callbacks) :
val absurd : unit -> unit
val contradiction : unit -> unit
val decompose : unit -> unit
- val whd_in_scratch :
- < mmlwidget : GMathViewAux.multi_selection_math_view;
- show : unit -> 'a; .. > ->
- unit -> unit
- val reduce_in_scratch :
- < mmlwidget : GMathViewAux.multi_selection_math_view;
- show : unit -> 'a; .. > ->
- unit -> unit
- val simpl_in_scratch :
- < mmlwidget : GMathViewAux.multi_selection_math_view;
- show : unit -> 'a; .. > ->
- unit -> unit
+ val whd_in_scratch : unit -> unit
+ val reduce_in_scratch : unit -> unit
+ val simpl_in_scratch : unit -> unit
end