open MatitaGtkMisc
-exception Not_implemented of string
-let not_implemented feature = raise (Not_implemented feature)
+(** {2 Internal status} *)
- (** exceptions whose content should be presented to the user *)
-exception Failure of string
-let error s = raise (Failure s)
+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)
- (** quit program, possibly asking for confirmation *)
-let quit () = GMain.Main.quit ()
-let _ = gui#setQuitCallback quit
-let _ = gui#main#debugMenu#misc#hide ()
+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> *)
-if BuildTimeConf.debug then begin
- gui#main#debugMenu#misc#show ();
- let addDebugItem ~label callback =
- let item = GMenu.menu_item ~label () in
- gui#main#debugMenu_menu#append item;
- ignore (item#connect#activate callback);
- in
- addDebugItem "interactive user uri choice" (fun _ ->
- try
- let uris =
- interactive_user_uri_choice ~gui ~selection_mode:`MULTIPLE
- ~title:"titolo" ~msg:"messaggio" ~nonvars_button:true
- ["cic:/uno.con"; "cic:/due.var"; "cic:/tre.con"; "cic:/quattro.con";
- "cic:/cinque.var"]
+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
- List.iter prerr_endline uris
- with No_choice -> error "no choice");
- addDebugItem "toggle auto disambiguation" (fun _ ->
- Helm_registry.set_bool "matita.auto_disambiguation"
- (not (Helm_registry.get_bool "matita.auto_disambiguation")))
-end
+ 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 ()