X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaGui.ml;h=589da7dcc8e9adb6eed32d161a7b9b583ec23b33;hb=e89367d2ad0e194c547a4e84cac87b7a48b69600;hp=fe0b4a1f9870ebd3e314363692b8d55040303bac;hpb=ddff8ae1e15c9fcaf83320978a5cad509d734a74;p=helm.git
diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml
index fe0b4a1f9..589da7dcc 100644
--- a/helm/matita/matitaGui.ml
+++ b/helm/matita/matitaGui.ml
@@ -29,7 +29,7 @@ open MatitaGeneratedGui
open MatitaGtkMisc
open MatitaMisc
-let gui_instance = ref None ;;
+let gui_instance = ref None
class type browserWin =
(* this class exists only because GEdit.combo_box_entry is not supported by
@@ -67,20 +67,21 @@ let clean_current_baseuri status =
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 &&
+ 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 =
- MatitaMisc.obj_file_of_script fname
+ 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?"
- mooname fname)
+ (Filename.basename mooname) (Filename.basename fname))
~parent ()
in
let b =
@@ -101,7 +102,7 @@ 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?")
+ "Do you want to save the script before continuing?")
()
class gui () =
@@ -171,15 +172,13 @@ class gui () =
(*~comments:"comments"*)
~copyright:"Copyright (C) 2005, the HELM team"
~license:(String.concat "\n" (parse_txt_file "LICENSE"))
- (*?logo:GdkPixbuf.pixbuf*)
- (*?logo_icon_name:string*)
+ ~logo:(GdkPixbuf.from_file (MatitaMisc.image_path "/matita_medium.png"))
~name:"Matita"
~version:BuildTimeConf.version
~website:"http://helm.cs.unibo.it"
()
in
- ignore (main#aboutMenuItem#connect#activate
- (fun _ -> about_dialog#present ()));
+ connect_menu_item main#aboutMenuItem about_dialog#present;
(* findRepl win *)
let show_find_Repl () =
findRepl#toplevel#misc#show ();
@@ -219,7 +218,7 @@ class gui () =
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_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 =
@@ -247,7 +246,7 @@ class gui () =
if mark_iter#offset < locked_iter_offset then
begin
source_view#buffer#move_mark `INSERT ~where:mark_iter;
- (MatitaScript.instance ())#goto `Cursor ();
+ (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 *)
@@ -257,7 +256,7 @@ class gui () =
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_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 =
@@ -285,19 +284,19 @@ class gui () =
if mark_iter#offset < locked_iter_offset then
begin
source_view#buffer#move_mark `INSERT ~where:mark_iter;
- (MatitaScript.instance ())#goto `Cursor ();
+ (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
- ignore(self#main#undoMenuItem#connect#activate ~callback:safe_undo);
+ connect_menu_item main#undoMenuItem safe_undo;
ignore(source_view#source_buffer#connect#can_undo
- ~callback:self#main#undoMenuItem#misc#set_sensitive);
- ignore(self#main#redoMenuItem#connect#activate ~callback:safe_redo);
+ ~callback:main#undoMenuItem#misc#set_sensitive);
+ connect_menu_item main#redoMenuItem safe_redo;
ignore(source_view#source_buffer#connect#can_redo
- ~callback:self#main#redoMenuItem#misc#set_sensitive);
+ ~callback:main#redoMenuItem#misc#set_sensitive);
ignore(source_view#connect#after#populate_popup
~callback:(fun pre_menu ->
let menu = new GMenu.menu pre_menu in
@@ -316,7 +315,7 @@ class gui () =
new_undoMenuItem#misc#set_sensitive
(undoMenuItem#misc#get_flag `SENSITIVE);
menu#remove (undoMenuItem :> GMenu.menu_item);
- ignore(new_undoMenuItem#connect#activate ~callback:safe_undo);
+ connect_menu_item new_undoMenuItem safe_undo;
let new_redoMenuItem =
GMenu.image_menu_item
~image:(GMisc.image ~stock:`REDO ())
@@ -326,40 +325,42 @@ class gui () =
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#editMenu#connect#activate
- ~callback:
- (fun () ->
- let something_selected =
- (source_buffer#get_iter_at_mark `INSERT)#compare
- (source_buffer#get_iter_at_mark `SEL_BOUND) <> 0
- in
- self#main#cutMenuItem#misc#set_sensitive something_selected;
- self#main#copyMenuItem#misc#set_sensitive something_selected;
- self#main#deleteMenuItem#misc#set_sensitive something_selected;
- self#main#pasteMenuItem#misc#set_sensitive (clipboard#text <> None)
- ));
- 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#selectAllMenuItem#connect#activate
- ~callback:(fun () ->
- source_buffer#move_mark `INSERT source_buffer#start_iter;
- source_buffer#move_mark `SEL_BOUND source_buffer#end_iter));
- ignore(self#main#findReplMenuItem#connect#activate
- ~callback:show_find_Repl);
- ignore (findRepl#findEntry#connect#activate ~callback:find_forward);
+ connect_menu_item new_redoMenuItem safe_redo));
+ let clipboard = GData.clipboard Gdk.Atom.clipboard in
+ let text_selected () =
+ (source_buffer#get_iter_at_mark `INSERT)#compare
+ (source_buffer#get_iter_at_mark `SEL_BOUND) <> 0
+ in
+ let markup_selected () = MatitaMathView.get_selections () <> None in
+ connect_menu_item main#editMenu (fun () ->
+ let text_selected = text_selected () in
+ let markup_selected = markup_selected () in
+ let something_selected = text_selected || markup_selected in
+ main#cutMenuItem#misc#set_sensitive text_selected;
+ main#copyMenuItem#misc#set_sensitive something_selected;
+ main#deleteMenuItem#misc#set_sensitive text_selected;
+ main#pasteMenuItem#misc#set_sensitive (clipboard#text <> None));
+ connect_menu_item main#cutMenuItem (fun () ->
+ source_view#buffer#cut_clipboard clipboard);
+ connect_menu_item main#copyMenuItem (fun () ->
+ if text_selected () then
+ source_view#buffer#copy_clipboard clipboard
+ else if markup_selected () then
+ match MatitaMathView.get_selections () with
+ | None
+ | Some [] -> ()
+ | Some (s :: _) -> clipboard#set_text s);
+ connect_menu_item main#pasteMenuItem (fun () ->
+ source_view#buffer#paste_clipboard clipboard;
+ (MatitaScript.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;
+ ignore (findRepl#findEntry#connect#activate find_forward);
(* interface lockers *)
let lock_world _ =
main#buttonsToolbar#misc#set_sensitive false;
@@ -395,7 +396,7 @@ class gui () =
let get_devel_selected () =
match model#easy_mselection () with
| [[name;_]] -> MatitamakeLib.development_for_name name
- | _ -> assert false
+ | _ -> None
in
let refresh () =
while Glib.Main.pending () do
@@ -435,7 +436,7 @@ class gui () =
ignore(develList#toplevel#event#connect#delete
(fun _ -> develList#toplevel#misc#hide();true));
let selected_devel = ref None in
- connect_menu_item self#main#developmentsMenuItem
+ connect_menu_item main#developmentsMenuItem
(fun () -> refresh_devels_win ();develList#toplevel#misc#show ());
(* add development win *)
@@ -495,9 +496,9 @@ class gui () =
let fname = fileSel#fileSelectionWin#filename in
if Sys.file_exists fname then
begin
- if is_regular fname && not(_only_directory) then
+ if HExtlib.is_regular fname && not (_only_directory) then
return (Some fname)
- else if _only_directory && is_dir fname then
+ else if _only_directory && HExtlib.is_dir fname then
return (Some fname)
end
else
@@ -518,25 +519,27 @@ class gui () =
(* toolbar *)
let module A = GrafiteAst in
let hole = CicNotationPt.UserInput in
- let loc = Disambiguate.dummy_floc in
+ let loc = DisambiguateTypes.dummy_floc in
let tac ast _ =
- if (MatitaScript.instance ())#onGoingProof () then
- (MatitaScript.instance ())#advance
+ 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" ^ 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, None, [])));
- connect_button tbar#elimTypeButton (tac_w_term (A.ElimType (loc, hole, None, None, [])));
+ 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));
@@ -547,25 +550,28 @@ class gui () =
(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,None))); (* ALB *)
+ 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;
+ | 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 (MatitaExcPp.to_string exn));
+ (fun exn ->
+ if not (Helm_registry.get_bool "matita.debug") then
+ MatitaLog.error (MatitaExcPp.to_string exn)
+ else raise exn);
(* script *)
let _ =
match GSourceView.source_language_from_file BuildTimeConf.lang_file with
@@ -576,10 +582,10 @@ 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
+ main#saveMenuItem#misc#set_sensitive false
in
let saveAsScript () =
let script = s () in
@@ -599,34 +605,36 @@ class gui () =
(s ())#saveToFile ();
console#message ("'"^f^"' saved.\n");
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
- 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 f;
- source_view#source_buffer#end_not_undoable_action ();
- console#message ("'"^f^"' loaded.\n");
- self#_enableSaveTo 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 ();
@@ -637,25 +645,25 @@ class gui () =
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
+ 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
(* quit *)
self#setQuitCallback (fun () ->
- let status = (MatitaScript.instance ())#status in
+ let status = (MatitaScript.current ())#status in
if source_view#buffer#modified then
begin
let rc = ask_unsaved main#toplevel in
@@ -685,19 +693,19 @@ class gui () =
GMain.Main.quit ()
with MatitaTypes.Cancel -> ())
end);
- connect_button self#main#scriptAdvanceButton advance;
- connect_button self#main#scriptRetractButton retract;
- connect_button self#main#scriptTopButton top;
- connect_button self#main#scriptBottomButton bottom;
+ connect_button main#scriptAdvanceButton advance;
+ connect_button main#scriptRetractButton retract;
+ connect_button main#scriptTopButton top;
+ connect_button main#scriptBottomButton bottom;
connect_key GdkKeysyms._Down advance;
connect_key GdkKeysyms._Up retract;
connect_key GdkKeysyms._Home top;
connect_key GdkKeysyms._End bottom;
- connect_button self#main#scriptJumpButton jump;
- connect_menu_item self#main#openMenuItem loadScript;
- connect_menu_item self#main#saveMenuItem saveScript;
- connect_menu_item self#main#saveAsMenuItem saveAsScript;
- connect_menu_item self#main#newMenuItem newScript;
+ connect_button main#scriptJumpButton jump;
+ connect_menu_item main#openMenuItem loadScript;
+ connect_menu_item main#saveMenuItem saveScript;
+ connect_menu_item main#saveAsMenuItem saveAsScript;
+ connect_menu_item main#newMenuItem newScript;
connect_key GdkKeysyms._period
(fun () ->
source_buffer#insert ~iter:(source_buffer#get_iter_at_mark `INSERT)
@@ -711,11 +719,11 @@ class gui () =
(* 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 *)
@@ -724,11 +732,11 @@ 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.instance ())#clean_dirty_lock));
+ ~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
@@ -745,11 +753,11 @@ class gui () =
~callback:(
fun tag ~start:_ ~stop:_ ->
if !clean_locked &&
- tag#get_oid = (MatitaScript.instance ())#locked_tag#get_oid
+ tag#get_oid = (MatitaScript.current ())#locked_tag#get_oid
then
begin
clean_locked := false;
- (MatitaScript.instance ())#clean_dirty_lock;
+ (MatitaScript.current ())#clean_dirty_lock;
clean_locked := true
end));
(* math view handling *)
@@ -769,8 +777,64 @@ class gui () =
MatitaMathView.update_font_sizes ());
MatitaMathView.reset_font_size ();
+ 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#assignFileName file;
let content =
@@ -794,9 +858,9 @@ class gui () =
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 sourceView: GSourceView.source_view =
+ (source_view: GSourceView.source_view)
method fileSel = fileSel
method findRepl = findRepl
method main = main
@@ -820,8 +884,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
@@ -840,7 +904,7 @@ class gui () =
keyBindingBoxes
method setQuitCallback callback =
- ignore (main#quitMenuItem#connect#activate callback);
+ connect_menu_item main#quitMenuItem callback;
ignore (main#toplevel#event#connect#delete
(fun _ -> callback ();true));
self#addKeyBinding GdkKeysyms._q callback
@@ -1033,32 +1097,30 @@ 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)