- let module TAPp = GrafiteAstPp in
- let module MD = GrafiteDisambiguator in
- let module ML = MatitaMisc in
- match ex with
- TA.Tactical (loc, _, _) ->
- eval_with_engine
- guistuff lexicon_status grafite_status user_goal parsed_text
- (TA.Executable (loc, ex))
- | TA.Command (loc, cmd) ->
- (try
- begin
- match cmd with
- | TA.Set (loc',"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)
- | TA.Macro (_,mac) ->
- eval_macro guistuff lexicon_status grafite_status user_goal unparsed_text
- parsed_text script mac
-
-let rec eval_statement (buffer : GText.buffer) guistuff lexicon_status
+ 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