bugfix: no longer raise End_of_file for scripts ending with comments

diff --git a/helm/matita/matitaScript.ml b/helm/matita/matitaScript.ml
index bd707de1eb522af2e148afc198a2ad464e685732..34e0408c598f281aa0d6bee4417bc3ad5493e407 100644 (file)
--- 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:";