added script template

added test for absurd

diff --git a/helm/matita/buildTimeConf.ml.in b/helm/matita/buildTimeConf.ml.in
index bc3466a69fc062f8f1a1be22a913ce6f67dbdaa6..acb2a3feb8f819360c911f80b700e8e064cdd76e 100644 (file)
--- 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 (file)
index 0000000..0a57c97
--- /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/<fill here>".
+

diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml
index 7b73eb112b5b2c5f517711da398f67ec1ca82054..c3e169c50a371c39051cc7b9863484cfc2f00053 100644 (file)
--- 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 965969a217855a611cdb309518744553aedff1cf..5dd6550a9d49a8a81c059f1f223ab054a8ed9a5c 100644 (file)
--- 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 43c40b6462148d4227a9e0a1a606cd95c4e0837f..cbdfb286bbdef58e8d0eb54448a7776a483afd1a 100644 (file)
--- 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 (file)
index 0000000..ce11071
--- /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