1. Several files in grafite that should be in grafite_parser moved there.

[helm.git] / helm / matita / matitaScript.ml

diff --git a/helm/matita/matitaScript.ml b/helm/matita/matitaScript.ml
index c35fb9307232975b1b8409005aea93bcc1810562..75773e3fe579f3b1ccf9cf12a55befbcf9618cc1 100644 (file)
--- a/helm/matita/matitaScript.ml
+++ b/helm/matita/matitaScript.ml
@@ -98,7 +98,7 @@ let eval_with_engine guistuff status user_goal parsed_text st =
 (*     | 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
@@ -109,9 +109,10 @@ let eval_with_engine guistuff status user_goal parsed_text st =
       | _ -> 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
@@ -163,7 +164,7 @@ let eval_with_engine guistuff status user_goal parsed_text st =
   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
@@ -294,6 +295,7 @@ let eval_macro guistuff status user_goal unparsed_text parsed_text script mac =
           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
@@ -356,7 +358,7 @@ let eval_executable guistuff status user_goal unparsed_text parsed_text script
   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
@@ -373,8 +375,8 @@ let eval_executable guistuff status user_goal unparsed_text parsed_text script
                    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