X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2FmatitaScript.ml;h=6221e4901c53ec37937d6e6488d7f82bea231937;hb=47a9eb47d4215450230840bc66570ce412d0ce79;hp=9fc79ca9261245520309698de312b744b76b3e02;hpb=729e08f5fb86b3ffee460fda4577b024ab5888aa;p=helm.git

diff --git a/matita/matita/matitaScript.ml b/matita/matita/matitaScript.ml
index 9fc79ca92..6221e4901 100644
--- 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:NotationPp.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
@@ -286,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 -> ());
@@ -294,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 =
@@ -430,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)