]> matita.cs.unibo.it Git - helm.git/blob - helm/matita/matita.ml
snapshot
[helm.git] / helm / matita / matita.ml
1 (* Copyright (C) 2004, HELM Team.
2  * 
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.
6  * 
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.
11  * 
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.
16  *
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,
20  * MA  02111-1307, USA.
21  * 
22  * For details, see the HELM World-Wide-Web page,
23  * http://helm.cs.unibo.it/
24  *)
25
26 open MatitaGtkMisc
27
28 (** {2 Internal status} *)
29
30   (* TODO Zack: may be current_proofs if we want an MDI interface *)
31 let (get_proof, set_proof, has_proof) =
32   let (current_proof: MatitaTypes.proof option ref) = ref None in
33   ((fun () ->
34     match !current_proof with
35     | Some proof -> proof
36     | None -> assert false),
37    (fun proof -> current_proof := Some proof),
38    (fun () -> !current_proof <> None))
39
40 (** {2 Settings} *)
41
42 let debug_print = MatitaTypes.debug_print
43
44 (** {2 Initialization} *)
45
46 let _ = Helm_registry.load_from "matita.conf.xml"
47 let _ = GMain.Main.init ()
48 let gui = new MatitaGui.gui (Helm_registry.get "matita.glade_file")
49 let parserr = new MatitaDisambiguator.parserr ()
50 let mqiconn = MQIConn.init ()
51 let disambiguator =
52   new MatitaDisambiguator.disambiguator ~parserr ~mqiconn
53     ~chooseUris:(interactive_user_uri_choice ~gui)
54     ~chooseInterp:(interactive_interp_choice ~gui)
55     ()
56 let new_proof proof =
57   (* TODO Zack: high level function which create a new proof object and register
58   * to it the widgets which must be refreshed upon status changes *)
59 (*       proof#status#attach ... *)
60   proof#status#notify ();
61   set_proof proof
62 let interpreter =
63   new MatitaInterpreter.interpreter
64     ~disambiguator ~console:gui#console ~get_proof ~new_proof ()
65
66   (** quit program, possibly asking for confirmation *)
67 let quit () = GMain.Main.quit ()
68
69 let _ =
70   gui#setQuitCallback quit;
71   gui#setPhraseCallback interpreter#evalPhrase;
72   gui#main#debugMenu#misc#hide ();
73   ignore (gui#main#newProofMenuItem#connect#activate (fun _ ->
74    if has_proof () &&
75       not (ask_confirmation ~gui
76               ~msg:("Starting a new proof will abort current one,\n" ^
77                 "are you sure you want to continue?")
78               ())
79     then
80       ()  (* abort new proof process *)
81     else
82       let input = ask_text ~gui ~msg:"Insert proof goal" ~multiline:true () in
83       let (env, metasenv, term) =
84         disambiguator#disambiguateTerm (Stream.of_string input)
85       in
86       let proof = MatitaProof.proof ~typ:term ~metasenv () in
87       new_proof proof;
88       debug_print ("new proof, goal is: " ^ CicPp.ppterm term)))
89
90   (** <DEBUGGING> *)
91 let _ =
92   if BuildTimeConf.debug then begin
93     gui#main#debugMenu#misc#show ();
94     let addDebugItem ~label callback =
95       let item =
96         GMenu.menu_item ~packing:gui#main#debugMenu_menu#append ~label ()
97       in
98       ignore (item#connect#activate callback)
99     in
100     addDebugItem "interactive user uri choice" (fun _ ->
101       try
102         let uris =
103           interactive_user_uri_choice ~gui ~selection_mode:`MULTIPLE
104             ~msg:"messaggio" ~nonvars_button:true
105             ["cic:/uno.con"; "cic:/due.var"; "cic:/tre.con"; "cic:/quattro.con";
106             "cic:/cinque.var"]
107         in
108         List.iter prerr_endline uris
109       with MatitaGtkMisc.Cancel -> MatitaTypes.error "no choice");
110     addDebugItem "toggle auto disambiguation" (fun _ ->
111       Helm_registry.set_bool "matita.auto_disambiguation"
112         (not (Helm_registry.get_bool "matita.auto_disambiguation")));
113     addDebugItem "mono line text input" (fun _ ->
114       prerr_endline (ask_text ~gui ~title:"title" ~msg:"message" ()));
115     addDebugItem "multi line text input" (fun _ ->
116       prerr_endline
117         (ask_text ~gui ~title:"title" ~multiline:true ~msg:"message" ()));
118     addDebugItem "dump proof status to stdout" (fun _ ->
119       print_endline ((get_proof ())#status#toString));
120   end
121   (** </DEBUGGING> *)
122
123 let _ = GtkThread.main ()
124