- set monospace buffer using modify_font widget method

- added configuration key for user defined font and built time default

diff --git a/helm/matita/Makefile.in b/helm/matita/Makefile.in
index f584ec84010aac92c7e85b9f88732f162439779b..51c1bed06aac29626eab1eb575166198a27c5bee 100644 (file)
--- a/helm/matita/Makefile.in
+++ b/helm/matita/Makefile.in
@@ -41,14 +41,14 @@ CCMOS =                             \
        matitaDisambiguator.cmo \
        matitaEngine.cmo
 
-LIB_DEPS = $(shell $(OCAMLFIND) query -recursive -predicates "byte" -format "%d/%a" $(REQUIRES))
 
 all: matita matitac cicbrowser
 
 ifeq ($(HAVE_OCAMLOPT),yes)
 CMXS = $(patsubst %.cmo,%.cmx,$(CMOS))
 CCMXS = $(patsubst %.cmo,%.cmx,$(CCMOS))
-LIBX_DEPS = $(shell $(OCAMLFIND) query -recursive -predicates "native" -format "%d/%a" $(REQUIRES))
+LIB_DEPS := $(shell $(OCAMLFIND) query -recursive -predicates "byte" -format "%d/%a" $(REQUIRES))
+LIBX_DEPS := $(shell $(OCAMLFIND) query -recursive -predicates "native" -format "%d/%a" $(REQUIRES))
 opt: matita.opt matitac.opt cicbrowser.opt
 else
 opt:

diff --git a/helm/matita/buildTimeConf.ml.in b/helm/matita/buildTimeConf.ml.in
index 98c033fdbc10b5dd932afa6d70da6e58a69ccc9f..bff7ad6aab43e4292139db4d1b1d436a3fbfddd3 100644 (file)
--- a/helm/matita/buildTimeConf.ml.in
+++ b/helm/matita/buildTimeConf.ml.in
@@ -33,4 +33,5 @@ let base_uri = "cic:/matita";;
 let phrase_sep = ".";;
 let blank_uri = "about:blank";;
 let current_proof_uri = "about:current_proof";;
+let default_script_font = "Monospace 10";;
 

diff --git a/helm/matita/matita.conf.xml b/helm/matita/matita.conf.xml
index 07887c6bd42adfc351a4c1ca1ce16c52fb0e524a..b4e6d0ff01f714e3e7369ea592c6b7abfc50b316 100644 (file)
--- a/helm/matita/matita.conf.xml
+++ b/helm/matita/matita.conf.xml
@@ -6,6 +6,7 @@
     <key name="baseuri">cic:/matita/</key>
     <key name="basedir">.matita/xml</key>
     <key name="owner">gares</key>
+<!--     <key name="script_font">Monospace 10</key> -->
   </section>
   <section name="db">
     <!-- <key name="host">localhost</key> -->

diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml
index 50d3f8ce8b046b9d338deb77f68af70462cc7f5d..2844aa92e5ce6b8666369e5aa4a549ed603ed851 100644 (file)
--- a/helm/matita/matitaGui.ml
+++ b/helm/matita/matitaGui.ml
@@ -226,16 +226,19 @@ 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 *)
@@ -243,7 +246,7 @@ 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