- 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 = DisambiguateTypes.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 status user_goal parsed_text st =
+ let module TAPp = GrafiteAstPp in
+ let include_ =
+ match guistuff.filenamedata with
+ | None,None -> []
+ | None,Some devel -> [MatitamakeLib.root_for_development devel ]
+ | Some f,_ ->
+ match MatitamakeLib.development_for_dir (Filename.dirname f) with
+ | None -> []
+ | Some devel -> [MatitamakeLib.root_for_development devel ]
+ in
+ let parsed_text_length = String.length parsed_text in
+ let loc, ex =
+ 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
+ (* we add the goal command if needed *)
+ let inital_space,new_status,new_status_and_text_list' =
+ match status.proof_status with
+(* | Incomplete_proof { stack = stack }
+ when not (List.mem user_goal (Continuationals.head_goals stack)) ->
+ let status =
+ MatitaEngine.eval_ast ~include_paths:include_
+ ~do_heavy_checks:true status (goal_ast user_goal)
+ in
+ let initial_space = if initial_space = "" then "\n" else initial_space
+ in
+ "\n", status,
+ [ status,
+ initial_space ^ TAPp.pp_tactical (TA.Select (loc, [user_goal])) ] *)
+ | _ -> initial_space,status,[] in
+ let new_status =
+ MatitaEngine.eval_ast
+ ~include_paths:include_ ~do_heavy_checks:true new_status st
+ in
+ let new_aliases =
+ match ex with
+ | TA.Command (_, TA.Alias _)
+ | TA.Command (_, TA.Include _)
+ | TA.Command (_, TA.Interpretation _) -> []
+ | _ -> MatitaSync.alias_diff ~from:status new_status
+ in
+ (* we remove the defined object since we consider them "automatic aliases" *)
+ let dummy_st =
+ TA.Comment (DisambiguateTypes.dummy_floc,
+ TA.Note (DisambiguateTypes.dummy_floc, ""))
+ in
+ let initial_space,status,new_status_and_text_list_rev =
+ let module DTE = DisambiguateTypes.Environment in
+ let module UM = UriManager in
+ List.fold_left (
+ fun (initial_space,status,acc) (k,((v,_) as value)) ->
+ let b =
+ try
+ let v = UM.strip_xpointer (UM.uri_of_string v) in
+ List.exists (fun (s,_) -> s = v) new_status.objects
+ with UM.IllFormedUri _ -> false
+ in
+ if b then
+ initial_space,status,acc
+ else
+ 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
+ let new_status =
+ MatitaSync.set_proof_aliases status [k,value]
+ in
+ "\n",new_status,((new_status, (new_text, dummy_st))::acc)
+ ) (initial_space,status,[]) new_aliases in
+ let parsed_text = initial_space ^ parsed_text in
+ let res =
+ List.rev new_status_and_text_list_rev @ new_status_and_text_list' @
+ [new_status, (parsed_text, st)]
+ in
+ res,parsed_text_length
+
+let eval_with_engine guistuff status user_goal parsed_text st =
+ try
+ eval_with_engine guistuff status user_goal parsed_text st
+ with
+ | MatitaEngine.UnableToInclude what
+ | MatitaEngine.IncludedFileNotCompiled what as exc ->
+ let compile_needed_and_go_on d =
+ let target = 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
+ eval_with_engine guistuff status user_goal parsed_text st