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
45 (** {2 Initialization} *)
47 let _ = Helm_registry.load_from "matita.conf.xml"
48 let _ = GMain.Main.init ()
49 let gui = new MatitaGui.gui (Helm_registry.get "matita.glade_file")
50 let parserr = new MatitaDisambiguator.parserr ()
51 let mqiconn = MQIConn.init ()
53 new MatitaDisambiguator.disambiguator ~parserr ~mqiconn
54 ~chooseUris:(interactive_user_uri_choice ~gui)
55 ~chooseInterp:(interactive_interp_choice ~gui)
58 let mml_of_cic_object = BuildTimeConf.Transformer.mml_of_cic_object in
59 MatitaMathView.proof_viewer ~mml_of_cic_object ~show:true
60 ~packing:(gui#proof#scrolledProof#add) ()
63 let mml_of_cic_sequent = BuildTimeConf.Transformer.mml_of_cic_sequent in
64 MatitaMathView.sequent_viewer ~mml_of_cic_sequent ~show:true
65 ~packing:(gui#main#scrolledSequents#add) ()
68 let new_proof (proof: MatitaTypes.proof) =
70 * - ids_to_inner_types, ids_to_inner_sorts handling
71 * - sequent viewer notification
73 let xmldump_observer _ (status, _) = print_endline proof#toString in
74 ignore (proof#attach_observer ~interested_in:StatefulProofEngine.all_events
77 let proof_observer _ (status, ()) =
78 prerr_endline "proof_observer";
79 let ((uri_opt, metasenv, bo, ty), _) = status in
80 let uri = MatitaTypes.unopt_uri uri_opt in
81 (* TODO CSC [] is wrong *)
82 let proof = Cic.Constant (UriManager.name_of_uri uri,Some bo,ty,[]) in
84 ignore (proof_viewer#load_proof uri proof)
86 prerr_endline "proof_observer exception:";
87 prerr_endline (Printexc.to_string exn);
90 let proof_observer_id =
91 proof#attach_observer ~interested_in:StatefulProofEngine.all_events
96 set_proof (Some proof)
98 let quit () = (* quit program, asking for confirmation if needed *)
99 if not (has_proof ()) ||
100 (ask_confirmation ~gui
101 ~msg:("Proof in progress, are you sure you want to quit?") ())
106 { MatitaTypes.get_proof = get_proof;
107 MatitaTypes.set_proof = set_proof;
108 MatitaTypes.has_proof = has_proof;
109 MatitaTypes.new_proof = new_proof;
110 MatitaTypes.quit = quit;
114 let console = gui#console in
115 new MatitaInterpreter.interpreter ~disambiguator ~proof_handler ~console ()
118 gui#setQuitCallback quit;
119 gui#setPhraseCallback interpreter#evalPhrase;
120 gui#main#debugMenu#misc#hide ();
121 ignore (gui#main#newProofMenuItem#connect#activate (fun _ ->
123 not (ask_confirmation ~gui
124 ~msg:("Proof in progress, are you sure you want to start a new one?")
127 () (* abort new proof process *)
129 let input = ask_text ~gui ~msg:"Insert proof goal" ~multiline:true () in
130 let (env, metasenv, expr) =
131 disambiguator#disambiguateTerm (Stream.of_string input)
133 let proof = MatitaProof.proof ~typ:expr ~metasenv () in
138 if BuildTimeConf.debug then begin
139 gui#main#debugMenu#misc#show ();
140 let addDebugItem ~label callback =
142 GMenu.menu_item ~packing:gui#main#debugMenu_menu#append ~label ()
144 ignore (item#connect#activate callback)
146 addDebugItem "interactive user uri choice" (fun _ ->
149 interactive_user_uri_choice ~gui ~selection_mode:`MULTIPLE
150 ~msg:"messaggio" ~nonvars_button:true
151 ["cic:/uno.con"; "cic:/due.var"; "cic:/tre.con"; "cic:/quattro.con";
154 List.iter prerr_endline uris
155 with MatitaGtkMisc.Cancel -> MatitaTypes.error "no choice");
156 addDebugItem "toggle auto disambiguation" (fun _ ->
157 Helm_registry.set_bool "matita.auto_disambiguation"
158 (not (Helm_registry.get_bool "matita.auto_disambiguation")));
159 addDebugItem "mono line text input" (fun _ ->
160 prerr_endline (ask_text ~gui ~title:"title" ~msg:"message" ()));
161 addDebugItem "multi line text input" (fun _ ->
163 (ask_text ~gui ~title:"title" ~multiline:true ~msg:"message" ()));
164 addDebugItem "dump proof status to stdout" (fun _ ->
165 print_endline ((get_proof ())#toString));
169 let _ = GtkThread.main ()