X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaGui.ml;h=90826e98f9f6e72265313c65495798849b5913a3;hb=de4be1b51749200158ffb1984d6da3004b3690a9;hp=c891a0bde63ec069fd9ec1207adde788589aa40a;hpb=5602ae08829342b7c2526053a5cb27cffe8a3d52;p=helm.git
diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml
index c891a0bde..90826e98f 100644
--- a/helm/matita/matitaGui.ml
+++ b/helm/matita/matitaGui.ml
@@ -42,7 +42,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 +58,59 @@ 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 *)
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 keyBindingBoxes = (* event boxes which should receive global key events *)
[ main#mainWinEventBox ]
in
@@ -77,17 +124,24 @@ 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 _only_directory = false
+ val mutable script_fname = None
+ val mutable font_size = default_font_size
+ val mutable next_devel_must_contain = None
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)
@@ -99,13 +153,312 @@ 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 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
+ ignore (main#aboutMenuItem#connect#activate
+ (fun _ -> 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.instance ())#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.instance ())#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.instance ())#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.instance ())#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
+ ignore(self#main#undoMenuItem#connect#activate ~callback: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);
+ ignore(source_view#source_buffer#connect#can_redo
+ ~callback:self#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);
+ ignore(new_undoMenuItem#connect#activate ~callback: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);
+ 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);
+ (* interface lockers *)
+ 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
+ let locker f =
+ fun () ->
+ lock_world ();
+ try f ();unlock_world () with exc -> unlock_world (); 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
+ | _ -> assert false
+ in
+ connect_button develList#newButton
+ (fun () ->
+ next_devel_must_contain <- None;
+ newDevel#toplevel#misc#show());
+ connect_button develList#deleteButton
+ (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
+ connect_button develList#buildButton
+ (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
+ (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 self#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 ->
@@ -118,9 +471,17 @@ 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 is_regular fname && not(_only_directory) then
+ return (Some fname)
+ else if _only_directory && 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));
@@ -129,30 +490,31 @@ class gui () =
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 = Disambiguate.dummy_floc in
let tac ast _ =
if (MatitaScript.instance ())#onGoingProof () then
(MatitaScript.instance ())#advance
- ~statement:("\n" ^ TacticAstPp.pp_tactical (A.Tactic (loc, ast))) ()
+ ~statement:("\n" ^ GrafiteAstPp.pp_tactical (A.Tactic (loc, ast)))
+ ()
in
let tac_w_term ast _ =
if (MatitaScript.instance ())#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
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));
@@ -162,13 +524,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 +540,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
@@ -199,21 +559,12 @@ class gui () =
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 -> ()
- 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 -> ()
@@ -222,10 +573,45 @@ 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 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;
+ source_view#source_buffer#begin_not_undoable_action ();
+ script#loadFromFile ();
+ source_view#source_buffer#end_not_undoable_action ();
+ console#message ("'"^f^"' loaded.\n");
+ self#_enableSaveTo f
+ | None -> ()
+ with MatitaTypes.Cancel -> ()
+ in
+ let newScript () =
+ 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"))
@@ -235,12 +621,49 @@ class gui () =
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 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 connect_key sym f =
connect_key self#main#mainWinEventBox#event
~modifiers:[`CONTROL] ~stop:true sym f;
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;
@@ -265,19 +688,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 *)
@@ -293,14 +704,34 @@ class gui () =
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
+ self#main#hpaneScriptSequent#set_position script_w;
+ (* source_view *)
+ ignore(source_view#connect#after#paste_clipboard
+ ~callback:(fun () -> (MatitaScript.instance ())#clean_dirty_lock))
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;
+ 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
+
+ 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;
@@ -309,9 +740,11 @@ class gui () =
method console = console
method sourceView: GSourceView.source_view = (source_view: GSourceView.source_view)
- method about = about
method fileSel = fileSel
+ method findRepl = findRepl
method main = main
+ method develList = develList
+ method newDevel = newDevel
method newBrowserWin () =
object (self)
@@ -350,15 +783,29 @@ 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) () =
_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
@@ -379,6 +826,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 +853,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 +862,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 +893,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 +911,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 ();