[ main#mainWinEventBox ]
in
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 source_buffer = source_view#source_buffer in
object (self)
val mutable chosen_file = None
val mutable _ok_not_exists = false
in
let tac_w_term ast _ =
if (MatitaScript.instance ())#onGoingProof () then
- let (buf: GText.buffer) = self#main#scriptTextView#buffer in
+ let buf = source_buffer in
buf#insert ~iter:(buf#get_iter_at_mark (`NAME "locked"))
("\n" ^ TacticAstPp.pp_tactic ast)
in
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)));
- ignore(self#main#tacticsBarMenuItem#connect#toggled
- ~callback:(fun _ ->
- if self#main#tacticsBarMenuItem#active then
- self#main#tacticsButtonsHandlebox#misc#show ()
- else
- self#main#tacticsButtonsHandlebox#misc#hide ()));
+ 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
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;
(* quit *)
self#setQuitCallback (fun () -> exit 0);
(* log *)
MatitaLog.error
(sprintf "Uncaught exception: %s" (Printexc.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;
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"))
+ 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 connect_key sym f =
connect_key self#main#mainWinEventBox#event
~modifiers:[`CONTROL] ~stop:true sym f;
- connect_key self#main#scriptTextView#event
+ connect_key self#sourceView#event
~modifiers:[`CONTROL] ~stop:true sym f
in
connect_button self#main#scriptAdvanceButton advance;
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 ());
+ source_buffer#insert ~iter:(source_buffer#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 ());
+ source_buffer#insert ~iter:(source_buffer#get_iter_at_mark `INSERT)
+ "\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 =
- self#main#scriptTextView#buffer#create_tag [`FONT_DESC font]
+ source_buffer#create_tag [`FONT_DESC font]
in *)
- self#main#scriptTextView#misc#modify_font_by_name font;
+ self#sourceView#misc#modify_font_by_name font;
(* let _ =
- self#main#scriptTextView#buffer#connect#changed ~callback:(fun _ ->
- let start, stop = self#main#scriptTextView#buffer#bounds in
- self#main#scriptTextView#buffer#apply_tag monospace_tag start stop)
+ source_buffer#connect#changed ~callback:(fun _ ->
+ let start, stop = source_buffer#bounds in
+ source_buffer#apply_tag monospace_tag start stop)
in *)
(* debug menu *)
self#main#debugMenu#misc#hide ();
self#main#hintMediumImage#set_file (image_path "matita-bulb-medium.png");
self#main#hintHighImage#set_file (image_path "matita-bulb-high.png");
(* focus *)
- self#main#scriptTextView#misc#grab_focus ();
+ self#sourceView#misc#grab_focus ();
(* main win dimension *)
let width = Gdk.Screen.width () in
let height = Gdk.Screen.height () in
method console = console
-
+ method sourceView: GSourceView.source_view = (source_view: GSourceView.source_view)
method about = about
method fileSel = fileSel
method main = main