From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Tue, 20 Sep 2005 08:07:13 +0000 (+0000)
Subject: development windows now avoids doing an anction selecting no developments
X-Git-Tag: LAST_BEFORE_NEW~89
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=1e9e21091e2e6e899578332f2e67b57fea8e9c0f;p=helm.git

development windows now avoids doing an anction selecting no developments
---

diff --git a/helm/matita/matita.txt b/helm/matita/matita.txt
index 7e4d747fa..dd89c7ea4 100644
--- 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 e0ca8c681..e2e490942 100644
--- 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