+ let rec aux st =
+ let (entries, parsed_len) =
+ eval_statement buffer guistuff self#status userGoal self st
+ in
+ let (new_statuses, new_statements, new_asts) =
+ let statuses, statements = List.split entries in
+ let texts, asts = List.split statements in
+ statuses, texts, asts
+ in
+ history <- List.rev new_statuses @ history;
+ statements <- List.rev new_statements @ statements;
+ let start = buffer#get_iter_at_mark (`MARK locked_mark) in
+ let new_text = String.concat "" new_statements in
+ if statement <> None then
+ buffer#insert ~iter:start new_text
+ else
+ let s = match st with `Raw s | `Ast (_, s) -> s in
+ if new_text <> String.sub s 0 parsed_len then
+ begin
+ let stop = start#copy#forward_chars parsed_len in
+ buffer#delete ~start ~stop;
+ buffer#insert ~iter:start new_text;
+ end;
+ self#moveMark (String.length new_text);
+ (*
+ (match List.rev new_asts with (* advance again on punctuation *)
+ | TA.Executable (_, TA.Tactical (_, tac, _)) :: _ ->
+ let baseoffset =
+ (buffer#get_iter_at_mark (`MARK locked_mark))#offset
+ in
+ let text = self#getFuture in
+ (try
+ (match parse_statement baseoffset 0 buffer text with
+ | TA.Executable (loc, TA.Tactical (_, tac, None)) as st
+ when GrafiteAst.is_punctuation tac ->
+ let len = snd (CicNotationPt.loc_of_floc loc) in
+ aux (`Ast (st, String.sub text 0 len))
+ | _ -> ())
+ with CicNotationParser.Parse_error _ | End_of_file -> ())
+ | _ -> ())
+ *)