+let call_tactic_with_goal_inputs tactic () =
+ let module L = LogicalOperations in
+ let module G = Gdome in
+ let notebook = (rendering_window ())#notebook in
+ let output =
+ ((rendering_window ())#output : GMathViewAux.single_selection_math_view) in
+ let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
+ let savedproof = !ProofEngine.proof in
+ let savedgoal = !ProofEngine.goal in
+ try
+ let term_of_node node =
+ let xpath =
+ ((node : Gdome.element)#getAttributeNS
+ ~namespaceURI:helmns
+ ~localName:(G.domString "xref"))#to_string
+ in
+ if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
+ else
+ match !current_goal_infos with
+ Some (ids_to_terms, ids_to_father_ids,_) ->
+ let id = xpath in
+ (Hashtbl.find ids_to_terms id)
+ | None -> assert false (* "ERROR: No current term!!!" *)
+ in
+ match notebook#proofw#get_selections with
+ [] ->
+ output_html outputhtml
+ ("<h1 color=\"red\">No term selected</h1>")
+ | l ->
+ let terms = List.map term_of_node l in
+ match !current_goal_infos with
+ Some (ids_to_terms, ids_to_father_ids,_) ->
+ tactic terms ;
+ refresh_sequent notebook ;
+ refresh_proof output
+ | None -> assert false (* "ERROR: No current term!!!" *)
+ with
+ RefreshSequentException e ->
+ output_html outputhtml
+ ("<h1 color=\"red\">Exception raised during the refresh of the " ^
+ "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
+ ProofEngine.proof := savedproof ;
+ ProofEngine.goal := savedgoal ;
+ refresh_sequent notebook
+ | RefreshProofException e ->
+ output_html outputhtml
+ ("<h1 color=\"red\">Exception raised during the refresh of the " ^
+ "proof: " ^ Printexc.to_string e ^ "</h1>") ;
+ ProofEngine.proof := savedproof ;
+ ProofEngine.goal := savedgoal ;
+ refresh_sequent notebook ;
+ refresh_proof output
+ | e ->
+ output_html outputhtml
+ ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
+ ProofEngine.proof := savedproof ;
+ ProofEngine.goal := savedgoal
+;;
+