+ match outer_syntax_parser () with
+ `Undo n ->
+ let rec drop =
+ function
+ 0,l -> l
+ | n,_::l -> drop (n-1,l)
+ | _,[] -> assert false
+ in
+ let to_be_dropped = List.length !lexicon_status - n in
+ let safe_hd = function [] -> assert false | he::_ -> he in
+ let cur_lexicon_status = safe_hd !lexicon_status in
+ let cur_grafite_status = safe_hd !grafite_status in
+ lexicon_status := drop (to_be_dropped, !lexicon_status) ;
+ grafite_status := drop (to_be_dropped, !grafite_status) ;
+ let lexicon_status = safe_hd !lexicon_status in
+ let grafite_status = safe_hd !grafite_status in
+ LexiconSync.time_travel
+ ~present:cur_lexicon_status ~past:lexicon_status;
+ GrafiteSync.time_travel
+ ~present:cur_grafite_status ~past:grafite_status;
+ interactive_loop (Some n)
+ | `Do command ->
+ let str = Ulexing.from_utf8_string command in
+ let watch_statuses lexicon_status grafite_status =
+ match grafite_status.GrafiteTypes.proof_status with
+ GrafiteTypes.Incomplete_proof
+ {GrafiteTypes.proof = uri,metasenv,bo,ty,attrs ;
+ GrafiteTypes.stack = stack } ->
+ let open_goals = Continuationals.Stack.open_goals stack in
+ print_endline
+ (String.concat "\n"
+ (List.map
+ (fun i ->
+ ApplyTransformation.txt_of_cic_sequent 80 metasenv
+ (List.find (fun (j,_,_) -> j=i) metasenv)
+ ) open_goals))
+ | _ -> ()
+ in
+ let include_paths =
+ Helm_registry.get_list Helm_registry.string "matita.includes"
+ in
+ run_script str
+ (MatitaEngine.eval_from_stream ~first_statement_only:true ~prompt:false
+ ~include_paths ~watch_statuses) ;
+ interactive_loop (Some (List.length !lexicon_status))