From: Claudio Sacerdoti Coen Date: Mon, 3 Jan 2011 14:02:29 +0000 (+0000) Subject: ... X-Git-Tag: make_still_working~2607 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=3ab6d253fd09344c0f277757ac8a4b32ed4d4e16;p=helm.git ... --- diff --git a/matita/matita/DA_FARE b/matita/matita/DA_FARE index 18dd56140..a7e244f22 100644 --- a/matita/matita/DA_FARE +++ b/matita/matita/DA_FARE @@ -21,9 +21,9 @@ 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