+ 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: GText.buffer) = self#main#scriptTextView#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)));
+ connect_button tbar#elimTypeButton (tac_w_term (A.ElimType (loc, hole)));
+ 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, hole)));
+ connect_button tbar#autoButton (tac (A.Auto (loc,None)));
+ (* 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)));
+ (* script *)
+ 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#loadFrom f;
+ console#message ("'"^f^"' loaded.");
+ self#_enableSaveTo f
+ | None -> ()
+ in
+ let saveAsScript () =
+ let script = s () in
+ match self#chooseFile ~ok_not_exists:true () with
+ | Some f ->
+ script#saveTo f;
+ console#message ("'"^f^"' saved.");
+ self#_enableSaveTo f
+ | None -> ()
+ in
+ let saveScript () =
+ match script_fname with
+ | None -> saveAsScript ()
+ | Some f ->
+ (s ())#saveTo f;
+ console#message ("'"^f^"' saved.");
+ in
+ let newScript () = (s ())#reset (); disableSave () in
+ let cursor () =
+ let buf = self#main#scriptTextView#buffer in
+ buf#place_cursor (buf#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#main#scriptTextView#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 () ->
+ let buf = self#main#scriptTextView#buffer in
+ buf#insert ~iter:(buf#get_iter_at_mark `INSERT) ".\n";
+ advance ());
+ connect_key GdkKeysyms._Return
+ (fun () ->
+ let buf = self#main#scriptTextView#buffer in
+ buf#insert ~iter:(buf#get_iter_at_mark `INSERT) "\n";
+ advance ());
+ (* debug menu *)
+ self#main#debugMenu#misc#hide ();
+ (* status bar *)
+ self#main#hintLowImage#set_file "icons/matita-bulb-low.png";
+ self#main#hintMediumImage#set_file "icons/matita-bulb-medium.png";
+ self#main#hintHighImage#set_file "icons/matita-bulb-high.png";
+ (* focus *)
+ self#main#scriptTextView#misc#grab_focus ()
+
+ method loadScript file =
+ let script = MatitaScript.instance () in
+ script#reset ();
+ script#loadFrom file;
+ console#message ("'"^file^"' loaded.");
+ self#_enableSaveTo file
+
+ method private _enableSaveTo file =
+ script_fname <- Some file;
+ self#main#saveMenuItem#misc#set_sensitive true
+