- try
- GrafiteParser.parse_statement (Ulexing.from_utf8_string text)
- with CicNotationParser.Parse_error (floc, err) as exn ->
- match error_tag with
- | None -> raise exn
- | Some error_tag ->
- let (x, y) = CicNotationPt.loc_of_floc floc in
- let x = parsedlen + x in
- let y = parsedlen + y in
- let x' = baseoffset + x in
- let y' = baseoffset + y in
- let x_iter = buffer#get_iter (`OFFSET x') in
- let y_iter = buffer#get_iter (`OFFSET y') in
- buffer#apply_tag error_tag ~start:x_iter ~stop:y_iter;
- let id = ref None in
- id := Some (buffer#connect#changed ~callback:(fun () ->
- buffer#remove_tag error_tag ~start:buffer#start_iter
- ~stop:buffer#end_iter;
- match !id with
- | None -> assert false (* a race condition occurred *)
- | Some id ->
- (new GObj.gobject_ops buffer#as_buffer)#disconnect id));
- let flocb,floce = floc in
- let floc =
- { flocb with Lexing.pos_cnum = x }, { floce with Lexing.pos_cnum = y }
- in
- buffer#place_cursor (buffer#get_iter (`OFFSET x'));
- raise (CicNotationParser.Parse_error (floc, err))
-
-let rec eval_statement baseoffset parsedlen error_tag (buffer : GText.buffer)
- guistuff status user_goal script statement
-=
- let st, unparsed_text =