+++ /dev/null
-(* Copyright (C) 2004, HELM Team.
- *
- * This file is part of HELM, an Hypertextual, Electronic
- * Library of Mathematics, developed at the Computer Science
- * Department, University of Bologna, Italy.
- *
- * HELM is free software; you can redistribute it and/or
- * modify it under the terms of the GNU General Public License
- * as published by the Free Software Foundation; either version 2
- * of the License, or (at your option) any later version.
- *
- * HELM is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
- * GNU General Public License for more details.
- *
- * You should have received a copy of the GNU General Public License
- * along with HELM; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
- * MA 02111-1307, USA.
- *
- * For details, see the HELM World-Wide-Web page,
- * http://helm.cs.unibo.it/
- *)
-
-open MatitaGtkMisc
-
-(** {2 Internal status} *)
-
-let (get_proof, set_proof, has_proof) =
- let (current_proof: MatitaTypes.proof option ref) = ref None in
- ((fun () ->
- match !current_proof with
- | Some proof -> proof
- | None -> failwith "No current proof"),
- (fun proof -> (* TODO Zack: this function should probably be smarter taking
- care also of unregistering notifications subscriber and so on *)
- current_proof := proof),
- (fun () -> !current_proof <> None))
-
-(** {2 Settings} *)
-
-let debug_print = MatitaTypes.debug_print
-
-(** {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 parserr = new MatitaDisambiguator.parserr ()
-let mqiconn = MQIConn.init ()
-let disambiguator =
- new MatitaDisambiguator.disambiguator ~parserr ~mqiconn
- ~chooseUris:(interactive_user_uri_choice ~gui)
- ~chooseInterp:(interactive_interp_choice ~gui)
- ()
-
-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 ();
- set_proof (Some proof)
-
-let quit () = (* quit program, asking for confirmation if needed *)
- if not (has_proof ()) ||
- (ask_confirmation ~gui
- ~msg:("Proof in progress, are you sure you want to quit?") ())
- then
- GMain.Main.quit ()
-
-let proof_handler =
- { MatitaTypes.get_proof = get_proof;
- MatitaTypes.set_proof = set_proof;
- MatitaTypes.has_proof = has_proof;
- MatitaTypes.new_proof = new_proof;
- MatitaTypes.quit = quit;
- }
-
-let interpreter =
- let console = gui#console in
- new MatitaInterpreter.interpreter ~disambiguator ~proof_handler ~console ()
-
-let _ =
- gui#setQuitCallback quit;
- gui#setPhraseCallback interpreter#evalPhrase;
- gui#main#debugMenu#misc#hide ();
- ignore (gui#main#newProofMenuItem#connect#activate (fun _ ->
- if has_proof () &&
- not (ask_confirmation ~gui
- ~msg:("Proof in progress, are you sure you want to start a new one?")
- ())
- then
- () (* abort new proof process *)
- else
- let input = ask_text ~gui ~msg:"Insert proof goal" ~multiline:true () in
- let (env, metasenv, term) =
- disambiguator#disambiguateTerm (Stream.of_string input)
- in
- let proof = MatitaProof.proof ~typ:term ~metasenv () in
- new_proof proof))
-
- (** <DEBUGGING> *)
-let _ =
- if BuildTimeConf.debug then begin
- gui#main#debugMenu#misc#show ();
- let addDebugItem ~label callback =
- let item =
- GMenu.menu_item ~packing:gui#main#debugMenu_menu#append ~label ()
- in
- ignore (item#connect#activate callback)
- in
- addDebugItem "interactive user uri choice" (fun _ ->
- try
- let uris =
- interactive_user_uri_choice ~gui ~selection_mode:`MULTIPLE
- ~msg:"messaggio" ~nonvars_button:true
- ["cic:/uno.con"; "cic:/due.var"; "cic:/tre.con"; "cic:/quattro.con";
- "cic:/cinque.var"]
- in
- List.iter prerr_endline uris
- with MatitaGtkMisc.Cancel -> MatitaTypes.error "no choice");
- addDebugItem "toggle auto disambiguation" (fun _ ->
- Helm_registry.set_bool "matita.auto_disambiguation"
- (not (Helm_registry.get_bool "matita.auto_disambiguation")));
- addDebugItem "mono line text input" (fun _ ->
- prerr_endline (ask_text ~gui ~title:"title" ~msg:"message" ()));
- addDebugItem "multi line text input" (fun _ ->
- prerr_endline
- (ask_text ~gui ~title:"title" ~multiline:true ~msg:"message" ()));
- addDebugItem "dump proof status to stdout" (fun _ ->
- print_endline ((get_proof ())#status#toString));
- end
- (** </DEBUGGING> *)
-
-let _ = GtkThread.main ()
-