+ (match guistuff.ask_confirmation ~title ~message with
+ | `YES ->
+ (match filename with
+ | Some f ->
+ guistuff.develcreator ~containing:(Some (Filename.dirname f))
+ | None -> guistuff.develcreator ~containing:None);
+ do_nothing ()
+ | `NO -> raise exc
+ | `CANCEL -> do_nothing())
+ in
+ match guistuff.filenamedata with
+ | None,None -> handle_without_devel None
+ | None,Some d -> handle_with_devel d
+ | Some f,_ ->
+ match MatitamakeLib.development_for_dir (Filename.dirname f) with
+ | None -> handle_without_devel (Some f)
+ | Some d -> handle_with_devel d
+;;
+
+let eval_with_engine
+ guistuff lexicon_status grafite_status user_goal parsed_text st
+=
+ wrap_with_developments guistuff
+ (eval_with_engine
+ guistuff lexicon_status grafite_status user_goal parsed_text) st
+;;
+
+let pp_eager_statement_ast =
+ GrafiteAstPp.pp_statement ~term_pp:CicNotationPp.pp_term
+ ~lazy_term_pp:(fun _ -> assert false) ~obj_pp:(fun _ -> assert false)
+
+let rec eval_macro include_paths (buffer : GText.buffer) guistuff lexicon_status grafite_status user_goal unparsed_text parsed_text script mac =
+ let module TAPp = GrafiteAstPp in
+ let module MQ = MetadataQuery in
+ let module MDB = LibraryDb in
+ let module CTC = CicTypeChecker in
+ let module CU = CicUniv in
+ (* no idea why ocaml wants this *)
+ let parsed_text_length = String.length parsed_text in
+ let dbd = LibraryDb.instance () in
+ (* XXX use a real CIC -> string pretty printer *)
+ let pp_macro = TAPp.pp_macro ~term_pp:CicPp.ppterm in
+ match mac with
+ (* WHELP's stuff *)
+ | TA.WMatch (loc, term) ->
+ let l = Whelp.match_term ~dbd term in
+ let query_url =
+ MatitaMisc.strip_suffix ~suffix:"."
+ (HExtlib.trim_blanks unparsed_text)
+ in
+ let entry = `Whelp (query_url, l) in
+ guistuff.mathviewer#show_uri_list ~reuse:true ~entry l;
+ [], parsed_text_length
+ | TA.WInstance (loc, term) ->
+ let l = Whelp.instance ~dbd term in
+ let entry = `Whelp (pp_macro (TA.WInstance (loc, term)), l) in
+ guistuff.mathviewer#show_uri_list ~reuse:true ~entry l;
+ [], parsed_text_length
+ | TA.WLocate (loc, s) ->
+ let l = Whelp.locate ~dbd s in
+ let entry = `Whelp (pp_macro (TA.WLocate (loc, s)), l) in
+ guistuff.mathviewer#show_uri_list ~reuse:true ~entry l;
+ [], parsed_text_length
+ | TA.WElim (loc, term) ->
+ let uri =
+ match term with
+ | Cic.MutInd (uri,n,_) -> UriManager.uri_of_uriref uri n None
+ | _ -> failwith "Not a MutInd"
+ in
+ let l = Whelp.elim ~dbd uri in
+ let entry = `Whelp (pp_macro (TA.WElim (loc, term)), l) in
+ guistuff.mathviewer#show_uri_list ~reuse:true ~entry l;
+ [], parsed_text_length
+ | TA.WHint (loc, term) ->
+ let s = ((None,[0,[],term], Cic.Meta (0,[]) ,term),0) in
+ let l = List.map fst (MQ.experimental_hint ~dbd s) in
+ let entry = `Whelp (pp_macro (TA.WHint (loc, term)), l) in
+ guistuff.mathviewer#show_uri_list ~reuse:true ~entry l;
+ [], parsed_text_length
+ (* REAL macro *)
+ | TA.Hint loc ->
+ let user_goal' =
+ match user_goal with
+ Some n -> n
+ | None -> raise NoUnfinishedProof
+ in
+ let proof = GrafiteTypes.get_current_proof grafite_status in
+ let proof_status = proof,user_goal' in
+ let l = List.map fst (MQ.experimental_hint ~dbd proof_status) in
+ let selected = guistuff.urichooser l in
+ (match selected with
+ | [] -> [], parsed_text_length
+ | [uri] ->
+ let suri = UriManager.string_of_uri uri in
+ let ast loc =
+ TA.Executable (loc, (TA.Tactical (loc,
+ TA.Tactic (loc,
+ TA.Apply (loc, CicNotationPt.Uri (suri, None))),
+ Some (TA.Dot loc)))) in
+ let text =
+ comment parsed_text ^ "\n" ^
+ pp_eager_statement_ast (ast HExtlib.dummy_floc) in
+ let text_len = String.length text in
+ let loc = HExtlib.floc_of_loc (0,text_len) in
+ let statement = `Ast (GrafiteParser.LSome (ast loc),text) in
+ let res,_parsed_text_len =
+ eval_statement include_paths buffer guistuff lexicon_status
+ grafite_status user_goal script statement