interim version (added smallLexer)

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

diff --git a/matitaB/matita/matitaEngine.ml b/matitaB/matita/matitaEngine.ml
index 68cb16c84fa63ca4d9d2aa711d458be4fc4ac408..437121b73f9aed171ba0184763b2d810ba1a7773 100644 (file)
--- a/matitaB/matita/matitaEngine.ml
+++ b/matitaB/matita/matitaEngine.ml
@@ -116,44 +116,9 @@ let activate_extraction baseuri fname =
 ;;
 
 
-let eval_ast ~include_paths ?do_heavy_checks status (text,prefix_len,ast) =
+let eval_ast ~include_paths ?do_heavy_checks status (text,prefix_len,ast as 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) -> 
-     let v = GrafiteAst.description_of_alias value in
-     let b =
-      try
-       let NReference.Ref (uri,_) = NReference.reference_of_string v in
-        NUri.baseuri_of_uri uri = baseuri
-      with
-       NReference.IllFormedReference _ ->
-        false (* v is a description, not a URI *)
-     in
-      if b then 
-       status,acc
-      else
-       let status =
-        GrafiteDisambiguate.set_proof_aliases status ~implicit_aliases:false
-         GrafiteAst.WithPreferences [k,value]
-       in
-        status, (status ,Some (k,value))::acc
-   ) (status,[]) new_aliases (* WARNING: this must be the old status! *)
- in
-  (new_status,None)::intermediate_states
-  *)
- [new_status,None]
+   GrafiteEngine.eval_ast ~include_paths ?do_heavy_checks status ast'
 ;;
 
 let baseuri_of_script ~include_paths fname =
@@ -192,14 +157,8 @@ and eval_from_stream ~compiling ~asserted ~include_paths ?do_heavy_checks status
      | None -> asserted, true, status
      | Some (asserted,ast) ->
         cb status ast;
-        let new_statuses =
-          eval_ast ~include_paths ?do_heavy_checks status ("",0,ast) in
         let status =
-         match new_statuses with
-            [s,None] -> s
-          | _::(_,Some (_,value))::_ ->
-                raise (TryingToAdd (lazy (GrafiteAstPp.pp_alias value)))
-          | _ -> assert false
+          eval_ast ~include_paths ?do_heavy_checks status ("",0,ast)
         in
          asserted, false, status
    with exn when not matita_debug ->
@@ -209,7 +168,7 @@ and eval_from_stream ~compiling ~asserted ~include_paths ?do_heavy_checks status
  in
   loop asserted status
 
-and compile ~compiling ~asserted ~include_paths fname =
+and compile ~compiling ~asserted ~include_paths ~outch fname =
   if List.mem fname compiling then raise (CircularDependency fname);
   let compiling = fname::compiling in
   let matita_debug = Helm_registry.get_bool "matita.debug" in
@@ -279,10 +238,8 @@ and compile ~compiling ~asserted ~include_paths fname =
      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;
+     ignore (SmallLexer.mk_small_printer interpr outch origbuf);
      asserted
 (* MATITA 1.0: debbo fare time_travel sulla ng_library?
      LexiconSync.time_travel 
@@ -297,7 +254,7 @@ and compile ~compiling ~asserted ~include_paths fname =
       pp_times fname false big_bang big_bang_u big_bang_s;
       clean_exit baseuri exn
 
-and assert_ng ~already_included ~compiling ~asserted ~include_paths mapath =
+and assert_ng ~already_included ~compiling ~asserted ~include_paths ?outch mapath =
  let _,baseuri,fullmapath,_ = Librarian.baseuri_of_script ~include_paths mapath in
  if List.mem fullmapath asserted then asserted,false
  else
@@ -342,13 +299,19 @@ and assert_ng ~already_included ~compiling ~asserted ~include_paths mapath =
        (* maybe recompiling it I would get the same... *)
        raise (AlreadyLoaded (lazy mapath))
      else
-      let asserted = compile ~compiling ~asserted ~include_paths fullmapath in
+      let outch, is_file_ch = 
+        match outch with
+        | None -> open_out (fullmapath ^ ".mad"), true
+        | Some c -> c, false
+      in
+      let asserted = compile ~compiling ~asserted ~include_paths ~outch fullmapath in
+       if is_file_ch then close_out outch;
        fullmapath::asserted,true
   end
 ;;
 
-let assert_ng ~include_paths mapath =
+let assert_ng ~include_paths ?outch mapath =
  snd (assert_ng ~include_paths ~already_included:[] ~compiling:[] ~asserted:[]
-  mapath)
+  ?outch mapath)
 let get_ast status ~include_paths strm =
  snd (get_ast status ~compiling:[] ~asserted:[] ~include_paths strm)