From: Stefano Zacchiroli Date: Fri, 8 Jul 2005 09:46:23 +0000 (+0000) Subject: added some items X-Git-Tag: pre_notation~79 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=338e32925dda5fec7f37ea9ded94cb0ee2e2816b;p=helm.git added some items --- diff --git a/helm/matita/matita.txt b/helm/matita/matita.txt index 94e17c62d..271b854f0 100644 --- a/helm/matita/matita.txt +++ b/helm/matita/matita.txt @@ -11,6 +11,11 @@ TODO oltre che di bug! - 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 - Dare errore significativo al posto di NotWellTypedInterpreation - Implementare menu edit: find/replace/cut/copy/undo/etc. - Bug vari nella generazione dei principi di eliminazione: