- begin
- try
- let uri,metasenv,bo,ty =
- match !ProofEngine.proof with
- None -> assert false
- | Some (uri,metasenv,bo,ty) -> uri,metasenv,bo,ty
- in
- let canonical_context =
- match !ProofEngine.goal with
- None -> assert false
- | Some metano ->
- let (_,canonical_context,_) =
- List.find (function (m,_,_) -> m=metano) metasenv
- in
- canonical_context in
- let (metasenv',expr) =
- (C.term_editor ())#get_metasenv_and_term canonical_context metasenv
- in
- ProofEngine.proof := Some (uri,metasenv',bo,ty) ;
- tactic ~goal_input:term ~input:expr ;
- C.refresh_goals () ;
- C.refresh_proof () ;
- (C.term_editor ())#reset
- with
- RefreshSequentException e ->
- C.output_html
- ("<h1 color=\"red\">Exception raised during the refresh of " ^
- "the sequent: " ^ Printexc.to_string e ^ "</h1>") ;
- ProofEngine.proof := savedproof ;
- ProofEngine.goal := savedgoal ;
- C.refresh_goals ()
- | RefreshProofException e ->
- C.output_html
- ("<h1 color=\"red\">Exception raised during the refresh of " ^
- "the proof: " ^ Printexc.to_string e ^ "</h1>") ;
- ProofEngine.proof := savedproof ;
- ProofEngine.goal := savedgoal ;
- C.refresh_goals () ;
- C.refresh_proof ()
- | e ->
- C.output_html
- ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
- ProofEngine.proof := savedproof ;
- ProofEngine.goal := savedgoal ;
- end
- | [] ->
- C.output_html
- ("<h1 color=\"red\">No term selected</h1>")
- | _ ->
- C.output_html
- ("<h1 color=\"red\">Many terms selected</h1>")
+ handle_refresh_exception
+ (fun () ->
+ let uri,metasenv,bo,ty =
+ match ProofEngine.get_proof () with
+ None -> assert false
+ | Some (uri,metasenv,bo,ty) -> uri,metasenv,bo,ty
+ in
+ let canonical_context =
+ match !ProofEngine.goal with
+ None -> assert false
+ | Some metano ->
+ let (_,canonical_context,_) =
+ List.find (function (m,_,_) -> m=metano) metasenv
+ in
+ canonical_context in
+ let (metasenv',expr,ugraph) =(* FIX THIS AND *)
+ (C.term_editor ())#get_metasenv_and_term
+ canonical_context metasenv
+ in
+ ProofEngine.set_proof (Some (uri,metasenv',bo,ty)) ;
+ tactic ~goal_input:term ~input:expr ;
+ C.refresh_goals () ;
+ C.refresh_proof () ;
+ (C.term_editor ())#reset)
+ savedproof savedgoal
+ | [] -> HelmLogger.log (`Error (`T "No term selected"))
+ | _ -> HelmLogger.log (`Error (`T "Too many terms selected"))