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 *)
(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
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
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
try
is_there_only_comments self#lexicon_status self#getFuture
with
+ | LexiconEngine.IncludedFileNotCompiled _
| HExtlib.Localized _
| CicNotationParser.Parse_error _ -> false
| Margin | End_of_file -> true