X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fmatita%2FDA_FARE;h=6e882cd007d8fcd5a0792b8e6d17daee5c91240f;hb=36660809dcfb90bea480c84997cfb40f347e0f0c;hp=da382c83de74b94a2761ea744a9f9b6c494dc373;hpb=5280ec9794de75e63ffc01bddf1756ebcca02be0;p=helm.git

diff --git a/matita/matita/DA_FARE b/matita/matita/DA_FARE
index da382c83d..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,14 +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 :-( (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