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 d4f7d5e008009da3a70f671ca15be7b707c3528f..75773e3fe579f3b1ccf9cf12a55befbcf9618cc1 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
 
@@ -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
@@ -108,8 +108,11 @@ 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 
-      ~include_paths:include_ ~do_heavy_checks:true new_status st 
+    GrafiteEngine.eval_ast
+      ~baseuri_of_script:(GrafiteParserMisc.baseuri_of_script ~include_paths:include_)
+      ~disambiguate_tactic:GrafiteDisambiguate.disambiguate_tactic
+      ~disambiguate_command:GrafiteDisambiguate.disambiguate_command
+      ~do_heavy_checks:true new_status st 
   in
   let new_aliases =
     match ex with
@@ -126,13 +129,14 @@ 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 = GrafiteTypes.get_string_option new_status "baseuri" in
     List.fold_left (
       fun (initial_space,status,acc) (k,((v,_) as value)) -> 
-        let b = 
-          try
-            let v = UM.strip_xpointer (UM.uri_of_string v) in
-            List.exists (fun (s,_) -> s = v) new_status.objects 
-          with UM.IllFormedUri _ -> false
+        let b =
+         try
+          UM.buri_of_uri (UM.uri_of_string v) = baseuri
+         with
+          UriManager.IllFormedUri _ -> false (* v is a description, not a URI *)
         in
         if b then 
           initial_space,status,acc
@@ -160,8 +164,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 ->
+  | GrafiteParserMisc.UnableToInclude what 
+  | GrafiteEngine.IncludedFileNotCompiled what as exc ->
       let compile_needed_and_go_on d =
         let target = what in
         let refresh_cb () = 
@@ -214,8 +218,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
@@ -275,7 +279,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
@@ -289,7 +293,12 @@ 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
+          ~baseuri_of_script:(fun _ -> assert false)
+          ~disambiguate_tactic:GrafiteDisambiguate.disambiguate_tactic
+          ~disambiguate_command:GrafiteDisambiguate.disambiguate_command
+          status ast in
         let extra_text = 
           comment parsed_text ^ 
           "\n" ^ TAPp.pp_statement ast
@@ -303,8 +312,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
@@ -349,10 +358,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 GrafiteParserMisc.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" 
@@ -366,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
@@ -418,7 +427,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
@@ -589,7 +598,7 @@ object (self)
 
   val mutable observers = []
 
-  method addObserver (o: MatitaTypes.status -> unit) =
+  method addObserver (o: GrafiteTypes.status -> unit) =
     observers <- o :: observers
 
   method private notify =
@@ -736,10 +745,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