X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fmatita%2Fmatita.txt;h=c7bf99899d9d04846a9ecc16d2fbad5d4a6c8803;hb=cec61c8b027b15b98d308cee8900d9cf35a02d28;hp=23bd0c42eec458436252170b98d5df3e3864e03f;hpb=828cc3e65c2a6387752f68afc716ff96b790c3eb;p=helm.git diff --git a/helm/matita/matita.txt b/helm/matita/matita.txt index 23bd0c42e..c7bf99899 100644 --- a/helm/matita/matita.txt +++ b/helm/matita/matita.txt @@ -47,11 +47,6 @@ 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 - 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 @@ -59,32 +54,45 @@ TODO - 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. + - finire e rendere piu' compliant (e.g. tags gestiti in maniera anomala) + il Cic Browser + - la barra di stato: c'e' ma non funziona? - - 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) + - menu contestuale (tasto dx) nel sequent viewer - 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) + - che farne della palette delle tattiche? - script outline -> Zack - - riattaccare hbugs (brrr...) -> Zack + - riattaccare hbugs (brrr...) -> Zack GUI LOGICA + - disambiguazione: attualmente io (CSC) ho committato la versione di + disambiguate.ml che NON ricorda gli alias in caso di disambiguazione + univoca (senza scelte per l'utente). [ cercare commento "Experimental" ] + Il problema di questa soluzione e' che rallenta in maniera significativa + l'esecuzione degli script. DOMANDA: quanto costano le fasi di + fetch/decode/execute delle linee dello script? + Una possibile alternativa e' avere alias "soft": se la disambiguazione + fallisce gli alias soft vengono ripuliti e si riprova. - 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 - sporcizia) - non chiudere transitivamente i moo ?? DONE +- bug di refresh del widget quando si avanza ("swap" tra la finestra dei + sequenti e la finestra dello script) -> CSC +- sensitiveness per goto begin/end/etc. (???) -> Gares +- cut&paste stile "X": rimane la parte blu e lockata! -> CSC +- highlight degli errori di parsing nello script -> CSC +- quando si fa una locate nel cicbrowser viene mangiato un pezzo di testo + dalla finestra principale!!! -> CSC +- sensitiveness per copy/paste/cut/delete nel menu Edit -> CSC +- fare "matita foo" (dove foo non esiste), cambiare qualcosa e uscire senza + salvare. In verita' foo e' stato scritto lo stesso! -> CSC - 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