X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaScript.ml;h=c35fb9307232975b1b8409005aea93bcc1810562;hb=75cce5f252471a73764953dbb5fa24a450d153bb;hp=08e3a45991ce6a53fbd9dbc5d2916e2245d6aa30;hpb=7c123bfb1568f90f37cd667332fbf60d4423b983;p=helm.git

diff --git a/helm/matita/matitaScript.ml b/helm/matita/matitaScript.ml
index 08e3a4599..c35fb9307 100644
--- 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,13 +128,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 +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 () = 
@@ -213,9 +216,9 @@ 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 = MatitaDb.instance () in
-  let metasenv = MatitaTypes.get_proof_metasenv status in
-  let context = MatitaTypes.get_proof_context status user_goal in
+  let dbd = LibraryDb.instance () 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
@@ -226,12 +229,12 @@ let disambiguate_macro_term term status user_goal =
 let eval_macro guistuff status user_goal unparsed_text parsed_text script mac =
   let module TAPp = GrafiteAstPp in
   let module MQ = MetadataQuery in
-  let module MDB = MatitaDb in
+  let module MDB = LibraryDb in
   let module CTC = CicTypeChecker in
   let module CU = CicUniv in
   (* no idea why ocaml wants this *)
   let parsed_text_length = String.length parsed_text in
-  let dbd = MatitaDb.instance () in
+  let dbd = LibraryDb.instance () in
   match mac with
   (* WHELP's stuff *)
   | TA.WMatch (loc, term) -> 
@@ -275,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
@@ -289,22 +292,26 @@ 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
         in
         [ new_status , (extra_text, ast) ], parsed_text_length
       | _ -> 
-          MatitaLog.error 
+          HLog.error 
             "The result of the urichooser should be only 1 uri, not:\n";
           List.iter (
-            fun u -> MatitaLog.error (UriManager.string_of_uri u ^ "\n")
+            fun u -> HLog.error (UriManager.string_of_uri u ^ "\n")
           ) 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
@@ -345,14 +352,14 @@ let eval_executable guistuff status user_goal unparsed_text parsed_text script
 =
   let module TAPp = GrafiteAstPp in
   let module MD = MatitaDisambiguator in
-  let module ML = MatitacleanLib in
+  let module ML = MatitaMisc in
   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" 
@@ -361,7 +368,9 @@ let eval_executable guistuff status user_goal unparsed_text parsed_text script
                     "Do you want to redefine the corresponding "^
                     "part of the library?")
               with
-              | `YES -> MatitacleanLib.clean_baseuris [u]
+              | `YES ->
+                  let basedir = Helm_registry.get "matita.basedir" in
+                   LibraryClean.clean_baseuris ~basedir [u]
               | `NO -> ()
               | `CANCEL -> raise MatitaTypes.Cancel);
         eval_with_engine 
@@ -394,9 +403,13 @@ let rec eval_statement (buffer : GText.buffer) guistuff status user_goal
        try
         eval_statement buffer guistuff status user_goal script
          (`Raw s)
-       with HExtlib.Localized (floc, exn) ->
-        HExtlib.raise_localized_exception
-         ~offset:parsed_text_length floc exn
+       with
+          HExtlib.Localized (floc, exn) ->
+           HExtlib.raise_localized_exception ~offset:parsed_text_length floc exn
+        | MatitaDisambiguator.DisambiguationError (offset,errorll) ->
+           raise
+            (MatitaDisambiguator.DisambiguationError
+              (offset+parsed_text_length, errorll))
       in
       (match s with
       | (status, (text, ast)) :: tl ->
@@ -412,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
@@ -515,7 +528,7 @@ object (self)
       *)
     in
     let s = match statement with Some s -> s | None -> self#getFuture in
-    MatitaLog.debug ("evaluating: " ^ first_line s ^ " ...");
+    HLog.debug ("evaluating: " ^ first_line s ^ " ...");
     (try aux (`Raw s) with End_of_file -> raise Margin)
 
   method private _retract offset status new_statements new_history =
@@ -583,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 =
@@ -615,7 +628,7 @@ object (self)
         output_string oc (buffer#get_text ~start:buffer#start_iter
                             ~stop:buffer#end_iter ());
         close_out oc;
-        MatitaLog.debug ("backup " ^ f ^ " saved")                    
+        HLog.debug ("backup " ^ f ^ " saved")                    
       end
   
   method private goto_top =
@@ -730,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
 
@@ -758,11 +771,11 @@ object (self)
 
   (* debug *)
   method dump () =
-    MatitaLog.debug "script status:";
-    MatitaLog.debug ("history size: " ^ string_of_int (List.length history));
-    MatitaLog.debug (sprintf "%d statements:" (List.length statements));
-    List.iter MatitaLog.debug statements;
-    MatitaLog.debug ("Current file name: " ^
+    HLog.debug "script status:";
+    HLog.debug ("history size: " ^ string_of_int (List.length history));
+    HLog.debug (sprintf "%d statements:" (List.length statements));
+    List.iter HLog.debug statements;
+    HLog.debug ("Current file name: " ^
       (match guistuff.filenamedata with 
       |None,_ -> "[ no name ]" 
       | Some f,_ -> f));