X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Fmatita.ml;h=0b5919ab9e8b28f78c7a81035eb2615ebdb7fcbf;hb=2da3c84c4badb8e6836e9dd6efe7e0d524234b28;hp=2ff07613a786b13c3288fb028538ea0499f765b3;hpb=2d1cecb1593f5d4f4f1bb697f983ac8db99c2987;p=helm.git

diff --git a/helm/matita/matita.ml b/helm/matita/matita.ml
index 2ff07613a..0b5919ab9 100644
--- a/helm/matita/matita.ml
+++ b/helm/matita/matita.ml
@@ -29,6 +29,11 @@ open MatitaGtkMisc
 open MatitaTypes
 open MatitaMisc
 
+
+(* ALB to link paramodulation... *)
+let _ = Saturation.init ()
+  
+
 (** {2 Initialization} *)
 
 let _ =
@@ -72,26 +77,34 @@ let _ =
     (MatitaGui.interactive_interp_choice ())
 
 let script =
-  MatitaScript.script 
-    ~buffer:gui#sourceView#buffer
-    ~init:(Lazy.force MatitaEngine.initial_status) 
-    ~mathviewer:(MatitaMathView.mathViewer ())
-    ~urichooser:(fun uris ->
-      try
-        MatitaGui.interactive_uri_choice ~selection_mode:`SINGLE
-        ~title:"Matita: URI chooser" 
-        ~msg:"Select the URI" ~hide_uri_entry:true
-        ~hide_try:true ~ok_label:"_Apply" ~ok_action:`SELECT
-        ~copy_cb:(fun s -> gui#sourceView#buffer#insert ("\n"^s^"\n"))
-        () ~id:"boh?" uris
-      with MatitaTypes.Cancel -> [])
-    ~set_star:gui#setStar
-    ~ask_confirmation:
-      (fun ~title ~message -> 
-          MatitaGtkMisc.ask_confirmation ~title ~message 
-          ~parent:gui#main#toplevel ())
-    ~develcreator:gui#createDevelopment
-    ()
+  let s = 
+    MatitaScript.script 
+      ~view:(gui#sourceView :> GText.view)
+      ~init:(Lazy.force MatitaEngine.initial_status) 
+      ~mathviewer:(MatitaMathView.mathViewer ())
+      ~urichooser:(fun uris ->
+        try
+          MatitaGui.interactive_uri_choice ~selection_mode:`SINGLE
+          ~title:"Matita: URI chooser" 
+          ~msg:"Select the URI" ~hide_uri_entry:true
+          ~hide_try:true ~ok_label:"_Apply" ~ok_action:`SELECT
+          ~copy_cb:(fun s -> gui#sourceView#buffer#insert ("\n"^s^"\n"))
+          () ~id:"boh?" uris
+        with MatitaTypes.Cancel -> [])
+      ~set_star:gui#setStar
+      ~ask_confirmation:
+        (fun ~title ~message -> 
+            MatitaGtkMisc.ask_confirmation ~title ~message 
+            ~parent:gui#main#toplevel ())
+      ~develcreator:gui#createDevelopment
+      ()
+  in
+  gui#sourceView#source_buffer#begin_not_undoable_action ();
+  s#reset (); 
+  s#template (); 
+  gui#sourceView#source_buffer#end_not_undoable_action ();
+  s
+  
 
   (* math viewers *)
 let _ =
@@ -173,9 +186,6 @@ let _ =
 let _ =
   at_exit (fun () -> print_endline "\nThanks for using Matita!\n");
   Sys.catch_break true;
-  (try
-     gui#loadScript Sys.argv.(1);
-   with Invalid_argument _ -> ());
   if Filename.basename Sys.argv.(0) = "cicbrowser" then begin (* cicbrowser *)
     Helm_registry.set "matita.mode" "cicbrowser";
     let browser = MatitaMathView.cicBrowser () in
@@ -187,6 +197,9 @@ let _ =
     browser#load entry
   end else begin  (* matita *)
     Helm_registry.set "matita.mode" "matita";
+    (try
+       gui#loadScript Sys.argv.(1);
+     with Invalid_argument _ -> ());
     gui#main#mainWin#show ();
   end;
   try