(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 =
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