From 82247d9af61693c803bbc87bc6df2de62f359976 Mon Sep 17 00:00:00 2001
From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Mon, 7 Nov 2005 10:28:50 +0000
Subject: [PATCH] bugfix: no longer raise End_of_file for scripts ending with
 comments

---
 helm/matita/matitaScript.ml | 8 +++-----
 1 file changed, 3 insertions(+), 5 deletions(-)

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