X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Fmatita.txt;h=adf0e1cf1651cc353a24e461c926adf0b82b63c1;hb=bd6f44797ad9d5b72e2177d885f5e56aaa2bea4d;hp=097eea2d2f94b47a8487c27e8d39e4bb115597e2;hpb=a8b7c2dde5be21864e841bcf2741293e8e0a82e6;p=helm.git diff --git a/helm/matita/matita.txt b/helm/matita/matita.txt index 097eea2d2..adf0e1cf1 100644 --- a/helm/matita/matita.txt +++ b/helm/matita/matita.txt @@ -2,18 +2,18 @@ (**********************************************************************) TODO -- implementare macro in matitaScript.ml (check, hint, ..) -> Gares -- script outline -> Zack +- 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 -- intro di una singola premessa -> Gares -- elim di un goal che e` un'implicazione -> Gares +- riattaccare hbugs (brrr...) -> Zack - tattica clear ? -> Gares DONE +- 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 @@ -21,20 +21,20 @@ DONE - 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 +- 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 (**********************************************************************) @@ -59,9 +59,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 -------------------------------------------------------------------- @@ -140,33 +140,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 *)