+ (* console *)
+ 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 = TacticAst in
+ let hole = CicAst.UserInput in
+ let loc = CicAst.dummy_floc in
+ let tac ast _ =
+ if (MatitaScript.instance ())#onGoingProof () then
+ (MatitaScript.instance ())#advance
+ ~statement:("\n" ^ TacticAstPp.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)
+ 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 loadScript () =
+ let script = s () in
+ match self#chooseFile () with
+ | Some f ->
+ script#reset ();
+ script#assignFileName f;
+ script#loadFromFile ();
+ 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#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 newScript () = (s ())#reset (); disableSave () 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
+ 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 () ->
+ if source_view#buffer#modified then
+ begin
+ let rc =
+ MatitaGtkMisc.ask_confirmation
+ ~parent:main#toplevel
+ ~title:"Unsaved work!"
+ ~message:("Your work is <b>unsaved</b>!\n\n"^
+ "<i>Do you want to save the script before exiting?</i>")
+ ()
+ in
+ match rc with
+ | `YES -> saveScript ();
+ if not source_view#buffer#modified then
+ GMain.Main.quit ()
+ | `NO -> GMain.Main.quit ()
+ | `CANCEL -> ()
+ end else GMain.Main.quit ());
+ 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
+
+ method loadScript file =
+ let script = MatitaScript.instance () in
+ script#reset ();
+ script#assignFileName file;
+ script#loadFromFile ();
+ 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
+