X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2FDA_FARE;h=6e882cd007d8fcd5a0792b8e6d17daee5c91240f;hb=119da3f9ce130f7c4e8b23fcc491d221472ad657;hp=18dd5614045a38b544b4155eb315f7afdbd6ceeb;hpb=945e4ed3f3d068394ccf8c893fd256e645e2d33a;p=helm.git

diff --git a/matita/matita/DA_FARE b/matita/matita/DA_FARE
index 18dd56140..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,22 +9,25 @@ 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
         aperti
 
 A) passare lo status con il metodo di pretty-printing in giro ovunque
-B) rendere globali le informazioni sull'inclusione :-( e combinarle con il
-   "non caricare oggetti non ancora inclusi" (oppure auto-includere in un
-   qualche modo) per poter ri-compilare un file. Dovrebbe risolvere due scenari:
+B) rendere globali le informazioni sull'inclusione :-( (magari iterando sulla
+   lista dei locali) e combinarle con il "non caricare oggetti non ancora
+   inclusi" per poter ri-compilare un file. Dovrebbe risolvere due scenari:
    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