(**********************************************************************)
TODO
+- Guardare il commento
+ (*CSC: this code is suspect and/or bugged: we try first without reduction
+ and then using whd. However, the saturate_term always tries with full
+ reduction without delta. *)
+ in primitiveTactics.ml. Potrebbe essere causa di rallentamento della apply
+ oltre che di bug!
+- 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:
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
projects / helm.git / blobdiff