X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2FmatitaScript.ml;h=510e736e5cc1896375ec723f2c77ab0c571d0183;hb=b1ee9ef71c8badde1b783e0e0296a4e7d87a8aa4;hp=07a7cbd2ed553a8b736fb83299d45c2c8cbeac57;hpb=cbcd34fe15122eb9835a5226b98be1050b097d6a;p=helm.git diff --git a/matita/matitaScript.ml b/matita/matitaScript.ml index 07a7cbd2e..510e736e5 100644 --- 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