From 4b84dd78aa6b596a0d3ee38745890ff65efa8b10 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 1 Jun 2005 11:08:38 +0000 Subject: [PATCH] some cosmetic fixes --- helm/matita/matita.glade | 8 ++-- helm/matita/matita.txt | 84 ++++++++++++++++++------------------- helm/matita/matitaEngine.ml | 5 ++- helm/matita/matitaGui.ml | 10 ++++- helm/matita/matitaLog.ml | 10 ++--- helm/matita/matitaScript.ml | 4 +- 6 files changed, 66 insertions(+), 55 deletions(-) diff --git a/helm/matita/matita.glade b/helm/matita/matita.glade index 7ae1860d5..2e2ef874e 100644 --- a/helm/matita/matita.glade +++ b/helm/matita/matita.glade @@ -1261,7 +1261,7 @@ Copyright (C) 2005, True Intros True - intros + intro True GTK_RELIEF_NORMAL True @@ -1838,12 +1838,12 @@ Copyright (C) 2005, - + True True - + 400 True False @@ -2044,7 +2044,7 @@ Copyright (C) 2005, - + True True True diff --git a/helm/matita/matita.txt b/helm/matita/matita.txt index 097eea2d2..454a13029 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 +- intro = intros 1 -> Gares +- timetravel -> gares DONE +- 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 *) diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml index 0496076e7..10fe24030 100644 --- a/helm/matita/matitaEngine.ml +++ b/helm/matita/matitaEngine.ml @@ -1,8 +1,9 @@ open Printf - open MatitaTypes +let debug = true ;; +let debug_print = if debug then prerr_endline else ignore ;; (** create a ProofEngineTypes.mk_fresh_name_type function which uses given * names as long as they are available, then it fallbacks to name generation @@ -253,7 +254,7 @@ let eval_command status cmd = in {status with proof_status = No_proof} | TacticAst.Theorem (_, _, None, _, _) -> - command_error "The grammas should avoid having unnamed theorems!" + command_error "The grammar should avoid having unnamed theorems!" | TacticAst.Coercion (loc, term) -> assert false (** TODO *) | TacticAst.Alias (loc, spec) -> match spec with diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml index 4c53c5abc..50d3f8ce8 100644 --- a/helm/matita/matitaGui.ml +++ b/helm/matita/matitaGui.ml @@ -243,7 +243,15 @@ class gui () = self#main#hintMediumImage#set_file "icons/matita-bulb-medium.png"; self#main#hintHighImage#set_file "icons/matita-bulb-high.png"; (* focus *) - self#main#scriptTextView#misc#grab_focus () + self#main#scriptTextView#misc#grab_focus (); + (* main win dimension *) + let width = Gdk.Screen.width () in + let height = Gdk.Screen.height () in + let main_w = width * 90 / 100 in + let main_h = height * 80 / 100 in + let script_w = main_w / 2 in + self#main#toplevel#resize ~width:main_w ~height:main_h; + self#main#hpaneScriptSequent#set_position script_w method loadScript file = let script = MatitaScript.instance () in diff --git a/helm/matita/matitaLog.ml b/helm/matita/matitaLog.ml index 02afaf9db..8c2e9a7a5 100644 --- a/helm/matita/matitaLog.ml +++ b/helm/matita/matitaLog.ml @@ -33,11 +33,11 @@ colors=(black red green yellow blue magenta cyan gray white) ccodes=(30 31 32 33 34 35 36 37 39) *) -let green = "" -let blue = "" -let yellow = "" -let red = "" -let black = "" +let blue = "" +let yellow = "" +let green = "" +let red = "" +let black = "" let default_callback tag s = let prefix = diff --git a/helm/matita/matitaScript.ml b/helm/matita/matitaScript.ml index f9855348a..99b7018e4 100644 --- a/helm/matita/matitaScript.ml +++ b/helm/matita/matitaScript.ml @@ -24,9 +24,11 @@ *) open Printf - open MatitaTypes +let debug = true +let debug_print = if debug then prerr_endline else ignore + (** raised when one of the script margins (top or bottom) is reached *) exception Margin -- 2.39.2