From 18ce84578a8aed3b1320ec0b42507f26fc5e3ca4 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 18 Apr 2002 12:14:36 +0000 Subject: [PATCH] * Scratch window added * Check command implemented --- helm/gTopLevel/gTopLevel.ml | 94 ++++++++++++++++++++++++++++++++++++- 1 file changed, 93 insertions(+), 1 deletion(-) diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml index 5726f3d8c..eb02cb07f 100644 --- a/helm/gTopLevel/gTopLevel.ml +++ b/helm/gTopLevel/gTopLevel.ml @@ -209,6 +209,28 @@ ignore(domImpl#saveDocumentToFile ~doc:sequent_mml *) ;; +let mml_of_cic_term term = + let context = + match !ProofEngine.goal with + None -> [] + | Some (_,(context,_)) -> context + in + let metasenv = + match !ProofEngine.proof with + None -> [] + | Some (_,metasenv,_,_) -> metasenv + in + let sequent_gdome,ids_to_terms,ids_to_father_ids = + SequentPp.XmlPp.print_sequent metasenv (context,term) + in + let sequent_doc = + Xml2Gdome.document_of_xml domImpl sequent_gdome + in + applyStylesheets sequent_doc sequent_styles sequent_args + (*CSC: magari prima o poi serve*) + (*current_scratch_infos := Some (ids_to_terms,ids_to_father_ids)*) +;; + let output_html outputhtml msg = htmlheader_and_content := !htmlheader_and_content ^ msg ; outputhtml#source (!htmlheader_and_content ^ htmlfooter) ; @@ -557,6 +579,57 @@ let state rendering_window () = print_endline ("Error: " ^ Printexc.to_string e) ; flush stdout ;; +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 +;; + let choose_selection (mmlwidget : GMathView.math_view) (element : Gdome.element option) = @@ -702,7 +775,21 @@ object(self) ignore(closeb#connect#clicked settings_window#misc#hide) end;; -(* Main windows *) +(* Scratch window *) + +class scratch_window () = + let window = + GWindow.window ~title:"MathML viewer" ~border_width:2 () in + let mmlwidget = + GMathView.math_view ~packing:(window#add) ~width:400 ~height:280 () in +object(self) + method display = mmlwidget#load_tree + method show = window#show + initializer + ignore(window#event#connect#delete (fun _ -> GMain.Main.quit () ; true )) +end;; + +(* Main window *) class rendering_window output proofw (label : GMisc.label) = let window = @@ -745,6 +832,9 @@ class rendering_window output proofw (label : GMisc.label) = let openb = GButton.button ~label:"Open" ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in + let checkb = + GButton.button ~label:"Check" + ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in let inputt = GEdit.text ~editable:true ~width:400 ~height: 100 ~packing:(vbox#pack ~padding:5) () in let vbox1 = @@ -791,6 +881,7 @@ class rendering_window output proofw (label : GMisc.label) = ~width:400 ~height: 200 ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) ~show:true () in + let scratch_window = new scratch_window () in object(self) method outputhtml = outputhtml method oldinputt = oldinputt @@ -815,6 +906,7 @@ object(self) ignore(window#event#connect#delete (fun _ -> GMain.Main.quit () ; true )) ; ignore(stateb#connect#clicked (state self)) ; ignore(openb#connect#clicked (open_ self)) ; + ignore(checkb#connect#clicked (check self scratch_window)) ; ignore(exactb#connect#clicked (exact self)) ; ignore(applyb#connect#clicked (apply self)) ; ignore(elimintrosb#connect#clicked (elimintros self)) ; -- 2.39.2