- 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 -> ())
- | _ -> ())
- *)