prima implementazione di demodulate, superposition_left e superposition_right

[helm.git] / helm / matita / matitaGui.ml

diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml
index 50d3f8ce8b046b9d338deb77f68af70462cc7f5d..34238f80d4e66cb199d7c0f232f4b6dfb0c29f65 100644 (file)
--- 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" ]
@@ -175,7 +183,7 @@ class gui () =
         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
@@ -184,7 +192,7 @@ class gui () =
         | 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 () =
@@ -226,24 +234,27 @@ class gui () =
            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#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
@@ -272,9 +283,15 @@ 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
+          uriHBox#add combo_widget
+        method browserUri = combo
+      end
 
     method newUriDialog () =
       let dialog = new uriChoiceDialog () in