X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaGui.ml;h=38f8cb7849da4d1af0d5cbf2c5328454c6e8f4da;hb=5022202a659044d981833ba8665424a52684b07f;hp=c1bdfcc77f0d46fc5a4b7e0c20d42a901761ba3c;hpb=6187b40af194fb960d91653682a0eb2096f20f3b;p=helm.git
diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml
index c1bdfcc77..38f8cb784 100644
--- a/helm/matita/matitaGui.ml
+++ b/helm/matita/matitaGui.ml
@@ -1,4 +1,4 @@
-(* Copyright (C) 2004, HELM Team.
+(* Copyright (C) 2004-2005, HELM Team.
*
* This file is part of HELM, an Hypertextual, Electronic
* Library of Mathematics, developed at the Computer Science
@@ -29,38 +29,120 @@ open MatitaGeneratedGui
open MatitaGtkMisc
open MatitaMisc
-class gui file =
+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 "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
+ method error s = buffer#insert ~iter:buffer#end_iter ~tags:[error_tag] s
+ method warning s = buffer#insert ~iter:buffer#end_iter ~tags:[warning_tag] s
+ method debug s = buffer#insert ~iter:buffer#end_iter ~tags:[debug_tag] s
+ method clear () =
+ buffer#delete ~start:buffer#start_iter ~stop:buffer#end_iter
+ method log_callback (tag: MatitaLog.log_tag) s =
+ match tag with
+ | `Debug -> self#debug (s ^ "\n")
+ | `Error -> self#error (s ^ "\n")
+ | `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 toolbar = new toolBarWin ~file () in
- let main = new mainWin ~file () in
- let about = new aboutWin ~file () in
- let fileSel = new fileSelectionWin ~file () in
- let script = new scriptWin ~file () in
+ 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 *)
- [ toolbar#toolBarEventBox; main#mainWinEventBox;
- script#scriptWinEventBox; main#consoleEventBox ]
+ [ main#mainWinEventBox ]
in
- let console =
- MatitaConsole.console ~evbox:main#consoleEventBox
- ~phrase_sep:BuildTimeConf.phrase_sep
- ~packing:main#scrolledConsole#add ~paned:main#mainVPanes ()
+ 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 script_buf = script#scriptTextView#buffer 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
-
- (** text mark and tag representing locked part of a script *)
- val locked_mark =
- script_buf#create_mark ~name:"locked" ~left_gravity:true
- script_buf#start_iter
- val locked_tag =
- script_buf#create_tag [`BACKGROUND "green"; `EDITABLE false]
-
+ 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
+
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 toolbar; c script ]);
+ [ c about; c fileSel; c main; c findRepl]);
(* key bindings *)
List.iter (* global key bindings *)
(fun (key, callback) -> self#addKeyBinding key callback)
@@ -70,11 +152,7 @@ class gui file =
GdkKeysyms._F4,
toggle_win ~check:main#showCheckMenuItem check#checkWin;
*)
- [ GdkKeysyms._F5,
- toggle_win ~check:main#showScriptMenuItem script#scriptWin;
- GdkKeysyms._x, (fun () -> console#toggle ());
- ];
- add_key_binding GdkKeysyms._Escape console#hide main#consoleEventBox;
+ [ ];
(* about win *)
ignore (about#aboutWin#event#connect#delete (fun _ -> true));
ignore (main#aboutMenuItem#connect#activate (fun _ ->
@@ -83,6 +161,196 @@ class gui file =
about#aboutWin#misc#hide ());
about#aboutLabel#set_label (Pcre.replace ~pat:"@VERSION@"
~templ:BuildTimeConf.version about#aboutLabel#label);
+ (* 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));
+ ignore(self#main#undoMenuItem#connect#activate
+ ~callback:(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;
+ source_view#buffer#move_mark `SEL_BOUND ~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 ()
+ ));
+ ignore(source_view#source_buffer#connect#can_undo
+ ~callback:self#main#undoMenuItem#misc#set_sensitive);
+ ignore(self#main#redoMenuItem#connect#activate
+ ~callback:source_view#source_buffer#redo);
+ ignore(source_view#source_buffer#connect#can_redo
+ ~callback:self#main#redoMenuItem#misc#set_sensitive);
+ 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);
+ (* 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 -> ignore(MatitamakeLib.build_development_in_bg refresh d));
+ connect_button develList#cleanButton
+ (fun () ->
+ match get_devel_selected () with
+ | None -> ()
+ | Some d -> ignore(MatitamakeLib.clean_development_in_bg refresh d));
+ 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 ->
@@ -94,59 +362,325 @@ class gui file =
match event with
| `OK ->
let fname = fileSel#fileSelectionWin#filename in
- if is_regular fname then return (Some fname)
+ if Sys.file_exists fname then
+ 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
+ begin
+ if _ok_not_exists then
+ return (Some fname)
+ end
| `CANCEL -> return None
| `HELP -> ()
| `DELETE_EVENT -> return None));
- (* script *)
(* menus *)
- toggle_visibility toolbar#toolBarWin main#showToolBarMenuItem;
-(*
- toggle_visibility proof#proofWin main#showProofMenuItem;
- toggle_visibility check#checkWin main#showCheckMenuItem;
-*)
- toggle_visibility script#scriptWin main#showScriptMenuItem;
- List.iter (fun w -> w#misc#set_sensitive false)
- [ main#saveMenuItem; main#saveAsMenuItem ];
+ List.iter (fun w -> w#misc#set_sensitive false) [ main#saveMenuItem ];
main#helpMenu#set_right_justified true;
- ignore (main#showConsoleMenuItem#connect#activate console#toggle);
- (* main *)
- connect_button main#hideConsoleButton console#hide;
(* console *)
- console#echo_message (sprintf "\tMatita version %s\n"
- BuildTimeConf.version);
- console#echo_prompt ();
- console#misc#grab_focus ();
+ let adj = main#logScrolledWin#vadjustment in
+ 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 = 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" ^ 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" ^ 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, 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));
+ connect_button tbar#existsButton (tac (A.Exists loc));
+ connect_button tbar#reflexivityButton (tac (A.Reflexivity loc));
+ connect_button tbar#symmetryButton (tac (A.Symmetry loc));
+ 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, 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 (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 saveAsScript () =
+ let script = s () in
+ match self#chooseFile ~ok_not_exists:true () with
+ | Some f ->
+ script#assignFileName f;
+ script#saveToFile ();
+ console#message ("'"^f^"' saved.\n");
+ self#_enableSaveTo f
+ | None -> ()
+ in
+ let saveScript () =
+ match script_fname with
+ | None -> saveAsScript ()
+ | Some f ->
+ (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;
+ 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"))
+ 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
+ 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 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;
+ 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 ());
+ (* script monospace font stuff *)
+ self#updateFontSize ();
+ (* debug menu *)
+ self#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");
+ (* 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 * 6 / 10 in
+ self#main#toplevel#resize ~width:main_w ~height:main_h;
+ 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#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;
+ self#main#saveMenuItem#misc#set_sensitive true
+
- method about = about
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 script = script
- method toolbar = toolbar
+ method develList = develList
+ method newDevel = newDevel
method newBrowserWin () =
- let win = new browserWin ~file () 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 ~file () in
+ let dialog = new uriChoiceDialog () in
dialog#check_widgets ();
dialog
method newInterpDialog () =
- let dialog = new interpChoiceDialog ~file () in
+ let dialog = new interpChoiceDialog () in
dialog#check_widgets ();
dialog
method newConfirmationDialog () =
- let dialog = new confirmationDialog ~file () in
+ let dialog = new confirmationDialog () in
dialog#check_widgets ();
dialog
method newEmptyDialog () =
- let dialog = new emptyDialog ~file () in
+ let dialog = new emptyDialog () in
dialog#check_widgets ();
dialog
@@ -155,16 +689,29 @@ class gui file =
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 setPhraseCallback = console#set_callback
+ method chooseFile ?(ok_not_exists = false) () =
+ _ok_not_exists <- ok_not_exists;
+ _only_directory <- false;
+ fileSel#fileSelectionWin#show ();
+ GtkThread.main ();
+ chosen_file
- method chooseFile () =
+ 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
@@ -185,16 +732,181 @@ class gui file =
GtkThread.main ();
!text
- method lockScript offset =
- let mark = `MARK locked_mark in
- script_buf#move_mark mark ~where:(script_buf#get_iter_at_char offset);
- script_buf#remove_tag locked_tag ~start:script_buf#start_iter
- ~stop:script_buf#end_iter;
- script_buf#apply_tag locked_tag ~start:script_buf#start_iter
- ~stop:(script_buf#get_iter_at_mark mark)
+ 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 () = new gui (Helm_registry.get "matita.glade_file")
+let gui () =
+ let g = new gui () in
+ gui_instance := Some g;
+ g
+
let instance = singleton gui
+let non p x = not (p x)
+
+(* this is a shit and should be changed :-{ *)
+let interactive_uri_choice
+ ?(selection_mode:[`SINGLE|`MULTIPLE] = `MULTIPLE) ?(title = "")
+ ?(msg = "") ?(nonvars_button = false) ?(hide_uri_entry=false)
+ ?(hide_try=false) ?(ok_label="_Auto") ?(ok_action:[`SELECT|`AUTO] = `AUTO)
+ ?copy_cb ()
+ ~id uris
+=
+ let gui = instance () 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
+ Lazy.force nonvars_uris
+ else begin
+ let dialog = gui#newUriDialog () in
+ if hide_uri_entry then
+ dialog#uriEntryHBox#misc#hide ();
+ if hide_try then
+ begin
+ dialog#uriChoiceSelectedButton#misc#hide ();
+ dialog#uriChoiceConstantsButton#misc#hide ();
+ end;
+ dialog#okLabel#set_label ok_label;
+ dialog#uriChoiceTreeView#selection#set_mode
+ (selection_mode :> Gtk.Tags.selection_mode);
+ let model = new stringListModel dialog#uriChoiceTreeView in
+ let choices = ref None in
+ let nonvars = ref false in
+ (match copy_cb with
+ | None -> ()
+ | Some cb ->
+ dialog#copyButton#misc#show ();
+ connect_button dialog#copyButton
+ (fun _ ->
+ match model#easy_selection () with
+ | [u] -> (cb u)
+ | _ -> ()));
+ dialog#uriChoiceDialog#set_title title;
+ dialog#uriChoiceLabel#set_text msg;
+ List.iter model#easy_append (List.map UriManager.string_of_uri uris);
+ dialog#uriChoiceConstantsButton#misc#set_sensitive nonvars_button;
+ let return v =
+ choices := v;
+ dialog#uriChoiceDialog#destroy ();
+ GMain.Main.quit ()
+ in
+ ignore (dialog#uriChoiceDialog#event#connect#delete (fun _ -> true));
+ connect_button dialog#uriChoiceConstantsButton (fun _ ->
+ return (Some (Lazy.force nonvars_uris)));
+ if ok_action = `AUTO then
+ connect_button dialog#uriChoiceAutoButton (fun _ ->
+ Helm_registry.set_bool "matita.auto_disambiguation" true;
+ return (Some (Lazy.force nonvars_uris)))
+ else
+ connect_button dialog#uriChoiceAutoButton (fun _ ->
+ match model#easy_selection () with
+ | [] -> ()
+ | uris -> return (Some (List.map UriManager.uri_of_string uris)));
+ connect_button dialog#uriChoiceSelectedButton (fun _ ->
+ match model#easy_selection () with
+ | [] -> ()
+ | uris -> return (Some (List.map UriManager.uri_of_string uris)));
+ connect_button dialog#uriChoiceAbortButton (fun _ -> return None);
+ dialog#uriChoiceDialog#show ();
+ GtkThread.main ();
+ (match !choices with
+ | None -> raise MatitaTypes.Cancel
+ | Some uris -> uris)
+ end
+
+class interpModel =
+ let cols = new GTree.column_list in
+ let id_col = cols#add Gobject.Data.string in
+ let dsc_col = cols#add Gobject.Data.string in
+ let interp_no_col = cols#add Gobject.Data.int in
+ let tree_store = GTree.tree_store cols in
+ let id_renderer = GTree.cell_renderer_text [], ["text", id_col] in
+ let dsc_renderer = GTree.cell_renderer_text [], ["text", dsc_col] in
+ let id_view_col = GTree.view_column ~renderer:id_renderer () in
+ let dsc_view_col = GTree.view_column ~renderer:dsc_renderer () in
+ fun tree_view choices ->
+ object
+ initializer
+ tree_view#set_model (Some (tree_store :> GTree.model));
+ ignore (tree_view#append_column id_view_col);
+ ignore (tree_view#append_column dsc_view_col);
+ let name_of_interp =
+ (* try to find a reasonable name for an interpretation *)
+ let idx = ref 0 in
+ fun interp ->
+ try
+ List.assoc "0" interp
+ with Not_found ->
+ incr idx; string_of_int !idx
+ in
+ tree_store#clear ();
+ let idx = ref ~-1 in
+ List.iter
+ (fun interp ->
+ incr idx;
+ let interp_row = tree_store#append () in
+ tree_store#set ~row:interp_row ~column:id_col
+ (name_of_interp interp);
+ tree_store#set ~row:interp_row ~column:interp_no_col !idx;
+ List.iter
+ (fun (id, dsc) ->
+ let row = tree_store#append ~parent:interp_row () in
+ tree_store#set ~row ~column:id_col id;
+ tree_store#set ~row ~column:dsc_col dsc;
+ tree_store#set ~row ~column:interp_no_col !idx)
+ interp)
+ choices
+
+ method get_interp_no tree_path =
+ let iter = tree_store#get_iter tree_path in
+ tree_store#get ~row:iter ~column:interp_no_col
+ end
+
+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 interp_len = List.length (List.hd choices) in
+ dialog#interpChoiceDialog#set_title "Interpretation choice";
+ dialog#interpChoiceDialogLabel#set_label "Choose an interpretation:";
+ let interp_no = ref None in
+ let return _ =
+ dialog#interpChoiceDialog#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 _ ->
+ match !interp_no with None -> () | Some _ -> return ());
+ connect_button dialog#interpChoiceCancelButton fail;
+ ignore (dialog#interpChoiceTreeView#connect#row_activated (fun path _ ->
+ interp_no := Some (model#get_interp_no path);
+ return ()));
+ let selection = dialog#interpChoiceTreeView#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)
+ | _ -> assert false));
+ dialog#interpChoiceDialog#show ();
+ GtkThread.main ();
+ (match !interp_no with Some row -> [row] | _ -> raise MatitaTypes.Cancel)
+