(* | Incomplete_proof { stack = stack }
when not (List.mem user_goal (Continuationals.head_goals stack)) ->
let status =
- MatitaEngine.eval_ast ~include_paths:include_
+ MatitaEngine.eval_ast
~do_heavy_checks:true status (goal_ast user_goal)
in
let initial_space = if initial_space = "" then "\n" else initial_space
| _ -> initial_space,status,[] in
let new_status =
GrafiteEngine.eval_ast
+ ~baseuri_of_script:(GrafiteParserMisc.baseuri_of_script ~include_paths:include_)
~disambiguate_tactic:GrafiteDisambiguate.disambiguate_tactic
~disambiguate_command:GrafiteDisambiguate.disambiguate_command
- ~include_paths:include_ ~do_heavy_checks:true new_status st
+ ~do_heavy_checks:true new_status st
in
let new_aliases =
match ex with
try
eval_with_engine guistuff status user_goal parsed_text st
with
- | GrafiteEngine.UnableToInclude what
+ | GrafiteParserMisc.UnableToInclude what
| GrafiteEngine.IncludedFileNotCompiled what as exc ->
let compile_needed_and_go_on d =
let target = what in
in
let new_status =
GrafiteEngine.eval_ast
+ ~baseuri_of_script:(fun _ -> assert false)
~disambiguate_tactic:GrafiteDisambiguate.disambiguate_tactic
~disambiguate_command:GrafiteDisambiguate.disambiguate_command
status ast in
match ex with
| TA.Command (loc, _) | TA.Tactical (loc, _, _) ->
(try
- (match GrafiteMisc.baseuri_of_baseuri_decl (TA.Executable (loc,ex)) with
+ (match GrafiteParserMisc.baseuri_of_baseuri_decl (TA.Executable (loc,ex)) with
| None -> ()
| Some u ->
if not (GrafiteMisc.is_empty u) then
LibraryClean.clean_baseuris ~basedir [u]
| `NO -> ()
| `CANCEL -> raise MatitaTypes.Cancel);
- eval_with_engine
- guistuff status user_goal parsed_text (TA.Executable (loc, ex))
+ eval_with_engine
+ guistuff status user_goal parsed_text (TA.Executable (loc, ex))
with MatitaTypes.Cancel -> [], 0)
| TA.Macro (_,mac) ->
eval_macro guistuff status user_goal unparsed_text parsed_text script mac