From b60666721441e676081a6e3b2f436b23dbcdae0f Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 6 Jul 2005 12:45:57 +0000 Subject: [PATCH] added script template added test for absurd --- helm/matita/buildTimeConf.ml.in | 1 + helm/matita/matita.ma.templ | 16 ++++++++++++++++ helm/matita/matitaGui.ml | 8 ++++++-- helm/matita/matitaScript.ml | 8 +++++++- helm/matita/matitaScript.mli | 1 + helm/matita/tests/absurd.ma | 27 +++++++++++++++++++++++++++ 6 files changed, 58 insertions(+), 3 deletions(-) create mode 100644 helm/matita/matita.ma.templ create mode 100644 helm/matita/tests/absurd.ma diff --git a/helm/matita/buildTimeConf.ml.in b/helm/matita/buildTimeConf.ml.in index bc3466a69..acb2a3feb 100644 --- a/helm/matita/buildTimeConf.ml.in +++ b/helm/matita/buildTimeConf.ml.in @@ -39,4 +39,5 @@ let runtime_base_dir = "@RT_BASE_DIR@";; let images_dir = runtime_base_dir ^ "/icons" let gtkrc_file = runtime_base_dir ^ "/matita.gtkrc" let lang_file = runtime_base_dir ^ "/matita.lang" +let script_template = runtime_base_dir ^ "/matita.ma.templ" diff --git a/helm/matita/matita.ma.templ b/helm/matita/matita.ma.templ new file mode 100644 index 000000000..0a57c97cd --- /dev/null +++ b/helm/matita/matita.ma.templ @@ -0,0 +1,16 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +set "baseuri" "cic:/matita/tests/". + diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml index 7b73eb112..c3e169c50 100644 --- a/helm/matita/matitaGui.ml +++ b/helm/matita/matitaGui.ml @@ -289,7 +289,11 @@ class gui () = | None -> () with MatitaTypes.Cancel -> () in - let newScript () = (s ())#reset (); disableSave () in + let newScript () = + (s ())#reset (); + (s ())#template (); + disableSave () + in let cursor () = source_buffer#place_cursor (source_buffer#get_iter_at_mark (`NAME "locked")) @@ -330,7 +334,7 @@ class gui () = else begin (match script_fname with - | None -> clean_current_baseuri status + | None -> clean_current_baseuri status; GMain.Main.quit () | Some fname -> try ask_and_save_moo_if_needed main#toplevel fname status; diff --git a/helm/matita/matitaScript.ml b/helm/matita/matitaScript.ml index 965969a21..5dd6550a9 100644 --- a/helm/matita/matitaScript.ml +++ b/helm/matita/matitaScript.ml @@ -334,7 +334,9 @@ object (self) set_star self#ppFilename true else set_star self#ppFilename false)); - self#reset () + self#reset (); + self#template (); + buffer#set_modified false val mutable statements = []; (** executed statements *) val mutable history = [ init ]; @@ -478,6 +480,10 @@ List.iter (fun s -> prerr_endline ("'" ^ s ^ "'")) new_statements; buffer#delete ~start:buffer#start_iter ~stop:buffer#end_iter; self#notify + method template () = + let template = MatitaMisc.input_file BuildTimeConf.script_template in + buffer#insert ~iter:(buffer#get_iter `START) template + method goto (pos: [`Top | `Bottom | `Cursor]) () = match pos with | `Top -> self#goto_top; self#notify diff --git a/helm/matita/matitaScript.mli b/helm/matita/matitaScript.mli index 43c40b646..cbdfb286b 100644 --- a/helm/matita/matitaScript.mli +++ b/helm/matita/matitaScript.mli @@ -39,6 +39,7 @@ object method retract : unit -> unit method goto: [`Top | `Bottom | `Cursor] -> unit -> unit method reset: unit -> unit + method template: unit -> unit (** {2 Load/save} *) diff --git a/helm/matita/tests/absurd.ma b/helm/matita/tests/absurd.ma new file mode 100644 index 000000000..ce110718a --- /dev/null +++ b/helm/matita/tests/absurd.ma @@ -0,0 +1,27 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +set "baseuri" "cic:/matita/tests/absurd/". +alias num (instance 0) = "natural number". +alias symbol "eq" (instance 0) = "leibnitz's equality". +alias id "not" = "cic:/Coq/Init/Logic/not.con". + + + +theorem stupid : \forall a:Prop. a \to not a \to 0 = 1. +intros. +absurd a. +assumption. +assumption. +qed. \ No newline at end of file -- 2.39.2