X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaScript.ml;h=34e0408c598f281aa0d6bee4417bc3ad5493e407;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=bd707de1eb522af2e148afc198a2ad464e685732;hpb=6fa89cef6aa8fc1774db065a9fcfc47867579054;p=helm.git

diff --git a/helm/matita/matitaScript.ml b/helm/matita/matitaScript.ml
index bd707de1e..34e0408c5 100644
--- a/helm/matita/matitaScript.ml
+++ b/helm/matita/matitaScript.ml
@@ -546,7 +546,7 @@ object (self)
     in
     let s = match statement with Some s -> s | None -> self#getFuture in
     MatitaLog.debug ("evaluating: " ^ first_line s ^ " ...");
-    aux (`Raw s)
+    (try aux (`Raw s) with End_of_file -> raise Margin)
 
   method private _retract offset status new_statements new_history =
     let cur_status = match history with s::_ -> s | [] -> assert false in
@@ -784,10 +784,8 @@ object (self)
       is_there_and_executable s
     with 
     | CicNotationParser.Parse_error _ -> false
-    | Margin -> true
-      
-    
-    
+    | Margin | End_of_file -> true
+
   (* debug *)
   method dump () =
     MatitaLog.debug "script status:";