added "dumb" test target

[helm.git] / matita / matitaScript.ml

diff --git a/matita/matitaScript.ml b/matita/matitaScript.ml
index 07a7cbd2ed553a8b736fb83299d45c2c8cbeac57..510e736e5cc1896375ec723f2c77ab0c571d0183 100644 (file)
--- a/matita/matitaScript.ml
+++ b/matita/matitaScript.ml
@@ -772,9 +772,10 @@ object (self)
       in
       match st with
       | GrafiteParser.LSome (GrafiteAst.Comment (loc,_)) -> 
-          let _,parsed_text_length = 
-            MatitaGtkMisc.utf8_parsed_text s loc 
-          in
+          let _,parsed_text_length = MatitaGtkMisc.utf8_parsed_text s loc in
+          (* CSC: why +1 in the following lines ???? *)
+          let parsed_text_length = parsed_text_length + 1 in
+prerr_endline ("## " ^ string_of_int parsed_text_length);
           let remain_len = String.length s - parsed_text_length in
           let next = String.sub s parsed_text_length remain_len in
           is_there_only_comments lexicon_status next
@@ -784,6 +785,7 @@ object (self)
     try
       is_there_only_comments self#lexicon_status self#getFuture
     with 
+    | LexiconEngine.IncludedFileNotCompiled _
     | HExtlib.Localized _
     | CicNotationParser.Parse_error _ -> false
     | Margin | End_of_file -> true