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
;;
C.output_html
("<h1 color=\"red\">Many terms selected</h1>")
- let call_tactic_with_goal_input_in_scratch tactic scratch_window () =
+ let call_tactic_with_goal_input_in_scratch tactic () =
let module L = LogicalOperations in
let module G = Gdome in
- let mmlwidget =
- (scratch_window#mmlwidget : GMathViewAux.multi_selection_math_view) in
let savedproof = !ProofEngine.proof in
let savedgoal = !ProofEngine.goal in
- match mmlwidget#get_selections with
- [node] ->
- let xpath =
- ((node : Gdome.element)#getAttributeNS
- ~namespaceURI:Misc.helmns
- ~localName:(G.domString "xref"))#to_string
- in
- if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
- else
- begin
- try
- match C.get_current_scratch_infos () with
- (* term is the whole goal in the scratch_area *)
- Some (term,ids_to_terms, ids_to_father_ids,_) ->
- let id = xpath in
- let expr = tactic term (Hashtbl.find ids_to_terms id) in
- let mml,scratch_infos =
- ApplyStylesheets.mml_of_cic_term 111 expr
- in
- C.set_current_scratch_infos (Some scratch_infos) ;
- scratch_window#show () ;
- scratch_window#mmlwidget#load_doc ~dom:mml
- | None -> assert false (* "ERROR: No current term!!!" *)
- with
- e ->
- C.output_html
- ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
- end
+ let scratch_window = C.scratch_window () in
+ match scratch_window#sequent_viewer#get_selected_terms with
+ [term] ->
+ begin
+ try
+ let expr = tactic term scratch_window#term in
+ scratch_window#sequent_viewer#load_sequent
+ scratch_window#metasenv (111,scratch_window#context,expr) ;
+ scratch_window#set_term expr ;
+ scratch_window#show () ;
+ with
+ e ->
+ C.output_html
+ ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
+ end
| [] ->
C.output_html
("<h1 color=\"red\">No term selected</h1>")
C.output_html
("<h1 color=\"red\">Many terms selected</h1>")
- let call_tactic_with_goal_inputs_in_scratch tactic scratch_window () =
+ let call_tactic_with_goal_inputs_in_scratch tactic () =
let module L = LogicalOperations in
let module G = Gdome in
- let mmlwidget =
- (scratch_window#mmlwidget : GMathViewAux.multi_selection_math_view) in
+ let scratch_window = C.scratch_window () in
let savedproof = !ProofEngine.proof in
let savedgoal = !ProofEngine.goal in
- match mmlwidget#get_selections with
+ match scratch_window#sequent_viewer#get_selected_terms with
[] ->
C.output_html
- ("<h1 color=\"red\">No term selected</h1>")
- | l ->
+ ("<h1 color=\"red\">No terms selected</h1>")
+ | terms ->
try
- match C.get_current_scratch_infos () with
- (* term is the whole goal in the scratch_area *)
- Some (term,ids_to_terms, ids_to_father_ids,_) ->
- let term_of_node node =
- let xpath =
- ((node : Gdome.element)#getAttributeNS
- ~namespaceURI:Misc.helmns
- ~localName:(G.domString "xref"))#to_string
- in
- if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
- else
- let id = xpath in
- Hashtbl.find ids_to_terms id
- in
- let terms = List.map term_of_node l in
- let expr = tactic terms term in
- let mml,scratch_infos =
- ApplyStylesheets.mml_of_cic_term 111 expr
- in
- C.set_current_scratch_infos (Some scratch_infos) ;
- scratch_window#show () ;
- scratch_window#mmlwidget#load_doc ~dom:mml
- | None -> assert false (* "ERROR: No current term!!!" *)
+ let expr = tactic terms scratch_window#term in
+ scratch_window#sequent_viewer#load_sequent
+ scratch_window#metasenv (111,scratch_window#context,expr) ;
+ scratch_window#set_term expr ;
+ scratch_window#show () ;
with
e ->
C.output_html
let left = call_tactic ProofEngine.left
let right = call_tactic ProofEngine.right
let assumption = call_tactic ProofEngine.assumption
+ let injection = call_tactic_with_input ProofEngine.injection
+ let discriminate = call_tactic_with_input ProofEngine.discriminate
let generalize =
call_tactic_with_goal_inputs
(ProofEngine.generalize ~mk_fresh_name_callback:C.mk_fresh_name_callback)
call_tactic_with_input
(ProofEngine.decompose
~uris_choice_callback:C.decompose_uris_choice_callback)
- let whd_in_scratch scratch_window =
+ let whd_in_scratch =
call_tactic_with_goal_inputs_in_scratch ProofEngine.whd_in_scratch
- scratch_window
- let reduce_in_scratch scratch_window =
+ let reduce_in_scratch =
call_tactic_with_goal_inputs_in_scratch ProofEngine.reduce_in_scratch
- scratch_window
- let simpl_in_scratch scratch_window =
+ let simpl_in_scratch =
call_tactic_with_goal_inputs_in_scratch ProofEngine.simpl_in_scratch
- scratch_window
end
;;