X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fmatita%2Fmatita.txt;h=67cc45c5a11820749a74253295b5f53536bd8b81;hb=dc861d214cb992a898f81752614201b8074eef12;hp=92626557c11550148ccb4eb6485bb8e05cf3f5c1;hpb=8df7fb956e77d5863338587ac3fdd5f46669d331;p=helm.git diff --git a/helm/matita/matita.txt b/helm/matita/matita.txt index 92626557c..67cc45c5a 100644 --- a/helm/matita/matita.txt +++ b/helm/matita/matita.txt @@ -47,25 +47,17 @@ 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 script uno stato appartiene) - - Implementare menu edit: cut/copy/undo/etc. - keybinding globali: CTRL-{su,giu,...} devono fungere anche quando altre finestre hanno il focus (e.g. cicBrowser). C'e' gia' da qualche parte il 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 @@ -74,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 @@ -87,6 +80,14 @@ 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 - freeze durante avanzamento -> Gares, CSC