X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Fmatita.txt;h=d4365d1cc57fb8c1beb552ff3595a723929b8283;hb=358cefe50cccd4cb7d8e2a9cecb7efcb5780b8a3;hp=30a8b535536e679fe8e3dda4ad33a9f5503e9afa;hpb=de9a83f286eee12117fb478ea2db18f7faebac9a;p=helm.git diff --git a/helm/matita/matita.txt b/helm/matita/matita.txt index 30a8b5355..d4365d1cc 100644 --- a/helm/matita/matita.txt +++ b/helm/matita/matita.txt @@ -2,32 +2,54 @@ (**********************************************************************) TODO -- implementare macro in matitaScript.ml (check, hint, ..) -> Gares -- script outline -> Zack +- uri_of_term and term_of_uri: cambiare il tipo per far tornare delle uri!!! +- eta_expand non usata da nessuno? +- eliminare eta_fix? (aspettare notazione da Zack e Luca) +- 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 - cicBrowser: riagganciare(?) resa di termini scritti - nella URL(??) -> -- menu contestuale (tasto dx) nel sequent viewer -> + nella URL(??) -> +- menu contestuale (tasto dx) nel sequent viewer -> - controllo per script modificato o meno prima di uscire -> -- riattaccare hbugs (brrr...) -> Zack -- spostare il codice di creazione delle tabelle da - MatitaDb, al momento quelle create da matita possono - andare out of sync con quelle create dai file .sql +- riattaccare hbugs (brrr...) -> Zack +- tattica clear ? -> Gares DONE -- tree update in background -> Gares -- update del getter in background -> Zack -- agganciare href_callback del sequent_viewer -> Zack -- shortcut varie per script handling -> Zack -- operazioni rimanenti su script (top, bottom, jump) -> Zack -- lighting-ls-getter in matita -> Gares -- riagganciare toolbar -> Zack +- intro = intros 1 -> Gares +- timetravel (urimanager) -> Gares +- implementare macro in matitaScript.ml -> Gares +- history deve aggiornare anche la whelp bar -> Gares +- commenti exeguibili (forse devono essere una lista e non + un singolo executable e forse devono contenere anche Note + e non solo Executable) -> Gares +- spostare il codice di creazione delle tabelle da + MatitaDb, al momento quelle create da matita possono + andare out of sync con quelle create dai file .sql -> Gares +- tree update in background -> Gares +- update del getter in background -> Zack +- agganciare href_callback del sequent_viewer -> Zack +- shortcut varie per script handling -> Zack +- operazioni rimanenti su script (top, bottom, jump) -> Zack +- lighting-ls-getter in matita -> Gares +- riagganciare toolbar -> Zack - evitare che n-mila tattiche Goal siano nello script - (una per ogni cambio di tab) -> Zack -- implementazione comandi rimanenti in matitaEngine.ml -> Gares -- sintassi per gli alias -> Gares -- implementazione script handling (sopra engine) -> Zack + (una per ogni cambio di tab) -> Zack +- implementazione comandi rimanenti in matitaEngine.ml -> Gares +- sintassi per gli alias -> Gares +- implementazione script handling (sopra engine) -> Zack - matitaSync all'indietro -> Gares -- riagganciare GUI -> Zack +- riagganciare GUI -> Zack (**********************************************************************) @@ -52,9 +74,9 @@ comandi: | lingua:/sintassi concreta non ambigua delle tattiche+Qed,Thm,alias/ +---------------------------------------------------------- | engine: TacticAst (cic) -> status -> status - | ma non usa il campo alias dello status + | ma non usa il campo alias dello status ---------+---------------------------------------------------------- - ocaml + ocaml -------------------------------------------------------------------- @@ -133,33 +155,33 @@ script handling - new: gtk_text_buffer -> script - redraw: unit (* ridisegna il contenuto del buffer di testo *) - advance: ?statement:string -> unit -> unit - (* valuta il primo statement del future text (usando eval_statement - (puo' fallire con una eccezione)), rimuove il testo corrispondente dal - future text, aggiunge alla statement list una entry per ogni statement - ritornato da eval_statement, aggiunge il nuovo stato alla state list, - invoka tutti gli observer - Se c'e' l'argomento opzionale statement, quello e' il testo che viene - passato ad eval_statement, se ha successo nessuna rimozione dal future - text viene effettuata *) + (* valuta il primo statement del future text (usando eval_statement + (puo' fallire con una eccezione)), rimuove il testo corrispondente dal + future text, aggiunge alla statement list una entry per ogni statement + ritornato da eval_statement, aggiunge il nuovo stato alla state list, + invoka tutti gli observer + Se c'e' l'argomento opzionale statement, quello e' il testo che viene + passato ad eval_statement, se ha successo nessuna rimozione dal future + text viene effettuata *) - retract: unit -> unit - (* sposta l'ultimo statement della statement list al future text, toglie - l'ultimo stato della state list, MatitaSync.time_travel - ~present:ultimo_stato ~past:stato_precedente *) + (* sposta l'ultimo statement della statement list al future text, toglie + l'ultimo stato della state list, MatitaSync.time_travel + ~present:ultimo_stato ~past:stato_precedente *) - private eval_statement: string -> MatitaTypes.status * string list - (* parsa lo statement - - se e' un Command o un Tactical (vedi TacticAst) invoca MatitaEngine - passando lo stato corrente - - se e' una Macro la gestisce (= tutte le Macro sono implementate qua) - Ritorna una lista di coppie . La proiezione sulla - prima componente rappresenta gli stati da aggiungere alla state list; - quella sulla seconda gli statement da aggiungere alla statement list. - *) + (* parsa lo statement + - se e' un Command o un Tactical (vedi TacticAst) invoca MatitaEngine + passando lo stato corrente + - se e' una Macro la gestisce (= tutte le Macro sono implementate qua) + Ritorna una lista di coppie . La proiezione sulla + prima componente rappresenta gli stati da aggiungere alla state list; + quella sulla seconda gli statement da aggiungere alla statement list. + *) (* gestione degli observer *) - add_observer: (MatitaTypes.status -> unit) -> observer_id - remove_observer: observer_id -> unit (* gestione del salvataggio *) - - save_to: string -> unit (* ridisegna su file *) + - save_to: string -> unit (* ridisegna su file *) - load_from: string -> unit (* retract fino allo stato zero, nuovo stato con future text pari al - contenuto del file passato *) + contenuto del file passato *)