Keeping track of locations of disambiguated ids and symbols.

[helm.git] / matitaB / matita / matitaEngine.ml

diff --git a/matitaB/matita/matitaEngine.ml b/matitaB/matita/matitaEngine.ml
index 913ba87f6a835e8269bdd3973297ed7b81ddff03..68cb16c84fa63ca4d9d2aa711d458be4fc4ac408 100644 (file)
--- a/matitaB/matita/matitaEngine.ml
+++ b/matitaB/matita/matitaEngine.ml
@@ -118,11 +118,17 @@ let activate_extraction baseuri fname =
 
 let eval_ast ~include_paths ?do_heavy_checks status (text,prefix_len,ast) =
  let baseuri = status#baseuri in
+ (*
  let new_aliases,new_status =
   GrafiteDisambiguate.eval_with_new_aliases status
    (fun status ->
      GrafiteEngine.eval_ast ~include_paths ?do_heavy_checks status
       (text,prefix_len,ast)) in
+ *)
+ let new_status = 
+   GrafiteEngine.eval_ast ~include_paths ?do_heavy_checks status
+    (text,prefix_len,ast) in
+ (*
  let _,intermediate_states = 
   List.fold_left
    (fun (status,acc) (k,value) -> 
@@ -146,6 +152,8 @@ let eval_ast ~include_paths ?do_heavy_checks status (text,prefix_len,ast) =
    ) (status,[]) new_aliases (* WARNING: this must be the old status! *)
  in
   (new_status,None)::intermediate_states
+  *)
+ [new_status,None]
 ;;
 
 let baseuri_of_script ~include_paths fname =
@@ -269,6 +277,12 @@ and compile ~compiling ~asserted ~include_paths fname =
      HLog.message 
        (sprintf "execution of %s completed in %s." fname (hou^min^sec));
      pp_times fname true big_bang big_bang_u big_bang_s;
+     (* XXX: update script -- currently to stdout *)
+     let origbuf = Ulexing.from_utf8_channel (open_in fname) in
+     let outfile = open_out (fname ^ ".mad") in
+     let interpr = GrafiteDisambiguate.get_interpr status#disambiguate_db in
+     ignore (SmallLexer.mk_small_printer interpr outfile origbuf);
+     close_out outfile;
      asserted
 (* MATITA 1.0: debbo fare time_travel sulla ng_library?
      LexiconSync.time_travel 
@@ -276,7 +290,7 @@ and compile ~compiling ~asserted ~include_paths fname =
 *))
   with 
   (* all exceptions should be wrapped to allow lexicon-undo (LS.time_travel) *)
-  | exn when not matita_debug ->
+  | exn when not matita_debug -> 
 (* MATITA 1.0: debbo fare time_travel sulla ng_library?
        LexiconSync.time_travel ~present:lexicon ~past:initial_lexicon_status;
  *       *)