From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Mon, 7 Nov 2005 10:28:50 +0000 (+0000)
Subject: bugfix: no longer raise End_of_file for scripts ending with comments
X-Git-Tag: V_0_7_2_3~120
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=82247d9af61693c803bbc87bc6df2de62f359976;p=helm.git

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 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:";