]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/matita/matitaGui.ml
some cosmetic fixes
[helm.git] / helm / matita / matitaGui.ml
index 4c53c5abcedf8aee75987435c0520ce1fb800f98..50d3f8ce8b046b9d338deb77f68af70462cc7f5d 100644 (file)
@@ -243,7 +243,15 @@ class gui () =
       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
+      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