X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaGui.ml;h=a17b9bfb16942a8c62ba3cda6f6a186f8824fbad;hb=fd372e069bbcaa96dc5b2eef04f341b28850d726;hp=f3b531fb285dee2bc6e60e46044fe1e5177acc12;hpb=aac382f935bc72578119fa7ff9f53c3b649dd0dd;p=helm.git

diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml
index f3b531fb2..a17b9bfb1 100644
--- a/helm/matita/matitaGui.ml
+++ b/helm/matita/matitaGui.ml
@@ -31,6 +31,14 @@ open MatitaMisc
 
 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" ]
@@ -225,14 +233,36 @@ class gui () =
            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
@@ -253,9 +283,16 @@ class gui () =
     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
+          browserHBox#add combo_widget;
+          browserHBox#reorder_child combo_widget ~pos:6
+        method browserUri = combo
+      end
 
     method newUriDialog () =
       let dialog = new uriChoiceDialog () in
@@ -327,10 +364,12 @@ let is_var_uri s =
     String.sub s (String.length s - 4) 4 = ".var"
   with Invalid_argument _ -> false
 
+(* this is a shit and should be changed :-{ *)
 let interactive_uri_choice
   ?(selection_mode:[`SINGLE|`MULTIPLE] = `MULTIPLE) ?(title = "")
   ?(msg = "") ?(nonvars_button = false) ?(hide_uri_entry=false) 
-  ?(hide_try=false) ?(ok_label="_Auto") ?copy_cb ()
+  ?(hide_try=false) ?(ok_label="_Auto") ?(ok_action:[`SELECT|`AUTO] = `AUTO) 
+  ?copy_cb ()
   ~id uris
 =
   let gui = instance () in
@@ -375,9 +414,15 @@ let interactive_uri_choice
     ignore (dialog#uriChoiceDialog#event#connect#delete (fun _ -> true));
     connect_button dialog#uriChoiceConstantsButton (fun _ ->
       return (Some (Lazy.force nonvars_uris)));
-    connect_button dialog#uriChoiceAutoButton (fun _ ->
-      Helm_registry.set_bool "matita.auto_disambiguation" true;
-      return (Some (Lazy.force nonvars_uris)));
+    if ok_action = `AUTO then
+      connect_button dialog#uriChoiceAutoButton (fun _ ->
+        Helm_registry.set_bool "matita.auto_disambiguation" true;
+        return (Some (Lazy.force nonvars_uris)))
+    else
+      connect_button dialog#uriChoiceAutoButton (fun _ ->
+        match model#easy_selection () with
+        | [] -> ()
+        | uris -> return (Some uris));
     connect_button dialog#uriChoiceSelectedButton (fun _ ->
       match model#easy_selection () with
       | [] -> ()