1 (* Copyright (C) 2004, HELM Team.
3 * This file is part of HELM, an Hypertextual, Electronic
4 * Library of Mathematics, developed at the Computer Science
5 * Department, University of Bologna, Italy.
7 * HELM is free software; you can redistribute it and/or
8 * modify it under the terms of the GNU General Public License
9 * as published by the Free Software Foundation; either version 2
10 * of the License, or (at your option) any later version.
12 * HELM is distributed in the hope that it will be useful,
13 * but WITHOUT ANY WARRANTY; without even the implied warranty of
14 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
15 * GNU General Public License for more details.
17 * You should have received a copy of the GNU General Public License
18 * along with HELM; if not, write to the Free Software
19 * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
22 * For details, see the HELM World-Wide-Web page,
23 * http://helm.cs.unibo.it/
28 (** {2 Internal status} *)
30 let (get_proof, set_proof, has_proof) =
31 let (current_proof: MatitaTypes.proof option ref) = ref None in
33 match !current_proof with
35 | None -> failwith "No current proof"),
36 (fun proof -> (* TODO Zack: this function should probably be smarter taking
37 care also of unregistering notifications subscriber and so on *)
38 current_proof := proof),
39 (fun () -> !current_proof <> None))
43 let debug_print = MatitaTypes.debug_print
46 let domImpl = lazy (Gdome.domImplementation ()) in
49 ((Lazy.force domImpl)#saveDocumentToFile ~doc ~name:dest ~indent:true ())
51 (** {2 Initialization} *)
53 let _ = Helm_registry.load_from "matita.conf.xml"
54 let _ = GMain.Main.init ()
55 let gui = new MatitaGui.gui (Helm_registry.get "matita.glade_file")
56 let parserr = new MatitaDisambiguator.parserr ()
57 let mqiconn = MQIConn.init ()
59 new MatitaDisambiguator.disambiguator ~parserr ~mqiconn
60 ~chooseUris:(interactive_user_uri_choice ~gui)
61 ~chooseInterp:(interactive_interp_choice ~gui)
64 let mml_of_cic_object = BuildTimeConf.Transformer.mml_of_cic_object in
66 let frame = GBin.frame ~packing:(gui#proof#scrolledProof#add) ~show:true () in
67 MatitaMathView.proof_viewer ~show:true ~packing:(frame#add) ()
69 MatitaMathView.proof_viewer ~show:true ~packing:(gui#proof#scrolledProof#add) ()
72 let mml_of_cic_sequent = BuildTimeConf.Transformer.mml_of_cic_sequent in
73 MatitaMathView.sequent_viewer ~mml_of_cic_sequent ~show:true
74 ~packing:(gui#main#scrolledSequents#add) ()
77 let new_proof (proof: MatitaTypes.proof) =
79 * - ids_to_inner_types, ids_to_inner_sorts handling
80 * - sequent viewer notification
82 let xmldump_observer _ _ = print_endline proof#toString in
83 let proof_observer _ (status, metadata) =
84 debug_print "proof_observer";
85 let (acic, ids_to_terms, ids_to_father_ids, ids_to_inner_sorts,
86 ids_to_inner_types, ids_to_conjectures, ids_to_hypotheses) =
89 let ((uri_opt, _, _, _), _) = status in
90 let uri = MatitaTypes.unopt_uri uri_opt in
91 debug_print "apply transformation";
93 BuildTimeConf.Transformer.mml_of_cic_object
94 ~explode_all:true uri acic ids_to_inner_sorts ids_to_inner_types
96 if BuildTimeConf.debug then save_dom ~doc:mathml ~dest:"/tmp/matita.xml";
97 proof_viewer#load_proof mathml metadata;
98 debug_print "/proof_observer"
100 ignore (proof#attach_observer ~interested_in:StatefulProofEngine.all_events
102 ignore (proof#attach_observer ~interested_in:StatefulProofEngine.all_events
105 set_proof (Some proof)
107 let quit () = (* quit program, asking for confirmation if needed *)
108 if not (has_proof ()) ||
109 (ask_confirmation ~gui
110 ~msg:("Proof in progress, are you sure you want to quit?") ())
115 { MatitaTypes.get_proof = get_proof;
116 MatitaTypes.set_proof = set_proof;
117 MatitaTypes.has_proof = has_proof;
118 MatitaTypes.new_proof = new_proof;
119 MatitaTypes.quit = quit;
123 let console = gui#console in
124 new MatitaInterpreter.interpreter ~disambiguator ~proof_handler ~console ()
127 gui#setQuitCallback quit;
128 gui#setPhraseCallback interpreter#evalPhrase;
129 gui#main#debugMenu#misc#hide ();
130 ignore (gui#main#newProofMenuItem#connect#activate (fun _ ->
132 not (ask_confirmation ~gui
133 ~msg:("Proof in progress, are you sure you want to start a new one?")
136 () (* abort new proof process *)
138 let input = ask_text ~gui ~msg:"Insert proof goal" ~multiline:true () in
139 let (env, metasenv, expr) =
140 disambiguator#disambiguateTerm (Stream.of_string input)
142 let proof = MatitaProof.proof ~typ:expr ~metasenv () in
147 if BuildTimeConf.debug then begin
148 gui#main#debugMenu#misc#show ();
149 let addDebugItem ~label callback =
151 GMenu.menu_item ~packing:gui#main#debugMenu_menu#append ~label ()
153 ignore (item#connect#activate callback)
155 addDebugItem "interactive user uri choice" (fun _ ->
158 interactive_user_uri_choice ~gui ~selection_mode:`MULTIPLE
159 ~msg:"messaggio" ~nonvars_button:true
160 ["cic:/uno.con"; "cic:/due.var"; "cic:/tre.con"; "cic:/quattro.con";
163 List.iter prerr_endline uris
164 with MatitaGtkMisc.Cancel -> MatitaTypes.error "no choice");
165 addDebugItem "toggle auto disambiguation" (fun _ ->
166 Helm_registry.set_bool "matita.auto_disambiguation"
167 (not (Helm_registry.get_bool "matita.auto_disambiguation")));
168 addDebugItem "mono line text input" (fun _ ->
169 prerr_endline (ask_text ~gui ~title:"title" ~msg:"message" ()));
170 addDebugItem "multi line text input" (fun _ ->
172 (ask_text ~gui ~title:"title" ~multiline:true ~msg:"message" ()));
173 addDebugItem "dump proof status to stdout" (fun _ ->
174 print_endline ((get_proof ())#toString));
178 let _ = GtkThread.main ()