X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=inline;f=helm%2Fmatita%2FmatitaGui.ml;h=c9b387178bc8cd1c780de9940d481013a1d035a0;hb=6e7fd1727eafb8280d2a01c05eddf49d19db2aaa;hp=c891a0bde63ec069fd9ec1207adde788589aa40a;hpb=5602ae08829342b7c2526053a5cb27cffe8a3d52;p=helm.git
diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml
index c891a0bde..c9b387178 100644
--- a/helm/matita/matitaGui.ml
+++ b/helm/matita/matitaGui.ml
@@ -77,11 +77,16 @@ class gui () =
~packing:main#scriptScrolledWin#add
()
in
+ let default_font_size =
+ Helm_registry.get_opt_default Helm_registry.int
+ ~default:BuildTimeConf.default_font_size "matita.font_size"
+ in
let source_buffer = source_view#source_buffer in
object (self)
val mutable chosen_file = None
val mutable _ok_not_exists = false
- val mutable script_fname = None
+ val mutable script_fname = None
+ val mutable font_size = default_font_size
initializer
(* glade's check widgets *)
@@ -162,13 +167,15 @@ class gui () =
connect_button tbar#transitivityButton
(tac_w_term (A.Transitivity (loc, hole)));
connect_button tbar#assumptionButton (tac (A.Assumption loc));
- connect_button tbar#cutButton (tac_w_term (A.Cut (loc, hole)));
- connect_button tbar#autoButton (tac (A.Auto (loc,None)));
+ connect_button tbar#cutButton (tac_w_term (A.Cut (loc, None, hole)));
+ connect_button tbar#autoButton (tac (A.Auto (loc,None,None)));
MatitaGtkMisc.toggle_widget_visibility
~widget:(self#main#tacticsButtonsHandlebox :> GObj.widget)
~check:self#main#tacticsBarMenuItem;
let module Hr = Helm_registry in
- if not(Hr.get_opt_default Hr.get_bool false "matita.tactics_bar") then
+ if
+ not (Hr.get_opt_default Hr.bool ~default:false "matita.tactics_bar")
+ then
self#main#tacticsBarMenuItem#set_active false;
MatitaGtkMisc.toggle_callback
~callback:(function
@@ -176,14 +183,10 @@ class gui () =
| false -> self#main#toplevel#unfullscreen ())
~check:self#main#fullscreenMenuItem;
self#main#fullscreenMenuItem#set_active false;
- (* quit *)
- self#setQuitCallback (fun () -> exit 0);
(* log *)
MatitaLog.set_log_callback self#console#log_callback;
GtkSignal.user_handler :=
- (fun exn ->
- MatitaLog.error
- (sprintf "Uncaught exception: %s" (Printexc.to_string exn)));
+ (fun exn -> MatitaLog.error (MatitaExcPp.to_string exn));
(* script *)
let _ =
match GSourceView.source_language_from_file BuildTimeConf.lang_file with
@@ -204,7 +207,8 @@ class gui () =
match self#chooseFile () with
| Some f ->
script#reset ();
- script#loadFrom f;
+ script#assignFileName f;
+ script#loadFromFile ();
console#message ("'"^f^"' loaded.\n");
self#_enableSaveTo f
| None -> ()
@@ -213,7 +217,8 @@ class gui () =
let script = s () in
match self#chooseFile ~ok_not_exists:true () with
| Some f ->
- script#saveTo f;
+ script#assignFileName f;
+ script#saveToFile ();
console#message ("'"^f^"' saved.\n");
self#_enableSaveTo f
| None -> ()
@@ -222,7 +227,8 @@ class gui () =
match script_fname with
| None -> saveAsScript ()
| Some f ->
- (s ())#saveTo f;
+ (s ())#assignFileName f;
+ (s ())#saveToFile ();
console#message ("'"^f^"' saved.\n");
in
let newScript () = (s ())#reset (); disableSave () in
@@ -241,6 +247,25 @@ class gui () =
connect_key self#sourceView#event
~modifiers:[`CONTROL] ~stop:true sym f
in
+ (* quit *)
+ self#setQuitCallback (fun () ->
+ if source_view#buffer#modified then
+ begin
+ let rc =
+ MatitaGtkMisc.ask_confirmation
+ ~parent:main#toplevel
+ ~title:"Unsaved work!"
+ ~message:("Your work is unsaved!\n\n"^
+ "Do you want to save the script before exiting?")
+ ()
+ in
+ match rc with
+ | `YES -> saveScript ();
+ if not source_view#buffer#modified then
+ GMain.Main.quit ()
+ | `NO -> GMain.Main.quit ()
+ | `CANCEL -> ()
+ end else GMain.Main.quit ());
connect_button self#main#scriptAdvanceButton advance;
connect_button self#main#scriptRetractButton retract;
connect_button self#main#scriptTopButton top;
@@ -265,19 +290,7 @@ class gui () =
"\n";
advance ());
(* script monospace font stuff *)
- let font =
- Helm_registry.get_opt_default Helm_registry.get
- BuildTimeConf.default_script_font "matita.script_font"
- in
-(* let monospace_tag =
- source_buffer#create_tag [`FONT_DESC font]
- in *)
- self#sourceView#misc#modify_font_by_name font;
-(* let _ =
- source_buffer#connect#changed ~callback:(fun _ ->
- let start, stop = source_buffer#bounds in
- source_buffer#apply_tag monospace_tag start stop)
- in *)
+ self#updateFontSize ();
(* debug menu *)
self#main#debugMenu#misc#hide ();
(* status bar *)
@@ -298,9 +311,17 @@ class gui () =
method loadScript file =
let script = MatitaScript.instance () in
script#reset ();
- script#loadFrom file;
+ script#assignFileName file;
+ script#loadFromFile ();
console#message ("'"^file^"' loaded.");
self#_enableSaveTo file
+
+ method setStar name b =
+ let l = main#scriptLabel in
+ if b then
+ l#set_text (name ^ " *")
+ else
+ l#set_text (name)
method private _enableSaveTo file =
script_fname <- Some file;
@@ -350,8 +371,9 @@ class gui () =
keyBindingBoxes
method setQuitCallback callback =
- ignore (main#toplevel#connect#destroy callback);
ignore (main#quitMenuItem#connect#activate callback);
+ ignore (main#toplevel#event#connect#delete
+ (fun _ -> callback ();true));
self#addKeyBinding GdkKeysyms._q callback
method chooseFile ?(ok_not_exists = false) () =
@@ -379,6 +401,22 @@ class gui () =
GtkThread.main ();
!text
+ method private updateFontSize () =
+ self#sourceView#misc#modify_font_by_name
+ (sprintf "%s %d" BuildTimeConf.script_font font_size)
+
+ method increaseFontSize () =
+ font_size <- font_size + 1;
+ self#updateFontSize ()
+
+ method decreaseFontSize () =
+ font_size <- font_size - 1;
+ self#updateFontSize ()
+
+ method resetFontSize () =
+ font_size <- default_font_size;
+ self#updateFontSize ()
+
end
let gui () =
@@ -390,11 +428,6 @@ let instance = singleton gui
let non p x = not (p x)
-let is_var_uri s =
- try
- String.sub s (String.length s - 4) 4 = ".var"
- with Invalid_argument _ -> false
-
(* this is a shit and should be changed :-{ *)
let interactive_uri_choice
?(selection_mode:[`SINGLE|`MULTIPLE] = `MULTIPLE) ?(title = "")
@@ -404,7 +437,7 @@ let interactive_uri_choice
~id uris
=
let gui = instance () in
- let nonvars_uris = lazy (List.filter (non is_var_uri) uris) in
+ let nonvars_uris = lazy (List.filter (non UriManager.uri_is_var) uris) in
if (selection_mode <> `SINGLE) &&
(Helm_registry.get_bool "matita.auto_disambiguation")
then
@@ -435,7 +468,7 @@ let interactive_uri_choice
| _ -> ()));
dialog#uriChoiceDialog#set_title title;
dialog#uriChoiceLabel#set_text msg;
- List.iter model#easy_append uris;
+ List.iter model#easy_append (List.map UriManager.string_of_uri uris);
dialog#uriChoiceConstantsButton#misc#set_sensitive nonvars_button;
let return v =
choices := v;
@@ -453,11 +486,11 @@ let interactive_uri_choice
connect_button dialog#uriChoiceAutoButton (fun _ ->
match model#easy_selection () with
| [] -> ()
- | uris -> return (Some uris));
+ | uris -> return (Some (List.map UriManager.uri_of_string uris)));
connect_button dialog#uriChoiceSelectedButton (fun _ ->
match model#easy_selection () with
| [] -> ()
- | uris -> return (Some uris));
+ | uris -> return (Some (List.map UriManager.uri_of_string uris)));
connect_button dialog#uriChoiceAbortButton (fun _ -> return None);
dialog#uriChoiceDialog#show ();
GtkThread.main ();