-let eval_executable guistuff status user_goal parsed_text script ex =
- let module TA = GrafiteAst in
- let module TAPp = GrafiteAstPp in
- let module MD = MatitaDisambiguator in
- let module ML = MatitacleanLib in
- let parsed_text_length = String.length parsed_text in
- match ex with
- | TA.Command (loc, _) | TA.Tactical (loc, _) ->
- (try
- (match ML.baseuri_of_baseuri_decl (TA.Executable (loc,ex)) with
- | None -> ()
- | Some u ->
- if not (MatitacleanLib.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 -> MatitacleanLib.clean_baseuris [u]
- | `NO -> ()
- | `CANCEL -> raise MatitaTypes.Cancel);
- eval_with_engine
- guistuff status user_goal parsed_text (TA.Executable (loc, ex))
- with MatitaTypes.Cancel -> [], 0)
- | TA.Macro (_,mac) ->
- eval_macro guistuff status parsed_text script mac
-
-let rec eval_statement guistuff status user_goal script s =
- if Pcre.pmatch ~rex:only_dust_RE s then raise Margin;
- let st = GrafiteParser.parse_statement (Stream.of_string s) in
+and eval_executable include_paths (buffer : GText.buffer) guistuff lexicon_status grafite_status user_goal unparsed_text parsed_text script loc ex
+=
+ 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;
+ let ast =
+ wrap_with_developments guistuff
+ (GrafiteParser.parse_statement
+ (Ulexing.from_utf8_string text) ~include_paths) lexicon_status
+ in
+ ast, text
+ | `Ast (st, text) -> (lexicon_status, st), text
+ in