- match st with TA.Executable (loc,ex) -> loc, ex | _ -> assert false
- in
- let goal_changed = ref false in
- let status =
- match status.proof_status with
- | Incomplete_proof (_, goal) when goal <> user_goal ->
- goal_changed := true;
- MatitaEngine.eval_ast ~include_paths:include_
- ~do_heavy_checks:true status (goal_ast user_goal)
- | _ -> status
- in
- let new_status =
- MatitaEngine.eval_ast
- ~include_paths:include_ ~do_heavy_checks:true status st
- in
- let new_aliases =
- match ex with
- | TA.Command (_, TA.Alias _)
- | TA.Command (_, TA.Include _) -> DisambiguateTypes.Environment.empty
- | _ -> MatitaSync.alias_diff ~from:status new_status
+ match st with TA.Executable (loc,ex) -> loc, ex | _ -> assert false in
+ let initial_space,parsed_text =
+ try
+ let pieces = Pcre.extract ~rex:heading_nl_RE' parsed_text in
+ pieces.(1), pieces.(2)
+ with
+ Not_found -> "", parsed_text in
+ let inital_space,new_grafite_status,new_lexicon_status,new_status_and_text_list' =
+ (* the code commented out adds the "select" command if needed *)
+ initial_space,grafite_status,lexicon_status,[] in
+(* match grafite_status.proof_status with
+ | Incomplete_proof { stack = stack }
+ when not (List.mem user_goal (Continuationals.head_goals stack)) ->
+ let grafite_status =
+ MatitaEngine.eval_ast
+ ~do_heavy_checks:true grafite_status (goal_ast user_goal)
+ in
+ let initial_space = if initial_space = "" then "\n" else initial_space
+ in
+ "\n", grafite_status,
+ [ grafite_status,
+ initial_space ^ TAPp.pp_tactical (TA.Select (loc, [user_goal])) ]
+ | _ -> initial_space,grafite_status,[] in *)
+ let enriched_history_fragment =
+ MatitaEngine.eval_ast ~do_heavy_checks:true
+ new_lexicon_status new_grafite_status st