X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Fmatita.txt;h=67cc45c5a11820749a74253295b5f53536bd8b81;hb=dc861d214cb992a898f81752614201b8074eef12;hp=2af7046457d42ab3ad9ec4c6b57e58739000320a;hpb=83f44ffec0422dbad242b56d651a6e56ce24ddd8;p=helm.git diff --git a/helm/matita/matita.txt b/helm/matita/matita.txt index 2af704645..67cc45c5a 100644 --- a/helm/matita/matita.txt +++ b/helm/matita/matita.txt @@ -47,15 +47,6 @@ TODO - highlight degli errori di parsing nello script (usando lo sfondo come per la parte lockata di testo, da ripulire quando si modifica il testo o si sposta il punto di esecuzione) - - fare in modo che il testo caricato inizialmente da matita non sia - undoable (usando i metodi begin/end_not_undoable_action di gtk_source_view) - - salvare la parte di testo lockata dagli effetti di undo/redo (come?????) - con ctrl-Z. Una possibilita' e' usare la coppia - begin/end_not_undoable_action di gtk_source_view nella moveMark (visto - che la coppia fa anche clear completo dello stack di Undo). Un'alternativa - differente (ma sicuramente piu' complessa e forse poco utile) e' trovare - il modo di fare undo logico fino a quando il posto dove fare undo fisico - (qual'e'?) ma ignoro come si potrebbe fare. - invertibilita' dell'inserimento automatico di alias: quando si torna su bisognerebbe tornare su di un passo e non fare undo degli alias (Zack: nella history ci sono anche gli offset per sapere a che pezzo di @@ -65,6 +56,8 @@ TODO codice che aggiunge i keybinding a tutte le eventBox, e' da ripristinare - fare "matita foo" (dove foo non esiste), cambiare qualcosa e uscire senza salvare. In verita' foo e' stato scritto lo stesso! + - sensitiveness per copy/paste/cut/delete nel menu Edit + - sensitiveness per goto begin/end/etc. - menu contestuale (tasto dx) nel sequent viewer -> attende notazione - bug di refresh del widget quando si avanza ("swap" tra la finestra dei @@ -73,6 +66,7 @@ TODO hyperlink (cursore a "manina"? hyperlink evidenziati?). La maction che collassa la prova e' fastidiosa: la prova si chiude se non si clicca correttamente su un hyperlink (anche tooltip sui bottoni) + - che farne della palette delle tattiche? - script outline -> Zack - riattaccare hbugs (brrr...) -> Zack @@ -86,6 +80,13 @@ TODO - non chiudere transitivamente i moo ?? DONE +- 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 + (shift-)ctrl-Z e anche usando il menu che si apre con il tasto destro -> CSC +- fare in modo che il testo caricato inizialmente da matita non sia + undoable (usando i metodi begin/end_not_undoable_action di gtk_source_view) + -> Gares - Implementare menu edit: cut/copy/undo/etc. -> CSC - gestione dei path per include: il path deve essere assoluto? da decidere ... ( -I ?? o chiedere a matitamake la root e farci una find? ) -> Gares