X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Fmatita.ml;h=e565c03a787e6f0c1cd6b4eaaef9afba9b1048cf;hb=6b7f04b45232e6c690cacf5815c85c39de1f52b3;hp=8f34f5bf728c141b88fe12cc8f97c3303cc45756;hpb=e89486cad653803954662a5e543537acd49a866f;p=helm.git diff --git a/helm/matita/matita.ml b/helm/matita/matita.ml index 8f34f5bf7..e565c03a7 100644 --- a/helm/matita/matita.ml +++ b/helm/matita/matita.ml @@ -23,41 +23,82 @@ * http://helm.cs.unibo.it/ *) +open Printf + open MatitaGtkMisc +open MatitaTypes +open MatitaMisc (** {2 Internal status} *) let (get_proof, set_proof, has_proof) = let (current_proof: MatitaTypes.proof option ref) = ref None in - ((fun () -> + ((fun () -> (* get_proof *) match !current_proof with | Some proof -> proof | None -> failwith "No current proof"), - (fun proof -> current_proof := proof), - (fun () -> !current_proof <> None)) - -(** {2 Settings} *) - -let debug_print = MatitaTypes.debug_print + (fun proof -> (* set_proof *) + current_proof := proof), + (fun () -> (* has_proof *) + !current_proof <> None)) (** {2 Initialization} *) -let _ = Helm_registry.load_from "matita.conf.xml" -let _ = GMain.Main.init () -let gui = new MatitaGui.gui (Helm_registry.get "matita.glade_file") +let _ = + Helm_registry.load_from "matita.conf.xml"; + GtkMain.Rc.add_default_file BuildTimeConf.gtkrc; + GMain.Main.init () let parserr = new MatitaDisambiguator.parserr () -let mqiconn = MQIConn.init () +let dbd = + Mysql.quick_connect + ~host:(Helm_registry.get "db.host") + ~user:(Helm_registry.get "db.user") + ~database:(Helm_registry.get "db.database") + () +let gui = MatitaGui.instance () let disambiguator = - new MatitaDisambiguator.disambiguator ~parserr ~mqiconn + new MatitaDisambiguator.disambiguator ~parserr ~dbd ~chooseUris:(interactive_user_uri_choice ~gui) ~chooseInterp:(interactive_interp_choice ~gui) () +let proof_viewer = + let frame = GBin.frame ~packing:(gui#proof#scrolledProof#add) ~show:true () in + MatitaMathView.proof_viewer ~show:true ~packing:(frame#add) () +let sequent_viewer = MatitaMathView.sequent_viewer ~show:true () +let sequents_viewer = + let set_goal goal = + debug_print (sprintf "Setting goal %d" goal); + if not (has_proof ()) then assert false; + (get_proof ())#set_goal goal + in + MatitaMathView.sequents_viewer ~notebook:gui#main#sequentsNotebook + ~sequent_viewer ~set_goal () -let new_proof proof = - (* TODO Zack: high level function which create a new proof object and register - * to it the widgets which must be refreshed upon status changes *) -(* proof#status#attach ... *) - proof#status#notify (); +let new_proof (proof: MatitaTypes.proof) = + let xmldump_observer _ _ = print_endline proof#toString in + let proof_observer _ (status, ()) = + debug_print "proof_observer"; + let ((uri_opt, _, _, _), _) = status in + let uri = MatitaTypes.unopt_uri uri_opt in + debug_print "apply transformation"; + proof_viewer#load_proof status; + debug_print "/proof_observer" + in + let sequents_observer _ (((_, metasenv, _, _), goal_opt), ()) = + sequents_viewer#reset; + (match goal_opt with + | None -> () + | Some goal -> + sequents_viewer#load_sequents metasenv; + sequents_viewer#goto_sequent goal) + in + ignore (proof#attach_observer ~interested_in:StatefulProofEngine.all_events + sequents_observer); + ignore (proof#attach_observer ~interested_in:StatefulProofEngine.all_events + proof_observer); + ignore (proof#attach_observer ~interested_in:StatefulProofEngine.all_events + xmldump_observer); + proof#notify; set_proof (Some proof) let quit () = (* quit program, asking for confirmation if needed *) @@ -67,8 +108,15 @@ let quit () = (* quit program, asking for confirmation if needed *) then GMain.Main.quit () +let abort_proof () = + if has_proof () then begin + set_proof None; + sequents_viewer#reset + end + let proof_handler = { MatitaTypes.get_proof = get_proof; + MatitaTypes.abort_proof = abort_proof; MatitaTypes.set_proof = set_proof; MatitaTypes.has_proof = has_proof; MatitaTypes.new_proof = new_proof; @@ -79,6 +127,14 @@ let interpreter = let console = gui#console in new MatitaInterpreter.interpreter ~disambiguator ~proof_handler ~console () + (** prompt the user for the textual input of a term and disambiguate it *) +let ask_term ?(title = "term input") ?(msg = "insert term") () = + match gui#askText ~title ~msg () with + | Some t -> + let (_, _, term) = disambiguator#disambiguateTerm (Stream.of_string t) in + Some term + | None -> None + let _ = gui#setQuitCallback quit; gui#setPhraseCallback interpreter#evalPhrase; @@ -92,13 +148,60 @@ let _ = () (* abort new proof process *) else let input = ask_text ~gui ~msg:"Insert proof goal" ~multiline:true () in - let (env, metasenv, term) = + let (env, metasenv, expr) = disambiguator#disambiguateTerm (Stream.of_string input) in - let proof = MatitaProof.proof ~typ:term ~metasenv () in - new_proof proof)) + let proof = MatitaProof.proof ~typ:expr ~metasenv () in + new_proof proof)); + ignore (gui#main#openMenuItem#connect#activate (fun _ -> + match gui#chooseFile () with + | None -> () + | Some f when is_proof_script f -> + gui#script#scriptTextView#buffer#set_text (input_file f); + gui#script#scriptWin#show (); + gui#main#showScriptMenuItem#set_active true + | Some f -> + gui#console#echo_error (sprintf + "Don't know what to do with file: %s\nUnrecognized file format." + f))); + let tac_w_term name tac _ = + match ask_term ~title:name ~msg:("term for " ^ name) () with + | Some term -> (get_proof ())#apply_tactic (tac ~term) + | None -> () + in + let tac _ tac _ = (get_proof ())#apply_tactic tac in + let tbar = gui#toolbar in + ignore (tbar#introsButton#connect#clicked (tac "intros" (Tactics.intros ()))); + ignore (tbar#applyButton#connect#clicked (tac_w_term "apply" Tactics.apply)); + ignore (tbar#exactButton#connect#clicked (tac_w_term "exact" Tactics.exact)); + ignore (tbar#elimButton#connect#clicked (tac_w_term "elim" + Tactics.elim_intros_simpl)); + ignore (tbar#elimTypeButton#connect#clicked (tac_w_term "elim type" + Tactics.elim_type)); + ignore (tbar#splitButton#connect#clicked (tac "split" Tactics.split)); + ignore (tbar#leftButton#connect#clicked (tac "left" Tactics.left)); + ignore (tbar#rightButton#connect#clicked (tac "right" Tactics.right)); + ignore (tbar#existsButton#connect#clicked (tac "exists" Tactics.exists)); + ignore (tbar#reflexivityButton#connect#clicked (tac "reflexivity" + Tactics.reflexivity)); + ignore (tbar#symmetryButton#connect#clicked (tac "symmetry" + Tactics.symmetry)); + ignore (tbar#transitivityButton#connect#clicked (tac_w_term "transitivity" + Tactics.transitivity)); + ignore (tbar#assumptionButton#connect#clicked (tac "assumption" + Tactics.assumption)); + ignore (tbar#cutButton#connect#clicked (tac_w_term "cut" + (Tactics.cut ?mk_fresh_name_callback:None))); + ignore (tbar#autoButton#connect#clicked (tac "auto" (Tactics.auto ~dbd))) (** *) + +let save_dom = + let domImpl = lazy (Gdome.domImplementation ()) in + fun ~doc ~dest -> + ignore + ((Lazy.force domImpl)#saveDocumentToFile ~doc ~name:dest ~indent:true ()) + let _ = if BuildTimeConf.debug then begin gui#main#debugMenu#misc#show (); @@ -127,8 +230,9 @@ let _ = prerr_endline (ask_text ~gui ~title:"title" ~multiline:true ~msg:"message" ())); addDebugItem "dump proof status to stdout" (fun _ -> - print_endline ((get_proof ())#status#toString)); + print_endline ((get_proof ())#toString)); end + (** *) let _ = GtkThread.main ()