+let check rendering_window scratch_window () =
+ let inputt = (rendering_window#inputt : GEdit.text) in
+ let oldinputt = (rendering_window#oldinputt : GEdit.text) in
+ let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in
+ let output = (rendering_window#output : GMathView.math_view) in
+ let proofw = (rendering_window#proofw : GMathView.math_view) in
+ let inputlen = inputt#length in
+ let input = inputt#get_chars 0 inputlen ^ "\n" in
+ let curi,metasenv =
+ match !ProofEngine.proof with
+ None -> assert false
+ | Some (curi,metasenv,_,_) -> curi,metasenv
+ in
+ let ciccontext,names_context =
+ let context =
+ match !ProofEngine.goal with
+ None -> assert false
+ | Some (_,(ctx,_)) -> ctx
+ in
+ ProofEngine.cic_context_of_context context,
+ List.map (function (_,n,_) -> n) context
+ in
+ (* Do something interesting *)
+ let lexbuf = Lexing.from_string input in
+ try
+ while true do
+ (* Execute the actions *)
+ match
+ CicTextualParserContext.main curi names_context CicTextualLexer.token
+ lexbuf
+ with
+ None -> ()
+ | Some expr ->
+ try
+ let ty = CicTypeChecker.type_of_aux' metasenv ciccontext expr in
+ let mml = mml_of_cic_term ty in
+ scratch_window#show () ;
+ scratch_window#display ~dom:mml
+ with
+ e ->
+ print_endline ("? " ^ CicPp.ppterm expr) ;
+ raise e
+ done
+ with
+ CicTextualParser0.Eof ->
+ inputt#delete_text 0 inputlen ;
+ ignore(oldinputt#insert_text input oldinputt#length)
+ | e ->
+ print_endline ("Error: " ^ Printexc.to_string e) ; flush stdout
+;;
+