+ let module TAPp = GrafiteAstPp in
+ let module MD = GrafiteDisambiguator in
+ let module ML = MatitaMisc in
+ try
+ begin
+ match ex with
+ | TA.Command (_,TA.Set (_,"baseuri",u)) ->
+ if not (GrafiteMisc.is_empty u) then
+ (match
+ guistuff.ask_confirmation
+ ~title:"Baseuri redefinition"
+ ~message:(
+ "Baseuri " ^ u ^ " already exists.\n" ^
+ "Do you want to redefine the corresponding "^
+ "part of the library?")
+ with
+ | `YES ->
+ let basedir = Helm_registry.get "matita.basedir" in
+ LibraryClean.clean_baseuris ~basedir [u]
+ | `NO -> ()
+ | `CANCEL -> raise MatitaTypes.Cancel)
+ | _ -> ()
+ end;
+ eval_with_engine
+ guistuff lexicon_status grafite_status user_goal parsed_text
+ (TA.Executable (loc, ex))
+ with
+ MatitaTypes.Cancel -> [], 0
+ | GrafiteEngine.Macro (_loc,lazy_macro) ->
+ let context =
+ match user_goal with
+ None -> []
+ | Some n -> GrafiteTypes.get_proof_context grafite_status n in
+ let grafite_status,macro = lazy_macro context in
+ eval_macro include_paths buffer guistuff lexicon_status grafite_status
+ user_goal unparsed_text parsed_text script macro
+
+and eval_statement include_paths (buffer : GText.buffer) guistuff lexicon_status
+ grafite_status user_goal script statement
+=
+ let (lexicon_status,st), unparsed_text =
+ match statement with
+ | `Raw text ->
+ if Pcre.pmatch ~rex:only_dust_RE text then raise Margin;
+ GrafiteParser.parse_statement (Ulexing.from_utf8_string text)
+ ~include_paths lexicon_status, text
+ | `Ast (st, text) -> (lexicon_status, st), text
+ in