From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 11 Jan 2011 21:29:25 +0000 (+0000)
Subject: Part of last HUGE COMMIT about NCic.status
X-Git-Tag: make_still_working~2597
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=daad2a4dda4e4b0eed3c1cd57846a31da5f706a5;p=helm.git

Part of last HUGE COMMIT about NCic.status
---

diff --git a/matita/matita/matitaScript.ml b/matita/matita/matitaScript.ml
index f1b20efe5..fafd7cdb2 100644
--- a/matita/matita/matitaScript.ml
+++ b/matita/matita/matitaScript.ml
@@ -147,7 +147,7 @@ let eval_nmacro include_paths (buffer : GText.buffer) status unparsed_text parse
         | thms -> 
            String.concat ", "  
              (HExtlib.filter_map (function 
-               | NotationPt.NRef r -> Some (NCicPp.r2s true r) 
+               | NotationPt.NRef r -> Some (NCicPp.r2s status true r) 
                | _ -> None) 
              thms)
       in
@@ -254,7 +254,7 @@ let source_buffer = source_view#source_buffer in
 let similarsymbols_tag_name = "similarsymbolos" in
 let similarsymbols_tag = `NAME similarsymbols_tag_name in
 let initial_statuses current baseuri =
- let status = new GrafiteTypes.status baseuri in
+ let status = new MatitaEngine.status baseuri in
  (match current with
      Some current ->
       NCicLibrary.time_travel status;