...

[helm.git] / helm / matita / matita.txt

diff --git a/helm/matita/matita.txt b/helm/matita/matita.txt
index 5fa4586024835f2291e83dfe6f0bbe2c7a75013c..1bcb2a3428bd1ff37812154dc4653cca425af61b 100644 (file)
--- a/helm/matita/matita.txt
+++ b/helm/matita/matita.txt
@@ -2,6 +2,8 @@
 (**********************************************************************)
 
 TODO
+- Bug di cut&paste: se si fa cut&paste di testo lockato si ottiene testo
+  lockato!
 - Dare errore significativo al posto di NotWellTypedInterpreation
 - Implementare menu edit: find/replace/cut/copy/undo/etc.
 - Bug vari nella generazione dei principi di eliminazione:
@@ -34,12 +36,18 @@ TODO
   Capita quando un tipo dall'environment (e.g. \lambda x.T)
   viene inserito in un contesto (e.g. x:nat) dove le variabili
   sono gia' state legate in precedenza.
-- script outline                                          -> Zack
+- script outline -> Zack
 - cicBrowser: riagganciare(?) resa di termini scritti
-  nella URL(??)                                           ->
-- menu contestuale (tasto dx) nel sequent viewer
-  -> attende notazione
+  nella URL(??)
+- menu contestuale (tasto dx) nel sequent viewer -> attende notazione
 - riattaccare hbugs (brrr...)                             -> Zack
+- gestione dei path per include: il path deve essere assoluto? da decidere ...
+- 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?????)
+- supportare l'apertura di piu' script contemporaneamente in tab/finestre
+  diversi/e
 
 DONE
 - controllo per script modificato o meno prima di uscire  -> Gares