X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Fmatita.txt;h=23bd0c42eec458436252170b98d5df3e3864e03f;hb=828cc3e65c2a6387752f68afc716ff96b790c3eb;hp=899ad7d386d5a2db8b45e35f4c481f68832f6b0b;hpb=a37142e5555346ff3c68d48cfd5be9182125c58d;p=helm.git diff --git a/helm/matita/matita.txt b/helm/matita/matita.txt index 899ad7d38..23bd0c42e 100644 --- a/helm/matita/matita.txt +++ b/helm/matita/matita.txt @@ -6,6 +6,8 @@ TODO genera i_rec e i_rect quando c'e' un argomento ricorsivo. (CSC: manca vincolo aggiuntivo non dipendente dalla sorta per il caso in questione) -> CSC + - bug universi e tipi induttivi + - Set predicativo TATTICHE @@ -44,6 +46,7 @@ TODO GUI GRAFICA + - integrare il famoso logo mancante (anche nell'About dialog) - quando si fa una locate nel cicbrowser viene mangiato un pezzo di testo dalla finestra principale!!! - highlight degli errori di parsing nello script (usando lo sfondo come per la @@ -73,8 +76,8 @@ TODO - riattaccare hbugs (brrr...) -> Zack GUI LOGICA - - matitaclean all (o matitamake cleanall) dovrebbe radere al suolo la - directory .matita + - matitamake foo/a.ma non funziona; bisogna chiamarlo con + matitamake /x/y/z/foo/a.ma - notazione -> Luca e Zack - copiare nel .moo la baseuri e poi il matitaclean la legge da li e non dal .ma (si evita il syntax error e il cambio di una baseuri non causa @@ -82,6 +85,11 @@ TODO - non chiudere transitivamente i moo ?? DONE +- matitaclean deve rimuovere anche i .moo; in alternativa il makefile + non deve basarsi sui .moo per decidere se qualcosa e' stato compilato o meno + -> CSC, Gares +- matitaclean all (o matitamake cleanall) dovrebbe radere al suolo la + directory .matita -> CSC, Gares - icone standard per zoom-in/out/= e piu' aderenza alle Gnome Interface Guidelines (e.g. about dialog) -> CSC - salvare la parte di testo lockata dagli effetti di undo/redo con