X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Fmatita.txt;h=38e204aa27f9ca8556a3eeacf569d9ff28b59e7b;hb=1bcad789810fd37d346e690f18557aeedc6fe08c;hp=5f213100acf2dbcd3debad1c3e81129e84b3f12b;hpb=8146c38b7a6658c03fcf825ba7dd25b7c824f499;p=helm.git diff --git a/helm/matita/matita.txt b/helm/matita/matita.txt index 5f213100a..38e204aa2 100644 --- a/helm/matita/matita.txt +++ b/helm/matita/matita.txt @@ -22,8 +22,6 @@ TODO in primitiveTactics.ml. Potrebbe essere causa di rallentamento della apply oltre che di bug! - Dare errore significativo al posto di NotWellTypedInterpreation -> CSC - - Bug nella generazione dei principi di eliminazione: - 1. generazione nomi (usa ref incrementata localmente) - elim_intros_simpl e rewrite_simpl: ora non viene usata dal ^^^^^^ ^^^^^^ toplevel la variante che semplifica. Capire quali sono i problemi @@ -46,53 +44,64 @@ TODO GUI GRAFICA - - bug di refresh del widget quando si avanza ("swap" tra la finestra dei - sequenti e la finestra dello script) - - feedback su hyperlink nei sequenti e nel browser: rendere visibili gli - 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) - - Implementare menu edit: find/replace/cut/copy/undo/etc. + - icone standard per zoom-in/out/= + - 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) - 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) - - Bug di cut&paste: se si fa cut&paste di testo lockato si ottiene testo - lockato! - 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 - - quando si sposta il punto di esecuzione dello script cambiare la parte di - script visibile nella finestra dello script (finche' l'utente non lo - modifica lui, tipo agendo sulla scrollbar) - fare "matita foo" (dove foo non esiste), cambiare qualcosa e uscire senza salvare. In verita' foo e' stato scritto lo stesso! - - script outline -> Zack + - sensitiveness per copy/paste/cut/delete nel menu Edit + - menu contestuale (tasto dx) nel sequent viewer -> attende notazione + - bug di refresh del widget quando si avanza ("swap" tra la finestra dei + sequenti e la finestra dello script) + - feedback su hyperlink nei sequenti e nel browser: rendere visibili gli + 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) + - script outline -> Zack - riattaccare hbugs (brrr...) -> Zack - - 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) - - salvare la parte di testo lockata dagli effetti di undo/redo (come?????) - con ctrl-Z GUI LOGICA - matitaclean all (o matitamake cleanall) dovrebbe radere al suolo la directory .matita - - tornare indietro (verso il cursore) in matita dovrebbe essere O(1) e non un - Undo passo passo (sembra che il collo di bottiglia sia fare iterare su ogni - uri da togliere (accorpare almeno il lavoro sul db magari aiuta). - - freeze durante avanzamento - notazione -> Luca e Zack - - gestione dei path per include: il path deve essere assoluto? da decidere ... - ( -I ?? o chiedere a matitamake la root e farci una find? ) + - 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 + sporcizia) + - non chiudere transitivamente i moo ?? DONE +- 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 +- tornare indietro (verso il cursore) in matita dovrebbe essere O(1) e non un + Undo passo passo (sembra che il collo di bottiglia sia fare iterare su ogni + uri da togliere (accorpare almeno il lavoro sul db magari aiuta) -> Gares, CSC +- quando si sposta il punto di esecuzione dello script cambiare la parte di + script visibile nella finestra dello script -> Gares, CSC +- find & replace -> Gares +- Bug di cut&paste: se si fa cut&paste di testo lockato si ottiene testo + lockato! -> Gares - Bug: non disambigua inductive i (x:nat) : bool \to Prop \def K : bool \to (i x true) \to (i x false). perche' non inserisce nat nel domain di disambiguazione. Deve esserci un bug stupido da qualche parte -> CSC - Bug vari nella generazione dei principi di eliminazione: + 1. generazione nomi (usa ref incrementata localmente) -> Andrea 2. prodotti dipendenti come non-dipendenti (visibili eseguendo passo passo il test inversion.ma) -> CSC, Gares 3. usato trucco outtype non dipendenti per il case -> CSC, Gares