let gui_instance = ref None ;;
+class type browserWin =
+ (* this class exists only because GEdit.combo_box_entry is not supported by
+ * lablgladecc :-(((( *)
+object
+ inherit MatitaGeneratedGui.browserWin
+ method browserUri: GEdit.combo_box_entry
+end
+
class console ~(buffer: GText.buffer) () =
object (self)
val error_tag = buffer#create_tag [ `FOREGROUND "red" ]
match self#chooseFile ~ok_not_exists:true () with
| Some f ->
script#saveTo f;
- console#message ("'"^f^"' saved.");
+ console#message ("'"^f^"' saved.\n");
self#_enableSaveTo f
| None -> ()
in
| None -> saveAsScript ()
| Some f ->
(s ())#saveTo f;
- console#message ("'"^f^"' saved.");
+ console#message ("'"^f^"' saved.\n");
in
let newScript () = (s ())#reset (); disableSave () in
let cursor () =
let buf = self#main#scriptTextView#buffer in
buf#insert ~iter:(buf#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]
+ 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 *)
(* 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";
+ 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#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
+ let main_w = width * 90 / 100 in
+ let main_h = height * 80 / 100 in
+ let script_w = main_w / 2 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
method main = main
method newBrowserWin () =
- let win = new browserWin () in
- win#check_widgets ();
- win
+ object (self)
+ inherit browserWin ()
+ val combo = GEdit.combo_box_entry ()
+ initializer
+ self#check_widgets ();
+ let combo_widget = combo#coerce in
+ uriHBox#add combo_widget
+ method browserUri = combo
+ end
method newUriDialog () =
let dialog = new uriChoiceDialog () in