we enabled the new style xml exportation, in particular for dual_rg

[helm.git] / helm / software / lambda-delta / toplevel / top.ml

diff --git a/helm/software/lambda-delta/toplevel/top.ml b/helm/software/lambda-delta/toplevel/top.ml
index 4c1ee1903bf0e8b6df9566f266344b329686f187..3558dc8d00540d064c6bc3f0046ab59501e9e3d0 100644 (file)
--- a/helm/software/lambda-delta/toplevel/top.ml
+++ b/helm/software/lambda-delta/toplevel/top.ml
@@ -24,6 +24,7 @@ module DA   = DrgAut
 module MA   = MetaAut
 module MO   = MetaOutput
 module ML   = MetaLibrary
+module DrgO = DrgOutput
 module MBrg = MetaBrg
 module BrgO = BrgOutput
 module BrgR = BrgReduction
@@ -97,13 +98,14 @@ let count_entity st = function
    | _            -> st
 
 let export_entity si g moch = function
+   | DrgEntity e  -> X.export_entity DrgO.export_term si g e
    | BrgEntity e  -> X.old_export_entity BrgO.export_term si g e
    | MetaEntity e ->
       begin match moch with
          | None     -> ()
          | Some och -> ML.write_entity C.start och e
       end
-   | _            -> ()
+   | BagEntity _  -> ()
 
 let type_check f st si g k =
    let brg_err msg = brg_error "Type Error" msg; failwith "Interrupted" in
@@ -144,7 +146,7 @@ let process_2 f st entity =
            
 let process_1 f st entity = 
    let st = count_entity st entity in
-   export_entity !si !graph !moch entity;
+   if !export && !stage = 1 then export_entity !si !graph !moch entity;
    if !stage > 1 then xlate (process_2 f) st entity else f st 
 
 let process_0 f st entity = 
@@ -205,6 +207,12 @@ try
       close_in ich;
       if !L.level > 0 then T.utime_stamp "parsed";
       O.clear_reductions ();
+      let mk_uri =
+         if !stage < 2 then Drg.mk_uri else
+        match !kernel with
+           | Brg -> Brg.mk_uri
+           | Bag -> Bag.mk_uri
+      in
       let cover = if !use_cover then base_name else "" in
       let f st = 
          if !L.level > 0 then T.utime_stamp "processed";
@@ -214,7 +222,7 @@ try
          if !L.level > 2 && !stage > 1 then print_counters st;
          if !L.level > 2 && !stage > 1 then O.print_reductions ()
       in
-      process f book (initial_status Drg.mk_uri cover)
+      process f book (initial_status mk_uri cover)
    in
    let exit () =
       close !moch;