(**********************************************************************)
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:
+ 1. generazione nomi (usa ref incrementata localmente)
+ 2. prodotti dipendenti come non-dipendenti (visibili eseguendo passo
+ passo il test inversion.ma)
+ 3. usato trucco outtype non dipendenti per il case
+- elim_intros_simpl e rewrite_simpl: ora non viene usata dal
+ ^^^^^^ ^^^^^^
+ toplevel la variante che semplifica. Capire quali sono i problemi
+ e/o cosa fare delle varianti con semplificazione.
- eta_expand non usata da nessuno?
-- eliminare eta_fix? (aspettare notazione da Zack e Luca)
+- notazione -> Luca e Zack
+- eliminare eta_fix? (aspettare 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
+- disabilitare (set_sensitive false) menu e bottoni mentre matita sta
+ processando lo script per evitare interazioni pericolose
- bug di ferruccio: fare un refresh dei nomi dopo l'applicazione
di una tattica. Di quali nomi fare refresh? (Andrea) di quelli
veramente ambigui, ovvero dell'ultimo binder tale che sotto di
esso un nome viene usato in maniera ambigua. Esempio:
\lambda x. \lambda x. (x x) (dove una x e' -2) ==> fare refresh
\lambda x. \lambda x. (x x) (dove entrambe sono -1) ==> non fare refresh
-- non eseguire comandi quando lo stato e' diverso da No_proof
-- fare tornare a matitac -1 quando lo stato finale e' diverso da No_proof
- a volte genera termini con variabili legate da piu' binder
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 ->
-- controllo per script modificato o meno prima di uscire ->
+ nella URL(??)
+- menu contestuale (tasto dx) nel sequent viewer -> attende notazione
- riattaccare hbugs (brrr...) -> Zack
-- tattica clear ? -> Gares
+- 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
+- LApply deve prendere in input gli identificatori che va a generare;
+ lascio a Ferruccio la scelta della sintassi concreta -> Ferruccio
+- fare tornare a matitac -1 quando lo stato finale e'
+ diverso da No_proof, non eseguire comandi quando lo
+ stato e' diverso da No_proof -> CSC
+- uri_of_term and term_of_uri: cambiare il tipo per far
+ tornare delle uri!!! -> CSC
- intro = intros 1 -> Gares
- timetravel (urimanager) -> Gares
- implementare macro in matitaScript.ml -> Gares
projects / helm.git / blobdiff