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)
+ (* TODO Zack: may be current_proofs if we want an MDI interface *)
+let (current_proof: MatitaProof.proof option ref) = ref None
+
+(** {2 Settings} *)
+
+let untitled_con_uri = UriManager.uri_of_string "cic:/untitled.con"
+let untitled_def_uri = UriManager.uri_of_string "cic:/untitled.def"
+
+(** {2 Initialization} *)
let _ = Helm_registry.load_from "matita.conf.xml"
let _ = GMain.Main.init ()
(** quit program, possibly asking for confirmation *)
let quit () = GMain.Main.quit ()
-let _ = gui#setQuitCallback quit
-let _ = gui#main#debugMenu#misc#hide ()
+
+let _ =
+ gui#setQuitCallback quit;
+ gui#main#debugMenu#misc#hide ();
+ ignore (gui#main#newProofMenuItem#connect#activate (fun _ ->
+ if (!current_proof <> None) &&
+ not (ask_confirmation ~gui
+ ~msg:("Starting a new proof will abort current one,\n" ^
+ "are you sure you want to continue?")
+ ())
+ then
+ () (* abort new proof process *)
+ else
+ prerr_endline "nuova prova"
+ (* TODO Zack: FINQUI ora mi serve il disambiguatore *)
+ ))
(** <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"]
- 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
+let _ =
+ 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
+ ~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 MatitaTypes.No_choice -> MatitaTypes.error "no choice");
+ addDebugItem "toggle auto disambiguation" (fun _ ->
+ Helm_registry.set_bool "matita.auto_disambiguation"
+ (not (Helm_registry.get_bool "matita.auto_disambiguation")))
+ end
(** </DEBUGGING> *)
let _ = GtkThread.main ()