urimanager removed

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

diff --git a/matita/matita/matitaScript.ml b/matita/matita/matitaScript.ml
index b6ec2a51f01262a58b483a093a7dafea26b4f7c1..6221e4901c53ec37937d6e6488d7f82bea231937 100644 (file)
--- a/matita/matita/matitaScript.ml
+++ b/matita/matita/matitaScript.ml
@@ -67,7 +67,7 @@ let first_line s =
 
 type guistuff = {
   mathviewer:MatitaTypes.mathViewer;
-  urichooser: UriManager.uri list -> UriManager.uri list;
+  urichooser: NReference.reference list -> NReference.reference list;
   ask_confirmation: title:string -> message:string -> [`YES | `NO | `CANCEL];
 }
 
@@ -124,9 +124,7 @@ let wrap_with_make include_paths (f : #LexiconEngine.status GrafiteParser.statem
       else raise (Failure ("Compiling: " ^ tgt))
 ;;
 
-let pp_eager_statement_ast =
-  GrafiteAstPp.pp_statement ~term_pp:CicNotationPp.pp_term
-    ~lazy_term_pp:(fun _ -> assert false) ~obj_pp:(fun _ -> assert false)
+let pp_eager_statement_ast = GrafiteAstPp.pp_statement 
 
 let eval_nmacro include_paths (buffer : GText.buffer) guistuff grafite_status user_goal unparsed_text parsed_text script mac =
   let parsed_text_length = String.length parsed_text in
@@ -151,7 +149,7 @@ let eval_nmacro include_paths (buffer : GText.buffer) guistuff grafite_status us
       let m, s, status, t = 
         GrafiteDisambiguate.disambiguate_nterm 
           None status ctx menv subst (parsed_text,parsed_text_length,
-            CicNotationPt.Cast (t,CicNotationPt.Implicit `JustOne))  
+            NotationPt.Cast (t,NotationPt.Implicit `JustOne))  
           (* XXX use the metasenv, if possible *)
       in
       guistuff.mathviewer#show_entry (`NCic (t,ctx,m,s));
@@ -181,7 +179,7 @@ let eval_nmacro include_paths (buffer : GText.buffer) guistuff grafite_status us
         | thms -> 
            String.concat ", "  
              (HExtlib.filter_map (function 
-               | CicNotationPt.NRef r -> Some (NCicPp.r2s true r) 
+               | NotationPt.NRef r -> Some (NCicPp.r2s true r) 
                | _ -> None) 
              thms)
       in
@@ -190,42 +188,7 @@ let eval_nmacro include_paths (buffer : GText.buffer) guistuff grafite_status us
       [s, nl ^ trace ^ thms ^ ";"], "", parsed_text_length
   | TA.NAutoInteractive (_, (Some _,_)) -> assert false
 
-let rec eval_macro include_paths (buffer : GText.buffer) guistuff grafite_status user_goal unparsed_text parsed_text script mac =
-  let module CTC = CicTypeChecker in
-  (* no idea why ocaml wants this *)
-  let parsed_text_length = String.length parsed_text in
-  let dbd = LibraryDb.instance () in
-  match mac with
-  (* REAL macro *)
-  | TA.Hint (loc, rewrite) -> (* MATITA 1.0 *) assert false
-  | TA.Eval (_, kind, term) -> assert false (* MATITA 1.0
-      let metasenv = GrafiteTypes.get_proof_metasenv grafite_status in
-      let context =
-       match user_goal with
-          None -> []
-        | Some n -> GrafiteTypes.get_proof_context grafite_status n in
-      let ty,_ = CTC.type_of_aux' metasenv context term CicUniv.empty_ugraph in
-      let term = 
-        match kind with
-        | `Normalize ->
-             CicReduction.normalize ~delta:true ~subst:[] context term
-        | `Simpl -> 
-            ProofEngineReduction.simpl context term
-        | `Unfold None ->
-            ProofEngineReduction.unfold ?what:None context term
-        | `Unfold (Some lazy_term) ->
-             let what, _, _ = 
-               lazy_term context metasenv CicUniv.empty_ugraph in
-             ProofEngineReduction.unfold ~what context term
-        | `Whd ->
-            CicReduction.whd ~delta:true ~subst:[] context term
-      in
-      let t_and_ty = Cic.Cast (term,ty) in
-      guistuff.mathviewer#show_entry (`Cic (t_and_ty,metasenv));
-      [(grafite_status#set_proof_status No_proof), parsed_text ],"", 
-        parsed_text_length *)
-                                
-and eval_executable include_paths (buffer : GText.buffer) guistuff
+let rec eval_executable include_paths (buffer : GText.buffer) guistuff
 grafite_status user_goal unparsed_text skipped_txt nonskipped_txt
 script ex loc
 =
@@ -238,11 +201,6 @@ script ex loc
      (TA.Executable (loc, ex))
   with
      MatitaTypes.Cancel -> [], "", 0
-   | GrafiteEngine.Macro (_loc,lazy_macro) ->
-      let context = [] in
-      let grafite_status,macro = lazy_macro context in
-       eval_macro include_paths buffer guistuff grafite_status
-        user_goal unparsed_text (skipped_txt ^ nonskipped_txt) script macro
    | GrafiteEngine.NMacro (_loc,macro) ->
        eval_nmacro include_paths buffer guistuff grafite_status
         user_goal unparsed_text (skipped_txt ^ nonskipped_txt) script macro
@@ -326,7 +284,8 @@ let initial_statuses current baseuri =
  (match current with
      Some current ->
       LexiconSync.time_travel ~present:current ~past:empty_lstatus;
-      GrafiteSync.time_travel ~present:current ();
+      NCicLibrary.time_travel
+       ((new GrafiteTypes.status current#baseuri)#set_lstatus current#lstatus);
       (* CSC: there is a known bug in invalidation; temporary fix here *)
       NCicEnvironment.invalidate ()
    | None -> ());
@@ -334,7 +293,7 @@ let initial_statuses current baseuri =
    CicNotation2.load_notation ~include_paths:[] empty_lstatus
      BuildTimeConf.core_notation_script 
  in
- let grafite_status = GrafiteSync.init lexicon_status baseuri in
+ let grafite_status = (new GrafiteTypes.status baseuri)#set_lstatus lexicon_status#lstatus in
   grafite_status
 in
 let read_include_paths file =
@@ -470,7 +429,7 @@ object (self)
     match history with s::_ -> s | [] -> assert false
    in
     LexiconSync.time_travel ~present:cur_grafite_status ~past:grafite_status;
-    GrafiteSync.time_travel ~present:cur_grafite_status ~past:grafite_status ();
+    NCicLibrary.time_travel grafite_status;
     statements <- new_statements;
     history <- new_history;
     self#moveMark (- offset)