open MatitaGtkMisc
open MatitaMisc
-let gui_instance = ref None ;;
+let gui_instance = ref None
class type browserWin =
(* this class exists only because GEdit.combo_box_entry is not supported by
class gui () =
(* creation order _is_ relevant for windows placement *)
let main = new mainWin () in
- let about = new aboutWin () in
let fileSel = new fileSelectionWin () in
let findRepl = new findReplWin () in
let develList = new develListWin () in
- let newDevel = new newDevelopmentWin () in
+ let newDevel = new newDevelWin () in
let keyBindingBoxes = (* event boxes which should receive global key events *)
[ main#mainWinEventBox ]
in
~default:BuildTimeConf.default_font_size "matita.font_size"
in
let source_buffer = source_view#source_buffer in
+(* let _ =
+ source_view#event#connect#selection_clear (fun _ ->
+ prerr_endline "source_view: selection clear";
+ false)
+ in *)
object (self)
val mutable chosen_file = None
val mutable _ok_not_exists = false
(* glade's check widgets *)
List.iter (fun w -> w#check_widgets ())
(let c w = (w :> <check_widgets: unit -> unit>) in
- [ c about; c fileSel; c main; c findRepl]);
+ [ c fileSel; c main; c findRepl]);
(* key bindings *)
List.iter (* global key bindings *)
(fun (key, callback) -> self#addKeyBinding key callback)
*)
[ ];
(* about win *)
- ignore (about#aboutWin#event#connect#delete (fun _ -> true));
- ignore (main#aboutMenuItem#connect#activate (fun _ ->
- about#aboutWin#show ()));
- connect_button about#aboutDismissButton (fun _ ->
- about#aboutWin#misc#hide ());
- about#aboutLabel#set_label (Pcre.replace ~pat:"@VERSION@"
- ~templ:BuildTimeConf.version about#aboutLabel#label);
+ let parse_txt_file file =
+ let ch = open_in (BuildTimeConf.runtime_base_dir ^ "/" ^ file) in
+ let l_rev = ref [] in
+ try
+ while true do
+ l_rev := input_line ch :: !l_rev;
+ done;
+ assert false
+ with
+ End_of_file ->
+ close_in ch;
+ List.rev !l_rev in
+ let about_dialog =
+ GWindow.about_dialog
+ ~authors:(parse_txt_file "AUTHORS")
+ (*~comments:"comments"*)
+ ~copyright:"Copyright (C) 2005, the HELM team"
+ ~license:(String.concat "\n" (parse_txt_file "LICENSE"))
+ (*?logo:GdkPixbuf.pixbuf*)
+ (*?logo_icon_name:string*)
+ ~name:"Matita"
+ ~version:BuildTimeConf.version
+ ~website:"http://helm.cs.unibo.it"
+ ()
+ in
+ connect_menu_item main#aboutMenuItem about_dialog#present;
(* findRepl win *)
let show_find_Repl () =
findRepl#toplevel#misc#show ();
source_view#source_buffer#redo ();
source_view#misc#grab_focus ()
in
- ignore(self#main#undoMenuItem#connect#activate ~callback:safe_undo);
+ connect_menu_item main#undoMenuItem safe_undo;
ignore(source_view#source_buffer#connect#can_undo
- ~callback:self#main#undoMenuItem#misc#set_sensitive);
- ignore(self#main#redoMenuItem#connect#activate ~callback:safe_redo);
+ ~callback:main#undoMenuItem#misc#set_sensitive);
+ connect_menu_item main#redoMenuItem safe_redo;
ignore(source_view#source_buffer#connect#can_redo
- ~callback:self#main#redoMenuItem#misc#set_sensitive);
+ ~callback:main#redoMenuItem#misc#set_sensitive);
ignore(source_view#connect#after#populate_popup
~callback:(fun pre_menu ->
let menu = new GMenu.menu pre_menu in
new_undoMenuItem#misc#set_sensitive
(undoMenuItem#misc#get_flag `SENSITIVE);
menu#remove (undoMenuItem :> GMenu.menu_item);
- ignore(new_undoMenuItem#connect#activate ~callback:safe_undo);
+ connect_menu_item new_undoMenuItem safe_undo;
let new_redoMenuItem =
GMenu.image_menu_item
~image:(GMisc.image ~stock:`REDO ())
new_redoMenuItem#misc#set_sensitive
(redoMenuItem#misc#get_flag `SENSITIVE);
menu#remove (redoMenuItem :> GMenu.menu_item);
- ignore(new_redoMenuItem#connect#activate ~callback:safe_redo);
- ));
- let clipboard =
- let atom = Gdk.Atom.clipboard in
- GData.clipboard atom in
- ignore(self#main#cutMenuItem#connect#activate
- ~callback:(fun () -> source_view#buffer#cut_clipboard clipboard));
- ignore(self#main#copyMenuItem#connect#activate
- ~callback:(fun () -> source_view#buffer#copy_clipboard clipboard));
- ignore(self#main#pasteMenuItem#connect#activate
- ~callback:(fun () ->
- source_view#buffer#paste_clipboard clipboard;
- (MatitaScript.instance ())#clean_dirty_lock));
- ignore(self#main#deleteMenuItem#connect#activate
- ~callback:(fun () -> ignore (source_view#buffer#delete_selection ())));
- ignore(self#main#findReplMenuItem#connect#activate
- ~callback:show_find_Repl);
- ignore (findRepl#findEntry#connect#activate ~callback:find_forward);
+ connect_menu_item new_redoMenuItem safe_redo));
+ let clipboard = GData.clipboard Gdk.Atom.clipboard in
+ let text_selected () =
+ (source_buffer#get_iter_at_mark `INSERT)#compare
+ (source_buffer#get_iter_at_mark `SEL_BOUND) <> 0
+ in
+ let markup_selected () = MatitaMathView.get_selections () <> None in
+ connect_menu_item main#editMenu (fun () ->
+ let text_selected = text_selected () in
+ let markup_selected = markup_selected () in
+ let something_selected = text_selected || markup_selected in
+ main#cutMenuItem#misc#set_sensitive text_selected;
+ main#copyMenuItem#misc#set_sensitive something_selected;
+ main#deleteMenuItem#misc#set_sensitive text_selected;
+ main#pasteMenuItem#misc#set_sensitive (clipboard#text <> None));
+ connect_menu_item main#cutMenuItem (fun () ->
+ source_view#buffer#cut_clipboard clipboard);
+ connect_menu_item main#copyMenuItem (fun () ->
+ if text_selected () then
+ source_view#buffer#copy_clipboard clipboard
+ else if markup_selected () then
+ match MatitaMathView.get_selections () with
+ | None
+ | Some [] -> ()
+ | Some (s :: _) -> clipboard#set_text s);
+ connect_menu_item main#pasteMenuItem (fun () ->
+ source_view#buffer#paste_clipboard clipboard;
+ (MatitaScript.instance ())#clean_dirty_lock);
+ connect_menu_item main#deleteMenuItem (fun () ->
+ ignore (source_view#buffer#delete_selection ()));
+ connect_menu_item main#selectAllMenuItem (fun () ->
+ source_buffer#move_mark `INSERT source_buffer#start_iter;
+ source_buffer#move_mark `SEL_BOUND source_buffer#end_iter);
+ connect_menu_item main#findReplMenuItem show_find_Repl;
+ ignore (findRepl#findEntry#connect#activate find_forward);
+ (* interface lockers *)
+ let lock_world _ =
+ main#buttonsToolbar#misc#set_sensitive false;
+ develList#buttonsHbox#misc#set_sensitive false;
+ source_view#set_editable false
+ in
+ let unlock_world _ =
+ main#buttonsToolbar#misc#set_sensitive true;
+ develList#buttonsHbox#misc#set_sensitive true;
+ source_view#set_editable true
+ in
+ let locker f =
+ fun () ->
+ lock_world ();
+ try f ();unlock_world () with exc -> unlock_world (); raise exc in
+ let keep_focus f =
+ fun () ->
+ try
+ f (); source_view#misc#grab_focus ()
+ with
+ exc -> source_view#misc#grab_focus (); raise exc in
(* developments win *)
let model =
new MatitaGtkMisc.multiStringListModel
| [[name;_]] -> MatitamakeLib.development_for_name name
| _ -> assert false
in
+ let refresh () =
+ while Glib.Main.pending () do
+ ignore(Glib.Main.iteration false);
+ done
+ in
connect_button develList#newButton
(fun () ->
next_devel_must_contain <- None;
newDevel#toplevel#misc#show());
connect_button develList#deleteButton
- (fun () ->
+ (locker (fun () ->
(match get_devel_selected () with
| None -> ()
- | Some d -> MatitamakeLib.destroy_development d);
- refresh_devels_win ());
- let refresh () =
- while Glib.Main.pending () do
- ignore(Glib.Main.iteration false);
- done
- in
+ | Some d -> MatitamakeLib.destroy_development_in_bg refresh d);
+ refresh_devels_win ()));
connect_button develList#buildButton
- (fun () ->
+ (locker (fun () ->
match get_devel_selected () with
| None -> ()
- | Some d -> ignore(MatitamakeLib.build_development_in_bg refresh d));
+ | Some d ->
+ let build = locker
+ (fun () -> MatitamakeLib.build_development_in_bg refresh d)
+ in
+ ignore(build ())));
connect_button develList#cleanButton
- (fun () ->
+ (locker (fun () ->
match get_devel_selected () with
| None -> ()
- | Some d -> ignore(MatitamakeLib.clean_development_in_bg refresh d));
+ | Some d ->
+ let clean = locker
+ (fun () -> MatitamakeLib.clean_development_in_bg refresh d)
+ in
+ ignore(clean ())));
connect_button develList#closeButton
(fun () -> develList#toplevel#misc#hide());
ignore(develList#toplevel#event#connect#delete
(fun _ -> develList#toplevel#misc#hide();true));
let selected_devel = ref None in
- connect_menu_item self#main#developmentsMenuItem
+ connect_menu_item main#developmentsMenuItem
(fun () -> refresh_devels_win ();develList#toplevel#misc#show ());
(* add development win *)
| `DELETE_EVENT -> return None));
(* menus *)
List.iter (fun w -> w#misc#set_sensitive false) [ main#saveMenuItem ];
- main#helpMenu#set_right_justified true;
(* console *)
let adj = main#logScrolledWin#vadjustment in
ignore (adj#connect#changed
buf#insert ~iter:(buf#get_iter_at_mark (`NAME "locked"))
("\n" ^ GrafiteAstPp.pp_tactic ast)
in
- let tbar = self#main in
+ let tbar = main in
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)));
(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, None, hole)));
- connect_button tbar#autoButton (tac (A.Auto (loc,None,None)));
+ connect_button tbar#autoButton (tac (A.Auto (loc,None,None,None))); (* ALB *)
MatitaGtkMisc.toggle_widget_visibility
- ~widget:(self#main#tacticsButtonsHandlebox :> GObj.widget)
- ~check:self#main#tacticsBarMenuItem;
+ ~widget:(main#tacticsButtonsHandlebox :> GObj.widget)
+ ~check: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;
+ 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;
+ | true -> main#toplevel#fullscreen ()
+ | false -> main#toplevel#unfullscreen ())
+ ~check:main#fullscreenMenuItem;
+ main#fullscreenMenuItem#set_active false;
(* log *)
MatitaLog.set_log_callback self#console#log_callback;
GtkSignal.user_handler :=
let s () = MatitaScript.instance () in
let disableSave () =
script_fname <- None;
- self#main#saveMenuItem#misc#set_sensitive false
+ main#saveMenuItem#misc#set_sensitive false
in
let saveAsScript () =
let script = s () in
script#reset ();
script#assignFileName f;
source_view#source_buffer#begin_not_undoable_action ();
- script#loadFromFile ();
+ script#loadFromFile f;
source_view#source_buffer#end_not_undoable_action ();
console#message ("'"^f^"' loaded.\n");
self#_enableSaveTo f
in
let cursor () =
source_buffer#place_cursor
- (source_buffer#get_iter_at_mark (`NAME "locked"))
- in
- let lock_world _ =
- main#buttonsToolbar#misc#set_sensitive false;
- source_view#set_editable false
- in
- let unlock_world _ =
- main#buttonsToolbar#misc#set_sensitive true;
- source_view#set_editable true
- in
+ (source_buffer#get_iter_at_mark (`NAME "locked")) in
let advance _ = (MatitaScript.instance ())#advance (); cursor () in
let retract _ = (MatitaScript.instance ())#retract (); cursor () in
let top _ = (MatitaScript.instance ())#goto `Top (); cursor () in
let bottom _ = (MatitaScript.instance ())#goto `Bottom (); cursor () in
let jump _ = (MatitaScript.instance ())#goto `Cursor (); cursor () in
- let locker f =
- fun () ->
- lock_world ();
- try f ();unlock_world () with exc -> unlock_world (); raise exc
- in
- let advance = locker advance in
- let retract = locker retract in
- let top = locker top in
- let bottom = locker bottom in
- let jump = locker jump in
+ let advance = locker (keep_focus advance) in
+ let retract = locker (keep_focus retract) in
+ let top = locker (keep_focus top) in
+ let bottom = locker (keep_focus bottom) in
+ let jump = locker (keep_focus jump) in
let connect_key sym f =
- connect_key self#main#mainWinEventBox#event
+ connect_key main#mainWinEventBox#event
~modifiers:[`CONTROL] ~stop:true sym f;
connect_key self#sourceView#event
~modifiers:[`CONTROL] ~stop:true sym f
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;
- connect_button self#main#scriptBottomButton bottom;
+ connect_button main#scriptAdvanceButton advance;
+ connect_button main#scriptRetractButton retract;
+ connect_button main#scriptTopButton top;
+ connect_button main#scriptBottomButton bottom;
connect_key GdkKeysyms._Down advance;
connect_key GdkKeysyms._Up retract;
connect_key GdkKeysyms._Home top;
connect_key GdkKeysyms._End bottom;
- connect_button self#main#scriptJumpButton jump;
- connect_menu_item self#main#openMenuItem loadScript;
- connect_menu_item self#main#saveMenuItem saveScript;
- connect_menu_item self#main#saveAsMenuItem saveAsScript;
- connect_menu_item self#main#newMenuItem newScript;
+ connect_button main#scriptJumpButton jump;
+ connect_menu_item main#openMenuItem loadScript;
+ connect_menu_item main#saveMenuItem saveScript;
+ connect_menu_item main#saveAsMenuItem saveAsScript;
+ connect_menu_item main#newMenuItem newScript;
connect_key GdkKeysyms._period
(fun () ->
source_buffer#insert ~iter:(source_buffer#get_iter_at_mark `INSERT)
(* script monospace font stuff *)
self#updateFontSize ();
(* debug menu *)
- self#main#debugMenu#misc#hide ();
+ main#debugMenu#misc#hide ();
(* status bar *)
- 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");
+ main#hintLowImage#set_file (image_path "matita-bulb-low.png");
+ main#hintMediumImage#set_file (image_path "matita-bulb-medium.png");
+ main#hintHighImage#set_file (image_path "matita-bulb-high.png");
(* focus *)
self#sourceView#misc#grab_focus ();
(* main win dimension *)
let main_w = width * 90 / 100 in
let main_h = height * 80 / 100 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;
+ main#toplevel#resize ~width:main_w ~height:main_h;
+ main#hpaneScriptSequent#set_position script_w;
(* source_view *)
ignore(source_view#connect#after#paste_clipboard
- ~callback:(fun () -> (MatitaScript.instance ())#clean_dirty_lock))
+ ~callback:(fun () -> (MatitaScript.instance ())#clean_dirty_lock));
+ (* clean_locked is set to true only "during" a PRIMARY paste
+ operation (i.e. by clicking with the second mouse button) *)
+ let clean_locked = ref false in
+ ignore(source_view#event#connect#button_press
+ ~callback:
+ (fun button ->
+ if GdkEvent.Button.button button = 2 then
+ clean_locked := true;
+ false
+ ));
+ ignore(source_view#event#connect#button_release
+ ~callback:(fun button -> clean_locked := false; false));
+ ignore(source_view#buffer#connect#after#apply_tag
+ ~callback:(
+ fun tag ~start:_ ~stop:_ ->
+ if !clean_locked &&
+ tag#get_oid = (MatitaScript.instance ())#locked_tag#get_oid
+ then
+ begin
+ clean_locked := false;
+ (MatitaScript.instance ())#clean_dirty_lock;
+ clean_locked := true
+ end));
+ (* math view handling *)
+ connect_menu_item main#newCicBrowserMenuItem (fun () ->
+ ignore (MatitaMathView.cicBrowser ()));
+ connect_menu_item main#increaseFontSizeMenuItem (fun () ->
+ self#increaseFontSize ();
+ MatitaMathView.increase_font_size ();
+ MatitaMathView.update_font_sizes ());
+ connect_menu_item main#decreaseFontSizeMenuItem (fun () ->
+ self#decreaseFontSize ();
+ MatitaMathView.decrease_font_size ();
+ MatitaMathView.update_font_sizes ());
+ connect_menu_item main#normalFontSizeMenuItem (fun () ->
+ self#resetFontSize ();
+ MatitaMathView.reset_font_size ();
+ MatitaMathView.update_font_sizes ());
+ MatitaMathView.reset_font_size ();
method loadScript file =
let script = MatitaScript.instance () in
script#reset ();
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;
- source_view#source_buffer#begin_not_undoable_action ();
- script#loadFromFile ();
- source_view#source_buffer#end_not_undoable_action ();
- console#message ("'"^file^"' loaded.");
- self#_enableSaveTo file
+ let content =
+ if Sys.file_exists file then file
+ else BuildTimeConf.script_template
+ in
+ source_view#source_buffer#begin_not_undoable_action ();
+ script#loadFromFile content;
+ source_view#source_buffer#end_not_undoable_action ();
+ console#message ("'"^file^"' loaded.");
+ self#_enableSaveTo file
method setStar name b =
let l = main#scriptLabel in
script_fname <- Some file;
self#main#saveMenuItem#misc#set_sensitive true
-
method console = console
- method sourceView: GSourceView.source_view = (source_view: GSourceView.source_view)
- method about = about
+ method sourceView: GSourceView.source_view =
+ (source_view: GSourceView.source_view)
method fileSel = fileSel
method findRepl = findRepl
method main = main
keyBindingBoxes
method setQuitCallback callback =
- ignore (main#quitMenuItem#connect#activate callback);
+ connect_menu_item main#quitMenuItem callback;
ignore (main#toplevel#event#connect#delete
(fun _ -> callback ();true));
self#addKeyBinding GdkKeysyms._q callback
let gui () =
let g = new gui () in
gui_instance := Some g;
+ MatitaMathView.set_gui g;
g
let instance = singleton gui
GtkThread.main ();
(match !interp_no with Some row -> [row] | _ -> raise MatitaTypes.Cancel)
+let _ =
+ (* disambiguator callbacks *)
+ MatitaDisambiguator.set_choose_uris_callback (interactive_uri_choice ());
+ MatitaDisambiguator.set_choose_interp_callback (interactive_interp_choice ());
+ (* gtk initialization *)
+ GtkMain.Rc.add_default_file BuildTimeConf.gtkrc_file; (* loads gtk rc *)
+ GMathView.add_configuration_path BuildTimeConf.gtkmathview_conf;
+ ignore (GMain.Main.init ())
+
projects / helm.git / blobdiff