X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2FDA_FARE;h=6e882cd007d8fcd5a0792b8e6d17daee5c91240f;hb=8f1a123e61ff079b1f9ad63cc915470ec7e6abf3;hp=a7e244f2249a4757dca4be4d1f9b80168172c236;hpb=3ab6d253fd09344c0f277757ac8a4b32ed4d4e16;p=helm.git

diff --git a/matita/matita/DA_FARE b/matita/matita/DA_FARE
index a7e244f22..6e882cd00 100644
--- a/matita/matita/DA_FARE
+++ b/matita/matita/DA_FARE
@@ -1,5 +1,6 @@
 MATITA 1.0:
   matitaMathView*: selezione semantica, hyperlink, etc.
+  coercion declaration has no "nocomposites" option, and no compact syntax.
 
 Problemi (MATITA 1.0):
   matitaEngine: durante la compilazione, che accade allo storage/env? dovrei
@@ -8,13 +9,6 @@ Problemi (MATITA 1.0):
   matitaGui: come faccio in uno stato funzionale a settare le interpretazioni?
    dovrei farlo su ogni elemento della history, ma sarebbe troppo costoso
 
-  matita.ml: non posso usare l'high level pretty printer perche' non ho nemmeno
-   uno status dove voglio stampare (e sarebbe comunque troppo basso).
-   Non posso implementare l'up-cast con
-   il solito metodo perche' uso oggetti funzionali. E inoltre ho stati
-   multipli per via del MTI. Di contro, la parte dello stato che si occupa
-   di notazione e' praticamente read-only.
-
 matitac: non entra nelle dir
 matita: due file anonimi stessa base uri
 matita: il pulsante close non si ingrigisce quando non ci sono piu' script
@@ -27,3 +21,13 @@ B) rendere globali le informazioni sull'inclusione :-( (magari iterando sulla
    1) A -> C, B -> C, C e' caricato, carico oggetti di C, B carica C
       ricompilandolo e mischio oggetti
    2) A -> C, edito A, torno in cima ad A, apro C, non mi fa editare C
+
+Bug: si chiude un tab ma resta il suo status :-) specie se e' l'ultimo tab
+
+Idea (Enrico):
+ - ogni oggetto ha il suo status con il suo env che e' una vista su quella
+   globale
+ - c'e' poi l'env attuale globale che e' una cache condivisa del disco;
+   oggetti nella cache del disco sono coppie uri/data;
+   funziona bene se combinato con "carica tutti gli oggetti all'include";
+   funziona bene se combinato con cambio universi e/o assiomi