buf#insert ~iter:(buf#get_iter_at_mark `INSERT) "\n";
advance ());
(* script monospace font stuff *)
- let font = Pango.Font.from_string "Monospace 10" in
- let monospace_tag =
- self#main#scriptTextView#buffer#create_tag [`FONT_DESC font]
+ let font =
+ Helm_registry.get_opt_default Helm_registry.get
+ BuildTimeConf.default_script_font "matita.script_font"
in
- let _ =
+(* let monospace_tag =
+ self#main#scriptTextView#buffer#create_tag [`FONT_DESC font]
+ in *)
+ self#main#scriptTextView#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)
- in
-
+ in *)
(* debug menu *)
self#main#debugMenu#misc#hide ();
(* status bar *)
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 ();
+ self#main#scriptTextView#misc#grab_focus ();
(* main win dimension *)
let width = Gdk.Screen.width () in
let height = Gdk.Screen.height () in