From 07a798607400b0ae70871b201592ae6286118cdb Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 14 Apr 2006 10:12:27 +0000 Subject: [PATCH] fixed another utf8 string length bug --- helm/software/matita/matitaScript.ml | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/helm/software/matita/matitaScript.ml b/helm/software/matita/matitaScript.ml index 62d760c3b..7f4d800f7 100644 --- a/helm/software/matita/matitaScript.ml +++ b/helm/software/matita/matitaScript.ml @@ -101,8 +101,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 +360,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 -- 2.39.2