- 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 -> ())
- | _ -> ())
- *)
- 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)
-
- method private _retract offset status new_statements new_history =
- let cur_status = match history with s::_ -> s | [] -> assert false in
- MatitaSync.time_travel ~present:cur_status ~past:status;
+ 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 include_paths 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 <-
+ (try Some (Continuationals.Stack.find_goal p.stack)
+ with Failure _ -> None)
+ | _ -> userGoal <- None
+
+ method private _retract offset lexicon_status grafite_status new_statements
+ new_history
+ =
+ let cur_grafite_status,cur_lexicon_status =
+ match history with s::_ -> s | [] -> assert false
+ in
+ LexiconSync.time_travel ~present:cur_lexicon_status ~past:lexicon_status;
+ GrafiteSync.time_travel ~present:cur_grafite_status ~past:grafite_status;