...

[helm.git] / matita / matitaScript.ml

diff --git a/matita/matitaScript.ml b/matita/matitaScript.ml
index 62d760c3b993b365b01b133b362855b3a3b20324..510e736e5cc1896375ec723f2c77ab0c571d0183 100644 (file)
--- a/matita/matitaScript.ml
+++ b/matita/matitaScript.ml
@@ -85,9 +85,11 @@ let eval_with_engine guistuff lexicon_status grafite_status user_goal
   let parsed_text_length =
     String.length skipped_txt + String.length nonskipped_txt 
   in
+  let text = skipped_txt ^ nonskipped_txt in
+  let prefix_len = MatitaGtkMisc.utf8_string_length skipped_txt in
   let enriched_history_fragment =
    MatitaEngine.eval_ast ~do_heavy_checks:true
-    lexicon_status grafite_status st
+    lexicon_status grafite_status (text,prefix_len,st)
   in
   let enriched_history_fragment = List.rev enriched_history_fragment in
   (* really fragile *)
@@ -101,8 +103,6 @@ let eval_with_engine guistuff lexicon_status grafite_status user_goal
             (status,to_prepend ^ newtxt ^ "\n")::acc, "")
       ([],skipped_txt) enriched_history_fragment
   in
-  let res = (*List.combine (List.map fst (List.rev enriched_history_fragment))
-  strings*) res in 
   res,parsed_text_length
 
 let wrap_with_developments guistuff f arg = 
@@ -362,7 +362,8 @@ and eval_statement include_paths (buffer : GText.buffer) guistuff lexicon_status
          grafite_status user_goal script (`Raw s)
        with
           HExtlib.Localized (floc, exn) ->
-           HExtlib.raise_localized_exception ~offset:parsed_text_length floc exn
+           HExtlib.raise_localized_exception 
+             ~offset:(MatitaGtkMisc.utf8_string_length parsed_text) floc exn
         | GrafiteDisambiguator.DisambiguationError (offset,errorll) ->
            raise
             (GrafiteDisambiguator.DisambiguationError
@@ -719,7 +720,7 @@ object (self)
              self#_retract (icmp - len) lexicon_status grafite_status statements
               history
           | statement::tl1, _::tl2 ->
-             back_until_cursor (len - String.length statement) (tl1,tl2)
+             back_until_cursor (len - MatitaGtkMisc.utf8_string_length statement) (tl1,tl2)
           | _,_ -> assert false
         in
         (try
@@ -771,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
@@ -783,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