- let module A = TacticAst in
- let loc = CicAst.dummy_floc in
- A.Tactical (loc, A.Tactic (loc, A.Goal (loc, n)))
-
-let eval_statement status mathviewer user_goal s =
- let st = CicTextualParser2.parse_statement (Stream.of_string s) in
- match st with
- | TacticAst.Command (loc, _) | TacticAst.Tactical (loc, _) ->
- let parsed_text_length = snd (CicAst.loc_of_floc loc) in
- let parsed_text = safe_substring s 0 parsed_text_length 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 status (goal_ast user_goal)
- | _ -> status
+ let module A = GrafiteAst in
+ let loc = HExtlib.dummy_floc in
+ A.Executable (loc, A.Tactical (loc,
+ A.Tactic (loc, A.Goal (loc, n)),
+ Some (A.Dot loc)))
+
+type guistuff = {
+ mathviewer:MatitaTypes.mathViewer;
+ urichooser: UriManager.uri list -> UriManager.uri list;
+ ask_confirmation: title:string -> message:string -> [`YES | `NO | `CANCEL];
+ develcreator: containing:string option -> unit;
+ mutable filenamedata: string option * MatitamakeLib.development option
+}
+
+let eval_with_engine guistuff lexicon_status grafite_status user_goal
+ parsed_text st
+=
+ let module TAPp = GrafiteAstPp in
+ let parsed_text_length = String.length parsed_text 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
+(* let loc, ex =
+ match st with TA.Executable (loc,ex) -> loc, ex | _ -> assert false 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
+ in
+ let _,new_text_list_rev =
+ let module DTE = DisambiguateTypes.Environment in
+ let module UM = UriManager in
+ List.fold_right (
+ fun (_,alias) (initial_space,acc) ->
+ match alias with
+ None -> initial_space,initial_space::acc
+ | Some (k,((v,_) as value)) ->
+ let new_text =
+ let initial_space =
+ if initial_space = "" then "\n" else initial_space
+ in
+ initial_space ^
+ DisambiguatePp.pp_environment
+ (DisambiguateTypes.Environment.add k value
+ DisambiguateTypes.Environment.empty)
+ in
+ "\n",new_text::acc
+ ) enriched_history_fragment (initial_space,[]) in
+ let new_text_list_rev =
+ match enriched_history_fragment,new_text_list_rev with
+ (_,None)::_, initial_space::tl -> (initial_space ^ parsed_text)::tl
+ | _,_ -> assert false
+ in
+ let res =
+ try
+ List.combine (fst (List.split enriched_history_fragment)) new_text_list_rev
+ with
+ Invalid_argument _ -> assert false
+ in
+ res,parsed_text_length
+
+let wrap_with_developments guistuff f arg =
+ try
+ f arg
+ with
+ | DependenciesParser.UnableToInclude what
+ | LexiconEngine.IncludedFileNotCompiled what
+ | GrafiteEngine.IncludedFileNotCompiled what as exc ->
+ let compile_needed_and_go_on d =
+ let target = Pcre.replace ~pat:"lexicon$" ~templ:"moo" what in
+ let refresh_cb () =
+ while Glib.Main.pending () do ignore(Glib.Main.iteration false); done
+ in
+ if not(MatitamakeLib.build_development_in_bg ~target refresh_cb d) then
+ raise exc
+ else
+ f arg