X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaGui.ml;h=fe113743b1d0ef7d9cbe7d2e5b9ccf5cd282c98e;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=cdbfc799a054f28e1743e1e941507e240949d22e;hpb=522bfe4fd22804ff7fb0013697721504003a6606;p=helm.git
diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml
index cdbfc799a..fe113743b 100644
--- a/helm/matita/matitaGui.ml
+++ b/helm/matita/matitaGui.ml
@@ -29,7 +29,9 @@ open MatitaGeneratedGui
open MatitaGtkMisc
open MatitaMisc
-let gui_instance = ref None ;;
+exception Found of int
+
+let gui_instance = ref None
class type browserWin =
(* this class exists only because GEdit.combo_box_entry is not supported by
@@ -42,7 +44,7 @@ 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
@@ -58,12 +60,60 @@ 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 () =
+ let moo_fname = MatitacleanLib.obj_file_of_script fname in
+ MatitaMoo.save_moo moo_fname status.MatitaTypes.moo_content_rev in
+ if (MatitaScript.current ())#eos &&
+ status.MatitaTypes.proof_status = MatitaTypes.No_proof
+ then
+ begin
+ let mooname =
+ MatitacleanLib.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?"
+ (Filename.basename mooname) (Filename.basename 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 continuing?")
+ ()
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 newDevelWin () in
let keyBindingBoxes = (* event boxes which should receive global key events *)
[ main#mainWinEventBox ]
in
@@ -85,14 +135,17 @@ class gui () =
object (self)
val mutable chosen_file = None
val mutable _ok_not_exists = false
+ val mutable _only_directory = false
val mutable script_fname = None
val mutable font_size = default_font_size
+ val mutable next_devel_must_contain = None
+ val mutable next_ligatures = []
initializer
(* glade's check widgets *)
List.iter (fun w -> w#check_widgets ())
(let c w = (w :> unit>) in
- [ c about; c fileSel; c main ]);
+ [ c fileSel; c main; c findRepl]);
(* key bindings *)
List.iter (* global key bindings *)
(fun (key, callback) -> self#addKeyBinding key callback)
@@ -104,13 +157,336 @@ class gui () =
*)
[ ];
(* 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.from_file (MatitaMisc.image_path "/matita_medium.png"))
+ ~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 ();
+ findRepl#toplevel#misc#grab_focus ()
+ in
+ let hide_find_Repl () = findRepl#toplevel#misc#hide () in
+ let find_forward _ =
+ let highlight start end_ =
+ source_buffer#move_mark `INSERT ~where:start;
+ source_buffer#move_mark `SEL_BOUND ~where:end_;
+ source_view#scroll_mark_onscreen `INSERT
+ in
+ let text = findRepl#findEntry#text in
+ let iter = source_buffer#get_iter `SEL_BOUND in
+ match iter#forward_search text with
+ | None ->
+ (match source_buffer#start_iter#forward_search text with
+ | None -> ()
+ | Some (start,end_) -> highlight start end_)
+ | Some (start,end_) -> highlight start end_
+ in
+ let replace _ =
+ let text = findRepl#replaceEntry#text in
+ let ins = source_buffer#get_iter `INSERT in
+ let sel = source_buffer#get_iter `SEL_BOUND in
+ if ins#compare sel < 0 then
+ begin
+ ignore(source_buffer#delete_selection ());
+ source_buffer#insert text
+ end
+ in
+ connect_button findRepl#findButton find_forward;
+ connect_button findRepl#findReplButton replace;
+ connect_button findRepl#cancelButton (fun _ -> hide_find_Repl ());
+ ignore(findRepl#toplevel#event#connect#delete
+ ~callback:(fun _ -> hide_find_Repl ();true));
+ let safe_undo =
+ fun () ->
+ (* phase 1: we save the actual status of the marks and we undo *)
+ let locked_mark = `MARK ((MatitaScript.current ())#locked_mark) in
+ let locked_iter = source_view#buffer#get_iter_at_mark locked_mark in
+ let locked_iter_offset = locked_iter#offset in
+ let mark2 =
+ `MARK
+ (source_view#buffer#create_mark ~name:"lock_point"
+ ~left_gravity:true locked_iter) in
+ source_view#source_buffer#undo ();
+ (* phase 2: we save the cursor position and we redo, restoring
+ the previous status of all the marks *)
+ let cursor_iter = source_view#buffer#get_iter_at_mark `INSERT in
+ let mark =
+ `MARK
+ (source_view#buffer#create_mark ~name:"undo_point"
+ ~left_gravity:true cursor_iter)
+ in
+ source_view#source_buffer#redo ();
+ let mark_iter = source_view#buffer#get_iter_at_mark mark in
+ let mark2_iter = source_view#buffer#get_iter_at_mark mark2 in
+ let mark2_iter = mark2_iter#set_offset locked_iter_offset in
+ source_view#buffer#move_mark locked_mark ~where:mark2_iter;
+ source_view#buffer#delete_mark mark;
+ source_view#buffer#delete_mark mark2;
+ (* phase 3: if after the undo the cursor was in the locked area,
+ then we move it there again and we perform a goto *)
+ if mark_iter#offset < locked_iter_offset then
+ begin
+ source_view#buffer#move_mark `INSERT ~where:mark_iter;
+ (MatitaScript.current ())#goto `Cursor ();
+ end;
+ (* phase 4: we perform again the undo. This time we are sure that
+ the text to undo is not locked *)
+ source_view#source_buffer#undo ();
+ source_view#misc#grab_focus () in
+ let safe_redo =
+ fun () ->
+ (* phase 1: we save the actual status of the marks, we redo and
+ we undo *)
+ let locked_mark = `MARK ((MatitaScript.current ())#locked_mark) in
+ let locked_iter = source_view#buffer#get_iter_at_mark locked_mark in
+ let locked_iter_offset = locked_iter#offset in
+ let mark2 =
+ `MARK
+ (source_view#buffer#create_mark ~name:"lock_point"
+ ~left_gravity:true locked_iter) in
+ source_view#source_buffer#redo ();
+ source_view#source_buffer#undo ();
+ (* phase 2: we save the cursor position and we restore
+ the previous status of all the marks *)
+ let cursor_iter = source_view#buffer#get_iter_at_mark `INSERT in
+ let mark =
+ `MARK
+ (source_view#buffer#create_mark ~name:"undo_point"
+ ~left_gravity:true cursor_iter)
+ in
+ let mark_iter = source_view#buffer#get_iter_at_mark mark in
+ let mark2_iter = source_view#buffer#get_iter_at_mark mark2 in
+ let mark2_iter = mark2_iter#set_offset locked_iter_offset in
+ source_view#buffer#move_mark locked_mark ~where:mark2_iter;
+ source_view#buffer#delete_mark mark;
+ source_view#buffer#delete_mark mark2;
+ (* phase 3: if after the undo the cursor is in the locked area,
+ then we move it there again and we perform a goto *)
+ if mark_iter#offset < locked_iter_offset then
+ begin
+ source_view#buffer#move_mark `INSERT ~where:mark_iter;
+ (MatitaScript.current ())#goto `Cursor ();
+ end;
+ (* phase 4: we perform again the redo. This time we are sure that
+ the text to redo is not locked *)
+ source_view#source_buffer#redo ();
+ source_view#misc#grab_focus ()
+ in
+ connect_menu_item main#undoMenuItem safe_undo;
+ ignore(source_view#source_buffer#connect#can_undo
+ ~callback:main#undoMenuItem#misc#set_sensitive);
+ connect_menu_item main#redoMenuItem safe_redo;
+ ignore(source_view#source_buffer#connect#can_redo
+ ~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
+ let menuItems = menu#children in
+ let undoMenuItem, redoMenuItem =
+ match menuItems with
+ [undo;redo;sep1;cut;copy;paste;delete;sep2;
+ selectall;sep3;inputmethod;insertunicodecharacter] -> undo,redo
+ | _ -> assert false in
+ let new_undoMenuItem =
+ GMenu.image_menu_item
+ ~image:(GMisc.image ~stock:`UNDO ())
+ ~use_mnemonic:true
+ ~label:"_Undo"
+ ~packing:(menu#insert ~pos:0) () in
+ new_undoMenuItem#misc#set_sensitive
+ (undoMenuItem#misc#get_flag `SENSITIVE);
+ menu#remove (undoMenuItem :> GMenu.menu_item);
+ connect_menu_item new_undoMenuItem safe_undo;
+ let new_redoMenuItem =
+ GMenu.image_menu_item
+ ~image:(GMisc.image ~stock:`REDO ())
+ ~use_mnemonic:true
+ ~label:"_Redo"
+ ~packing:(menu#insert ~pos:1) () in
+ new_redoMenuItem#misc#set_sensitive
+ (redoMenuItem#misc#get_flag `SENSITIVE);
+ menu#remove (redoMenuItem :> GMenu.menu_item);
+ 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.current ())#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;
+ connect_menu_item main#externalEditorMenuItem self#externalEditor;
+ connect_menu_item main#ligatureButton self#nextLigature;
+ 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
+ ~cols:2 develList#developmentsTreeview
+ in
+ let refresh_devels_win () =
+ model#list_store#clear ();
+ List.iter
+ (fun (name, root) -> model#easy_mappend [name;root])
+ (MatitamakeLib.list_known_developments ())
+ in
+ let get_devel_selected () =
+ match model#easy_mselection () with
+ | [[name;_]] -> MatitamakeLib.development_for_name name
+ | _ -> None
+ 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
+ (locker (fun () ->
+ (match get_devel_selected () with
+ | None -> ()
+ | Some d -> MatitamakeLib.destroy_development_in_bg refresh d);
+ refresh_devels_win ()));
+ connect_button develList#buildButton
+ (locker (fun () ->
+ match get_devel_selected () with
+ | None -> ()
+ | Some d ->
+ let build = locker
+ (fun () -> MatitamakeLib.build_development_in_bg refresh d)
+ in
+ ignore(build ())));
+ connect_button develList#cleanButton
+ (locker (fun () ->
+ match get_devel_selected () with
+ | None -> ()
+ | 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 main#developmentsMenuItem
+ (fun () -> refresh_devels_win ();develList#toplevel#misc#show ());
+
+ (* add development win *)
+ let check_if_root_contains root =
+ match next_devel_must_contain with
+ | None -> true
+ | Some path ->
+ let is_prefix_of d1 d2 =
+ let len1 = String.length d1 in
+ let len2 = String.length d2 in
+ if len2 < len1 then
+ false
+ else
+ let pref = String.sub d2 0 len1 in
+ pref = d1
+ in
+ is_prefix_of root path
+ in
+ connect_button newDevel#addButton
+ (fun () ->
+ let name = newDevel#nameEntry#text in
+ let root = newDevel#rootEntry#text in
+ if check_if_root_contains root then
+ begin
+ ignore (MatitamakeLib.initialize_development name root);
+ refresh_devels_win ();
+ newDevel#nameEntry#set_text "";
+ newDevel#rootEntry#set_text "";
+ newDevel#toplevel#misc#hide()
+ end
+ else
+ MatitaLog.error ("The selected root does not contain " ^
+ match next_devel_must_contain with
+ | Some x -> x
+ | _ -> assert false));
+ connect_button newDevel#chooseRootButton
+ (fun () ->
+ let path = self#chooseDir () in
+ match path with
+ | Some path -> newDevel#rootEntry#set_text path
+ | None -> ());
+ connect_button newDevel#cancelButton
+ (fun () -> newDevel#toplevel#misc#hide ());
+ ignore(newDevel#toplevel#event#connect#delete
+ (fun _ -> newDevel#toplevel#misc#hide();true));
+
(* file selection win *)
ignore (fileSel#fileSelectionWin#event#connect#delete (fun _ -> true));
ignore (fileSel#fileSelectionWin#connect#response (fun event ->
@@ -123,41 +499,51 @@ class gui () =
| `OK ->
let fname = fileSel#fileSelectionWin#filename in
if Sys.file_exists fname then
- (if is_regular fname then return (Some fname))
+ begin
+ if HExtlib.is_regular fname && not (_only_directory) then
+ return (Some fname)
+ else if _only_directory && HExtlib.is_dir fname then
+ return (Some fname)
+ end
else
- (if _ok_not_exists then return (Some fname))
+ begin
+ if _ok_not_exists then
+ return (Some fname)
+ end
| `CANCEL -> return None
| `HELP -> ()
| `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
+ ignore (adj#connect#changed
(fun _ -> adj#set_value (adj#upper -. adj#page_size)));
console#message (sprintf "\tMatita version %s\n" BuildTimeConf.version);
(* toolbar *)
- let module A = TacticAst in
- let hole = CicAst.UserInput in
- let loc = CicAst.dummy_floc in
+ let module A = GrafiteAst in
+ let hole = CicNotationPt.UserInput in
+ let loc = DisambiguateTypes.dummy_floc in
let tac ast _ =
- if (MatitaScript.instance ())#onGoingProof () then
- (MatitaScript.instance ())#advance
- ~statement:("\n" ^ TacticAstPp.pp_tactical (A.Tactic (loc, ast))) ()
+ if (MatitaScript.current ())#onGoingProof () then
+ (MatitaScript.current ())#advance
+ ~statement:("\n" ^ GrafiteAstPp.pp_tactical (A.Tactic (loc, ast)))
+ ()
in
let tac_w_term ast _ =
- if (MatitaScript.instance ())#onGoingProof () then
+ if (MatitaScript.current ())#onGoingProof () then
let buf = source_buffer in
buf#insert ~iter:(buf#get_iter_at_mark (`NAME "locked"))
- ("\n" ^ TacticAstPp.pp_tactic ast)
+ ("\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)));
- 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));
@@ -167,31 +553,31 @@ 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,None,None)));
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;
- (* quit *)
- self#setQuitCallback (fun () -> exit 0);
+ | 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 :=
(fun exn ->
- MatitaLog.error
- (sprintf "Uncaught exception: %s" (Printexc.to_string exn)));
+ if not (Helm_registry.get_bool "matita.debug") then
+ MatitaLog.error (MatitaExcPp.to_string exn)
+ else raise exn);
(* script *)
+ ignore (source_buffer#connect#mark_set (fun _ _ -> next_ligatures <- []));
let _ =
match GSourceView.source_language_from_file BuildTimeConf.lang_file with
| None ->
@@ -201,26 +587,17 @@ class gui () =
source_buffer#set_language matita_lang;
source_buffer#set_highlight true
in
- let s () = MatitaScript.instance () in
+ let s () = MatitaScript.current () 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.\n");
- self#_enableSaveTo f
- | None -> ()
+ main#saveMenuItem#misc#set_sensitive false
in
let saveAsScript () =
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 -> ()
@@ -229,56 +606,120 @@ 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
+ let abandon_script () =
+ let status = (s ())#status in
+ if source_view#buffer#modified then
+ (match ask_unsaved main#toplevel with
+ | `YES -> saveScript ()
+ | `NO -> ()
+ | `CANCEL -> raise MatitaTypes.Cancel);
+ (match script_fname with
+ | None -> ()
+ | Some fname -> ask_and_save_moo_if_needed main#toplevel fname status);
+ in
+ let loadScript () =
+ let script = s () in
+ let status = script#status in
+ try
+ match self#chooseFile () with
+ | Some f ->
+ abandon_script ();
+ script#reset ();
+ script#assignFileName f;
+ source_view#source_buffer#begin_not_undoable_action ();
+ script#loadFromFile f;
+ source_view#source_buffer#end_not_undoable_action ();
+ console#message ("'"^f^"' loaded.\n");
+ self#_enableSaveTo f
+ | None -> ()
+ with MatitaTypes.Cancel -> ()
+ in
+ let newScript () =
+ abandon_script ();
+ source_view#source_buffer#begin_not_undoable_action ();
+ (s ())#reset ();
+ (s ())#template ();
+ source_view#source_buffer#end_not_undoable_action ();
+ disableSave ();
+ script_fname <- None
+ in
let cursor () =
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
- let top _ = (MatitaScript.instance ())#goto `Top (); cursor () in
- let bottom _ = (MatitaScript.instance ())#goto `Bottom (); cursor () in
- let jump _ = (MatitaScript.instance ())#goto `Cursor (); cursor () in
+ (source_buffer#get_iter_at_mark (`NAME "locked")) in
+ let advance _ = (MatitaScript.current ())#advance (); cursor () in
+ let retract _ = (MatitaScript.current ())#retract (); cursor () in
+ let top _ = (MatitaScript.current ())#goto `Top (); cursor () in
+ let bottom _ = (MatitaScript.current ())#goto `Bottom (); cursor () in
+ let jump _ = (MatitaScript.current ())#goto `Cursor (); cursor () 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
in
- 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_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_key GdkKeysyms._period
- (fun () ->
- source_buffer#insert ~iter:(source_buffer#get_iter_at_mark `INSERT)
- ".\n";
- advance ());
- connect_key GdkKeysyms._Return
- (fun () ->
- source_buffer#insert ~iter:(source_buffer#get_iter_at_mark `INSERT)
- "\n";
- advance ());
+ (* quit *)
+ self#setQuitCallback (fun () ->
+ let status = (MatitaScript.current ())#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 main#scriptAdvanceButton advance;
+ connect_button main#scriptRetractButton retract;
+ connect_button main#scriptTopButton top;
+ connect_button main#scriptBottomButton bottom;
+ connect_button main#scriptJumpButton jump;
+ connect_menu_item main#scriptAdvanceMenuItem advance;
+ connect_menu_item main#scriptRetractMenuItem retract;
+ connect_menu_item main#scriptTopMenuItem top;
+ connect_menu_item main#scriptBottomMenuItem bottom;
+ connect_menu_item main#scriptJumpMenuItem 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;
(* 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 *)
@@ -287,26 +728,192 @@ class gui () =
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.current ())#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.current ())#locked_tag#get_oid
+ then
+ begin
+ clean_locked := false;
+ (MatitaScript.current ())#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 private nextLigature () =
+ let iter = source_buffer#get_iter_at_mark `INSERT in
+ let write_ligature len s =
+ source_buffer#delete ~start:iter ~stop:(iter#copy#backward_chars len);
+ source_buffer#insert ~iter:(source_buffer#get_iter_at_mark `INSERT) s
+ in
+ let get_ligature word =
+ let len = String.length word in
+ let aux_tex () =
+ try
+ for i = len - 1 downto 0 do
+ if HExtlib.is_alpha word.[i] then ()
+ else
+ (if word.[i] = '\\' then raise (Found i) else raise (Found ~-1))
+ done;
+ None
+ with Found i ->
+ if i = ~-1 then None else Some (String.sub word i (len - i))
+ in
+ let aux_ligature () =
+ try
+ for i = len - 1 downto 0 do
+ if CicNotationLexer.is_ligature_char word.[i] then ()
+ else raise (Found (i+1))
+ done;
+ raise (Found 0)
+ with
+ | Found i ->
+ (try
+ Some (String.sub word i (len - i))
+ with Invalid_argument _ -> None)
+ in
+ match aux_tex () with
+ | Some macro -> macro
+ | None -> (match aux_ligature () with Some l -> l | None -> word)
+ in
+ (match next_ligatures with
+ | [] -> (* find ligatures and fill next_ligatures, then try again *)
+ let last_word =
+ iter#get_slice
+ ~stop:(iter#copy#backward_find_char Glib.Unichar.isspace)
+ in
+ let ligature = get_ligature last_word in
+ (match CicNotationLexer.lookup_ligatures ligature with
+ | [] -> ()
+ | hd :: tl ->
+ write_ligature (String.length ligature) hd;
+ next_ligatures <- tl @ [ hd ])
+ | hd :: tl ->
+ write_ligature 1 hd;
+ next_ligatures <- tl @ [ hd ])
+
+ method private externalEditor () =
+ let cmd = Helm_registry.get "matita.external_editor" in
+(* ZACK uncomment to enable interactive ask of external editor command *)
+(* let cmd =
+ let msg =
+ "External editor command:
+%f will be substitute for the script name,
+%p for the cursor position in bytes,
+%l for the execution point in bytes."
+ in
+ ask_text ~gui:self ~title:"External editor" ~msg ~multiline:false
+ ~default:(Helm_registry.get "matita.external_editor") ()
+ in *)
+ let fname = (MatitaScript.current ())#filename in
+ let slice mark =
+ source_buffer#start_iter#get_slice
+ ~stop:(source_buffer#get_iter_at_mark mark)
+ in
+ let script = MatitaScript.current () in
+ let locked = `MARK script#locked_mark in
+ let string_pos mark = string_of_int (String.length (slice mark)) in
+ let cursor_pos = string_pos `INSERT in
+ let locked_pos = string_pos locked in
+ let cmd =
+ Pcre.replace ~pat:"%f" ~templ:fname
+ (Pcre.replace ~pat:"%p" ~templ:cursor_pos
+ (Pcre.replace ~pat:"%l" ~templ:locked_pos
+ cmd))
+ in
+ let locked_before = slice locked in
+ let locked_offset = (source_buffer#get_iter_at_mark locked)#offset in
+ ignore (Unix.system cmd);
+ source_buffer#set_text (HExtlib.input_file fname);
+ let locked_iter = source_buffer#get_iter (`OFFSET locked_offset) in
+ source_buffer#move_mark locked locked_iter;
+ source_buffer#apply_tag script#locked_tag
+ ~start:source_buffer#start_iter ~stop:locked_iter;
+ let locked_after = slice locked in
+ let line = ref 0 in
+ let col = ref 0 in
+ try
+ for i = 0 to String.length locked_before - 1 do
+ if locked_before.[i] <> locked_after.[i] then begin
+ source_buffer#place_cursor
+ ~where:(source_buffer#get_iter (`LINEBYTE (!line, !col)));
+ script#goto `Cursor ();
+ raise Exit
+ end else if locked_before.[i] = '\n' then begin
+ incr line;
+ col := 0
+ end
+ done
+ with
+ | Exit -> ()
+ | Invalid_argument _ -> script#goto `Bottom ()
+
method loadScript file =
- let script = MatitaScript.instance () in
+ let script = MatitaScript.current () in
script#reset ();
- script#loadFrom file;
- console#message ("'"^file^"' loaded.");
- self#_enableSaveTo file
+ script#assignFileName 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
+ if b then
+ l#set_text (name ^ " *")
+ else
+ l#set_text (name)
method private _enableSaveTo file =
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
+ method develList = develList
+ method newDevel = newDevel
method newBrowserWin () =
object (self)
@@ -325,8 +932,8 @@ class gui () =
dialog#check_widgets ();
dialog
- method newInterpDialog () =
- let dialog = new interpChoiceDialog () in
+ method newRecordDialog () =
+ let dialog = new recordChoiceDialog () in
dialog#check_widgets ();
dialog
@@ -345,16 +952,30 @@ class gui () =
keyBindingBoxes
method setQuitCallback callback =
- ignore (main#toplevel#connect#destroy 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
method chooseFile ?(ok_not_exists = false) () =
_ok_not_exists <- ok_not_exists;
+ _only_directory <- false;
fileSel#fileSelectionWin#show ();
GtkThread.main ();
chosen_file
+ method private chooseDir ?(ok_not_exists = false) () =
+ _ok_not_exists <- ok_not_exists;
+ _only_directory <- true;
+ fileSel#fileSelectionWin#show ();
+ GtkThread.main ();
+ (* we should check that this is a directory *)
+ chosen_file
+
+ method createDevelopment ~containing =
+ next_devel_must_contain <- containing;
+ newDevel#toplevel#misc#show()
+
method askText ?(title = "") ?(msg = "") () =
let dialog = new textDialog () in
dialog#textDialog#set_title title;
@@ -395,17 +1016,13 @@ class gui () =
let gui () =
let g = new gui () in
gui_instance := Some g;
+ MatitaMathView.set_gui g;
g
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 = "")
@@ -415,7 +1032,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
@@ -446,7 +1063,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;
@@ -464,11 +1081,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 ();
@@ -528,32 +1145,39 @@ class interpModel =
let interactive_interp_choice () choices =
let gui = instance () in
assert (choices <> []);
- let dialog = gui#newInterpDialog () in
- let model = new interpModel dialog#interpChoiceTreeView choices in
+ let dialog = gui#newRecordDialog () in
+ let model = new interpModel dialog#recordChoiceTreeView choices in
let interp_len = List.length (List.hd choices) in
- dialog#interpChoiceDialog#set_title "Interpretation choice";
- dialog#interpChoiceDialogLabel#set_label "Choose an interpretation:";
+ dialog#recordChoiceDialog#set_title "Interpretation choice";
+ dialog#recordChoiceDialogLabel#set_label "Choose an interpretation:";
let interp_no = ref None in
let return _ =
- dialog#interpChoiceDialog#destroy ();
+ dialog#recordChoiceDialog#destroy ();
GMain.Main.quit ()
in
let fail _ = interp_no := None; return () in
- ignore (dialog#interpChoiceDialog#event#connect#delete (fun _ -> true));
- connect_button dialog#interpChoiceOkButton (fun _ ->
+ ignore (dialog#recordChoiceDialog#event#connect#delete (fun _ -> true));
+ connect_button dialog#recordChoiceOkButton (fun _ ->
match !interp_no with None -> () | Some _ -> return ());
- connect_button dialog#interpChoiceCancelButton fail;
- ignore (dialog#interpChoiceTreeView#connect#row_activated (fun path _ ->
+ connect_button dialog#recordChoiceCancelButton fail;
+ ignore (dialog#recordChoiceTreeView#connect#row_activated (fun path _ ->
interp_no := Some (model#get_interp_no path);
return ()));
- let selection = dialog#interpChoiceTreeView#selection in
+ let selection = dialog#recordChoiceTreeView#selection in
ignore (selection#connect#changed (fun _ ->
match selection#get_selected_rows with
- | [path] ->
- MatitaLog.debug (sprintf "selection: %d" (model#get_interp_no path));
- interp_no := Some (model#get_interp_no path)
+ | [path] -> interp_no := Some (model#get_interp_no path)
| _ -> assert false));
- dialog#interpChoiceDialog#show ();
+ dialog#recordChoiceDialog#show ();
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 ())
+