X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaGui.ml;h=5ea3903835f05dafa4a83dc4c6b2711b84aa3a5d;hb=12cc5b2b8e7f7bb0b5e315094b008a293a4df6b1;hp=2844aa92e5ce6b8666369e5aa4a549ed603ed851;hpb=8ce8ba9db77be5c6515301aa109726029e12834b;p=helm.git
diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml
index 2844aa92e..5ea390383 100644
--- a/helm/matita/matitaGui.ml
+++ b/helm/matita/matitaGui.ml
@@ -31,10 +31,18 @@ open MatitaMisc
let gui_instance = ref None ;;
+class type browserWin =
+ (* this class exists only because GEdit.combo_box_entry is not supported by
+ * lablgladecc :-(((( *)
+object
+ inherit MatitaGeneratedGui.browserWin
+ method browserUri: GEdit.combo_box_entry
+end
+
class console ~(buffer: GText.buffer) () =
object (self)
val error_tag = buffer#create_tag [ `FOREGROUND "red" ]
- val warning_tag = buffer#create_tag [ `FOREGROUND "yellow" ]
+ val warning_tag = buffer#create_tag [ `FOREGROUND "orange" ]
val message_tag = buffer#create_tag []
val debug_tag = buffer#create_tag [ `FOREGROUND "#888888" ]
method message s = buffer#insert ~iter:buffer#end_iter ~tags:[message_tag] s
@@ -50,6 +58,51 @@ class console ~(buffer: GText.buffer) () =
| `Message -> self#message (s ^ "\n")
| `Warning -> self#warning (s ^ "\n")
end
+
+let clean_current_baseuri status =
+ try
+ let baseuri = MatitaTypes.get_string_option status "baseuri" in
+ MatitacleanLib.clean_baseuris [baseuri]
+ with MatitaTypes.Option_error _ -> ()
+
+let ask_and_save_moo_if_needed parent fname status =
+ let save () =
+ MatitacLib.dump_moo_to_file fname status.MatitaTypes.moo_content_rev in
+ if (MatitaScript.instance ())#eos &&
+ status.MatitaTypes.proof_status = MatitaTypes.No_proof
+ then
+ begin
+ let mooname =
+ MatitaMisc.obj_file_of_script fname
+ in
+ let rc =
+ MatitaGtkMisc.ask_confirmation
+ ~title:"A .moo can be generated"
+ ~message:(Printf.sprintf
+ "%s can be generated for %s.\nShould I generate it?"
+ mooname fname)
+ ~parent ()
+ in
+ let b =
+ match rc with
+ | `YES -> true
+ | `NO -> false
+ | `CANCEL -> raise MatitaTypes.Cancel
+ in
+ if b then
+ save ()
+ else
+ clean_current_baseuri status
+ end
+ else
+ clean_current_baseuri status
+
+let ask_unsaved parent =
+ MatitaGtkMisc.ask_confirmation
+ ~parent ~title:"Unsaved work!"
+ ~message:("Your work is unsaved!\n\n"^
+ "Do you want to save the script before exiting?")
+ ()
class gui () =
(* creation order _is_ relevant for windows placement *)
@@ -60,10 +113,25 @@ class gui () =
[ main#mainWinEventBox ]
in
let console = new console ~buffer:main#logTextView#buffer () in
+ let (source_view: GSourceView.source_view) =
+ GSourceView.source_view
+ ~auto_indent:true
+ ~insert_spaces_instead_of_tabs:true ~tabs_width:2
+ ~margin:80 ~show_margin:true
+ ~smart_home_end:true
+ ~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 *)
@@ -125,7 +193,7 @@ class gui () =
in
let tac_w_term ast _ =
if (MatitaScript.instance ())#onGoingProof () then
- let (buf: GText.buffer) = self#main#scriptTextView#buffer in
+ let buf = source_buffer in
buf#insert ~iter:(buf#get_iter_at_mark (`NAME "locked"))
("\n" ^ TacticAstPp.pp_tactic ast)
in
@@ -133,8 +201,8 @@ class gui () =
connect_button tbar#introsButton (tac (A.Intros (loc, None, [])));
connect_button tbar#applyButton (tac_w_term (A.Apply (loc, hole)));
connect_button tbar#exactButton (tac_w_term (A.Exact (loc, hole)));
- connect_button tbar#elimButton (tac_w_term (A.Elim (loc, hole, None)));
- connect_button tbar#elimTypeButton (tac_w_term (A.ElimType (loc, hole)));
+ connect_button tbar#elimButton (tac_w_term (A.Elim (loc, hole, None, None, [])));
+ connect_button tbar#elimTypeButton (tac_w_term (A.ElimType (loc, hole, None, None, [])));
connect_button tbar#splitButton (tac (A.Split loc));
connect_button tbar#leftButton (tac (A.Left loc));
connect_button tbar#rightButton (tac (A.Right loc));
@@ -144,38 +212,48 @@ 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)));
- (* quit *)
- self#setQuitCallback (fun () -> exit 0);
+ 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.bool ~default:false "matita.tactics_bar")
+ then
+ self#main#tacticsBarMenuItem#set_active false;
+ MatitaGtkMisc.toggle_callback
+ ~callback:(function
+ | true -> self#main#toplevel#fullscreen ()
+ | false -> self#main#toplevel#unfullscreen ())
+ ~check:self#main#fullscreenMenuItem;
+ self#main#fullscreenMenuItem#set_active false;
(* 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
+ | None ->
+ MatitaLog.warn (sprintf "can't load language file %s"
+ BuildTimeConf.lang_file)
+ | Some matita_lang ->
+ source_buffer#set_language matita_lang;
+ source_buffer#set_highlight true
+ in
let s () = MatitaScript.instance () in
let disableSave () =
script_fname <- None;
self#main#saveMenuItem#misc#set_sensitive false
in
- let loadScript () =
- let script = s () in
- match self#chooseFile () with
- | Some f ->
- script#reset ();
- script#loadFrom f;
- console#message ("'"^f^"' loaded.");
- self#_enableSaveTo f
- | None -> ()
- in
let saveAsScript () =
let script = s () in
match self#chooseFile ~ok_not_exists:true () with
| Some f ->
- script#saveTo f;
- console#message ("'"^f^"' saved.");
+ script#assignFileName f;
+ script#saveToFile ();
+ console#message ("'"^f^"' saved.\n");
self#_enableSaveTo f
| None -> ()
in
@@ -183,13 +261,44 @@ class gui () =
match script_fname with
| None -> saveAsScript ()
| Some f ->
- (s ())#saveTo f;
- console#message ("'"^f^"' saved.");
+ (s ())#assignFileName f;
+ (s ())#saveToFile ();
+ console#message ("'"^f^"' saved.\n");
+ in
+ let loadScript () =
+ let script = s () in
+ let status = script#status in
+ try
+ if source_view#buffer#modified then
+ begin
+ match ask_unsaved main#toplevel with
+ | `YES -> saveScript ()
+ | `NO -> ()
+ | `CANCEL -> raise MatitaTypes.Cancel
+ end;
+ (match script_fname with
+ | None -> ()
+ | Some fname ->
+ ask_and_save_moo_if_needed main#toplevel fname status);
+ match self#chooseFile () with
+ | Some f ->
+ script#reset ();
+ script#assignFileName f;
+ script#loadFromFile ();
+ console#message ("'"^f^"' loaded.\n");
+ self#_enableSaveTo f
+ | None -> ()
+ with MatitaTypes.Cancel -> ()
+ in
+ let newScript () =
+ (s ())#reset ();
+ (s ())#template ();
+ disableSave ();
+ script_fname <- None
in
- let newScript () = (s ())#reset (); disableSave () in
let cursor () =
- let buf = self#main#scriptTextView#buffer in
- buf#place_cursor (buf#get_iter_at_mark (`NAME "locked"))
+ source_buffer#place_cursor
+ (source_buffer#get_iter_at_mark (`NAME "locked"))
in
let advance _ = (MatitaScript.instance ())#advance (); cursor () in
let retract _ = (MatitaScript.instance ())#retract (); cursor () in
@@ -199,9 +308,41 @@ class gui () =
let connect_key sym f =
connect_key self#main#mainWinEventBox#event
~modifiers:[`CONTROL] ~stop:true sym f;
- connect_key self#main#scriptTextView#event
+ connect_key self#sourceView#event
~modifiers:[`CONTROL] ~stop:true sym f
in
+ (* quit *)
+ self#setQuitCallback (fun () ->
+ let status = (MatitaScript.instance ())#status in
+ if source_view#buffer#modified then
+ begin
+ let rc = ask_unsaved main#toplevel in
+ try
+ match rc with
+ | `YES -> saveScript ();
+ if not source_view#buffer#modified then
+ begin
+ (match script_fname with
+ | None -> ()
+ | Some fname ->
+ ask_and_save_moo_if_needed
+ main#toplevel fname status);
+ GMain.Main.quit ()
+ end
+ | `NO -> GMain.Main.quit ()
+ | `CANCEL -> raise MatitaTypes.Cancel
+ with MatitaTypes.Cancel -> ()
+ end
+ else
+ begin
+ (match script_fname with
+ | None -> clean_current_baseuri status; GMain.Main.quit ()
+ | Some fname ->
+ try
+ ask_and_save_moo_if_needed main#toplevel fname status;
+ GMain.Main.quit ()
+ with MatitaTypes.Cancel -> ())
+ end);
connect_button self#main#scriptAdvanceButton advance;
connect_button self#main#scriptRetractButton retract;
connect_button self#main#scriptTopButton top;
@@ -217,51 +358,54 @@ class gui () =
connect_menu_item self#main#newMenuItem newScript;
connect_key GdkKeysyms._period
(fun () ->
- let buf = self#main#scriptTextView#buffer in
- buf#insert ~iter:(buf#get_iter_at_mark `INSERT) ".\n";
- advance ());
+ source_buffer#insert ~iter:(source_buffer#get_iter_at_mark `INSERT)
+ ".\n";
+ advance ());
connect_key GdkKeysyms._Return
(fun () ->
- let buf = self#main#scriptTextView#buffer in
- buf#insert ~iter:(buf#get_iter_at_mark `INSERT) "\n";
- advance ());
+ source_buffer#insert ~iter:(source_buffer#get_iter_at_mark `INSERT)
+ "\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 =
- self#main#scriptTextView#buffer#create_tag [`FONT_DESC font]
- in *)
- self#main#scriptTextView#misc#modify_font_by_name font;
-(* let _ =
- self#main#scriptTextView#buffer#connect#changed ~callback:(fun _ ->
- let start, stop = self#main#scriptTextView#buffer#bounds in
- self#main#scriptTextView#buffer#apply_tag monospace_tag start stop)
- in *)
+ self#updateFontSize ();
(* debug menu *)
self#main#debugMenu#misc#hide ();
(* status bar *)
- self#main#hintLowImage#set_file "icons/matita-bulb-low.png";
- self#main#hintMediumImage#set_file "icons/matita-bulb-medium.png";
- self#main#hintHighImage#set_file "icons/matita-bulb-high.png";
+ self#main#hintLowImage#set_file (image_path "matita-bulb-low.png");
+ self#main#hintMediumImage#set_file (image_path "matita-bulb-medium.png");
+ self#main#hintHighImage#set_file (image_path "matita-bulb-high.png");
(* focus *)
- self#main#scriptTextView#misc#grab_focus ();
+ self#sourceView#misc#grab_focus ();
(* main win dimension *)
let width = Gdk.Screen.width () in
let height = Gdk.Screen.height () in
let main_w = width * 90 / 100 in
let main_h = height * 80 / 100 in
- let script_w = main_w / 2 in
+ let script_w = main_w * 6 / 10 in
self#main#toplevel#resize ~width:main_w ~height:main_h;
self#main#hpaneScriptSequent#set_position script_w
method loadScript file =
let script = MatitaScript.instance () in
script#reset ();
- script#loadFrom file;
+ script#assignFileName file;
+ if not (Sys.file_exists file) then
+ begin
+ let oc = open_out file in
+ let template = MatitaMisc.input_file BuildTimeConf.script_template in
+ output_string oc template;
+ close_out oc
+ end;
+ 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;
@@ -269,15 +413,22 @@ class gui () =
method console = console
-
+ method sourceView: GSourceView.source_view = (source_view: GSourceView.source_view)
method about = about
method fileSel = fileSel
method main = main
method newBrowserWin () =
- let win = new browserWin () in
- win#check_widgets ();
- win
+ object (self)
+ inherit browserWin ()
+ val combo = GEdit.combo_box_entry ()
+ initializer
+ self#check_widgets ();
+ let combo_widget = combo#coerce in
+ uriHBox#pack ~from:`END ~fill:true ~expand:true combo_widget;
+ combo#entry#misc#grab_focus ()
+ method browserUri = combo
+ end
method newUriDialog () =
let dialog = new uriChoiceDialog () in
@@ -304,8 +455,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) () =
@@ -333,6 +485,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 () =
@@ -344,11 +512,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 = "")
@@ -358,7 +521,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
@@ -389,7 +552,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;
@@ -407,11 +570,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 ();