- let rec aux st =
- let (entries, parsed_len) =
- eval_statement buffer guistuff self#lexicon_status self#grafite_status
- userGoal self st
- in
- let new_statuses, new_statements =
- let statuses, texts = List.split entries in
- statuses, texts
- in
- history <- new_statuses @ history;
- statements <- new_statements @ statements;
- let start = buffer#get_iter_at_mark (`MARK locked_mark) in
- let new_text = String.concat "" (List.rev new_statements) in
- if statement <> None then
- buffer#insert ~iter:start new_text
- else begin
- let s = match st with `Raw s | `Ast (_, s) -> s in
- if new_text <> String.sub s 0 parsed_len then begin
- buffer#delete ~start ~stop:(start#copy#forward_chars parsed_len);
- buffer#insert ~iter:start new_text;
- end;
- end;
- self#moveMark (String.length new_text)
- in
- let s = match statement with Some s -> s | None -> self#getFuture in
- HLog.debug ("evaluating: " ^ first_line s ^ " ...");
- (try aux (`Raw s) with End_of_file -> raise Margin)
+ let s = match statement with Some s -> s | None -> self#getFuture in
+ HLog.debug ("evaluating: " ^ first_line s ^ " ...");
+ let (entries, parsed_len) =
+ try
+ eval_statement buffer guistuff self#lexicon_status self#grafite_status
+ userGoal self (`Raw s)
+ with End_of_file -> raise Margin
+ in
+ let new_statuses, new_statements =
+ let statuses, texts = List.split entries in
+ statuses, texts
+ in
+ history <- new_statuses @ history;
+ statements <- new_statements @ statements;
+ let start = buffer#get_iter_at_mark (`MARK locked_mark) in
+ let new_text = String.concat "" (List.rev new_statements) in
+ if statement <> None then
+ buffer#insert ~iter:start new_text
+ else begin
+ if new_text <> String.sub s 0 parsed_len then begin
+ buffer#delete ~start ~stop:(start#copy#forward_chars parsed_len);
+ buffer#insert ~iter:start new_text;
+ end;
+ end;
+ self#moveMark (String.length new_text);
+ (* here we need to set the Goal in case we are going to cursor (or to
+ bottom) and we will face a macro *)
+ match self#grafite_status.proof_status with
+ Incomplete_proof p ->
+ userGoal <- Some (Continuationals.Stack.find_goal p.stack)
+ | _ -> userGoal <- None