1. matitaEngine splitted into disambiguation (now in grafite_parser) and

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

diff --git a/helm/matita/matitaScript.ml b/helm/matita/matitaScript.ml
index 9b9e870855b2b74f2de8656942d1a65dc399f30c..c35fb9307232975b1b8409005aea93bcc1810562 100644 (file)
--- a/helm/matita/matitaScript.ml
+++ b/helm/matita/matitaScript.ml
@@ -24,7 +24,7 @@
  *)
 
 open Printf
-open MatitaTypes
+open GrafiteTypes
 
 module TA = GrafiteAst
 
@@ -108,7 +108,9 @@ let eval_with_engine guistuff status user_goal parsed_text st =
           initial_space ^ TAPp.pp_tactical (TA.Select (loc, [user_goal])) ] *)
       | _ -> initial_space,status,[] in
   let new_status = 
-    MatitaEngine.eval_ast 
+    GrafiteEngine.eval_ast
+      ~disambiguate_tactic:GrafiteDisambiguate.disambiguate_tactic
+      ~disambiguate_command:GrafiteDisambiguate.disambiguate_command
       ~include_paths:include_ ~do_heavy_checks:true new_status st 
   in
   let new_aliases =
@@ -126,7 +128,7 @@ let eval_with_engine guistuff status user_goal parsed_text st =
   let initial_space,status,new_status_and_text_list_rev = 
     let module DTE = DisambiguateTypes.Environment in
     let module UM = UriManager in
-    let baseuri = MatitaTypes.get_string_option new_status "baseuri" in
+    let baseuri = GrafiteTypes.get_string_option new_status "baseuri" in
     List.fold_left (
       fun (initial_space,status,acc) (k,((v,_) as value)) -> 
         let b =
@@ -161,8 +163,8 @@ let eval_with_engine guistuff status user_goal parsed_text st =
   try
     eval_with_engine guistuff status user_goal parsed_text st
   with
-  | MatitaEngine.UnableToInclude what 
-  | MatitaEngine.IncludedFileNotCompiled what as exc ->
+  | GrafiteEngine.UnableToInclude what 
+  | GrafiteEngine.IncludedFileNotCompiled what as exc ->
       let compile_needed_and_go_on d =
         let target = what in
         let refresh_cb () = 
@@ -215,8 +217,8 @@ let eval_with_engine guistuff status user_goal parsed_text st =
 let disambiguate_macro_term term status user_goal =
   let module MD = MatitaDisambiguator in
   let dbd = LibraryDb.instance () in
-  let metasenv = MatitaTypes.get_proof_metasenv status in
-  let context = MatitaTypes.get_proof_context status user_goal in
+  let metasenv = GrafiteTypes.get_proof_metasenv status in
+  let context = GrafiteTypes.get_proof_context status user_goal in
   let interps =
    MD.disambiguate_term ~dbd ~context ~metasenv ~aliases:status.aliases
     ~universe:(Some status.multi_aliases) term in
@@ -276,7 +278,7 @@ let eval_macro guistuff status user_goal unparsed_text parsed_text script mac =
       [], parsed_text_length
   (* REAL macro *)
   | TA.Hint loc -> 
-      let proof = MatitaTypes.get_current_proof status in
+      let proof = GrafiteTypes.get_current_proof status in
       let proof_status = proof, user_goal in
       let l = List.map fst (MQ.experimental_hint ~dbd proof_status) in
       let selected = guistuff.urichooser l in
@@ -290,7 +292,11 @@ let eval_macro guistuff status user_goal unparsed_text parsed_text script mac =
                 TA.Apply (loc, CicNotationPt.Uri (suri, None))),
                 Some (TA.Dot loc))))
           in
-        let new_status = MatitaEngine.eval_ast status ast in
+        let new_status =
+         GrafiteEngine.eval_ast
+          ~disambiguate_tactic:GrafiteDisambiguate.disambiguate_tactic
+          ~disambiguate_command:GrafiteDisambiguate.disambiguate_command
+          status ast in
         let extra_text = 
           comment parsed_text ^ 
           "\n" ^ TAPp.pp_statement ast
@@ -304,8 +310,8 @@ let eval_macro guistuff status user_goal unparsed_text parsed_text script mac =
           ) selected;
           assert false)
   | TA.Check (_,term) ->
-      let metasenv = MatitaTypes.get_proof_metasenv status in
-      let context = MatitaTypes.get_proof_context status user_goal in
+      let metasenv = GrafiteTypes.get_proof_metasenv status in
+      let context = GrafiteTypes.get_proof_context status user_goal in
       let interps = 
         MatitaDisambiguator.disambiguate_term ~dbd ~context ~metasenv
          ~aliases:status.aliases ~universe:(Some status.multi_aliases) term
@@ -350,10 +356,10 @@ let eval_executable guistuff status user_goal unparsed_text parsed_text script
   match ex with
   | TA.Command (loc, _) | TA.Tactical (loc, _, _) ->
       (try 
-        (match MatitaMisc.baseuri_of_baseuri_decl (TA.Executable (loc,ex)) with
+        (match GrafiteMisc.baseuri_of_baseuri_decl (TA.Executable (loc,ex)) with
         | None -> ()
         | Some u -> 
-            if not (MatitaMisc.is_empty u) then
+            if not (GrafiteMisc.is_empty u) then
               match 
                 guistuff.ask_confirmation 
                   ~title:"Baseuri redefinition" 
@@ -419,7 +425,7 @@ let fresh_script_id =
   fun () -> incr i; !i
 
 class script  ~(source_view: GSourceView.source_view)
-              ~(init: MatitaTypes.status) 
+              ~(init: GrafiteTypes.status) 
               ~(mathviewer: MatitaTypes.mathViewer) 
               ~set_star
               ~ask_confirmation
@@ -590,7 +596,7 @@ object (self)
 
   val mutable observers = []
 
-  method addObserver (o: MatitaTypes.status -> unit) =
+  method addObserver (o: GrafiteTypes.status -> unit) =
     observers <- o :: observers
 
   method private notify =
@@ -737,10 +743,10 @@ object (self)
     | Intermediate _ -> assert false
 
 (*   method proofStatus = MatitaTypes.get_proof_status self#status *)
-  method proofMetasenv = MatitaTypes.get_proof_metasenv self#status
-  method proofContext = MatitaTypes.get_proof_context self#status userGoal
-  method proofConclusion = MatitaTypes.get_proof_conclusion self#status userGoal
-  method stack = MatitaTypes.get_stack self#status
+  method proofMetasenv = GrafiteTypes.get_proof_metasenv self#status
+  method proofContext = GrafiteTypes.get_proof_context self#status userGoal
+  method proofConclusion= GrafiteTypes.get_proof_conclusion self#status userGoal
+  method stack = GrafiteTypes.get_stack self#status
   method setGoal n = userGoal <- n
   method goal = userGoal