development windows now avoids doing an anction selecting no developments

diff --git a/helm/matita/matita.txt b/helm/matita/matita.txt
index 7e4d747fa9e64fb3a9369b43d230027264a883bb..dd89c7ea4bdf6ad0f9ecd09093b2c67757ea5486 100644 (file)
--- a/helm/matita/matita.txt
+++ b/helm/matita/matita.txt
@@ -63,8 +63,7 @@ TODO
     finestre hanno il focus (e.g. cicBrowser). C'e' gia' da qualche parte il
     codice che aggiunge i keybinding a tutte le eventBox, e' da ripristinare
   - la finestrella per i development ha i pulsanti non sensitive.
-    E' possibile fare "Build" senza selezionare nulla, ottenendo un
-    assert false
+    (* non capisco cosa vuol dire: Gares *)
   - l'entry "Save" da menu non e' context sensitive (ti fa salvare anche
     quando il file non e' stato modificato)
   - finire e rendere piu' compliant (e.g. tags gestiti in maniera anomala)
@@ -121,6 +120,8 @@ TODO
   DEMONI E ALTRO
 
 DONE
+- E' possibile fare "Build" senza selezionare nulla, ottenendo un
+  assert false -> Gares
 - disambiguazione: attualmente io (CSC) ho committato la versione di
   disambiguate.ml che NON ricorda gli alias in caso di disambiguazione
   univoca (senza scelte per l'utente). [ cercare commento "Experimental" ]

diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml
index e0ca8c6816fb88b97bc00e59d7f0122adf408f15..e2e4909428dc56f39c5bbde2edba05caaf9e7a27 100644 (file)
--- a/helm/matita/matitaGui.ml
+++ b/helm/matita/matitaGui.ml
@@ -394,7 +394,7 @@ class gui () =
       let get_devel_selected () = 
         match model#easy_mselection () with
         | [[name;_]] -> MatitamakeLib.development_for_name name
-        | _ -> assert false 
+        | _ -> None
       in
       let refresh () = 
         while Glib.Main.pending () do