- pipeline support for generated entities in text mode completed

diff --git a/helm/software/lambda-delta/complete_rg/crgTxt.ml b/helm/software/lambda-delta/complete_rg/crgTxt.ml
index e0f5feb1a17182964cecab652fd12c5b3286626d..34727aff9a28e00ea756f2eaab3aba2cbe803045 100644 (file)
--- a/helm/software/lambda-delta/complete_rg/crgTxt.ml
+++ b/helm/software/lambda-delta/complete_rg/crgTxt.ml
@@ -110,7 +110,7 @@ let mk_contents tt = function
    | T.Def  -> [], Y.Abbr tt
    | T.Th   -> [], Y.Abbr tt
 
-let xlate_entity err f st = function
+let xlate_entity err f gen st = function
    | T.Require _                  ->
       err st
    | T.Section (Some name)        ->

diff --git a/helm/software/lambda-delta/complete_rg/crgTxt.mli b/helm/software/lambda-delta/complete_rg/crgTxt.mli
index 90105b57f68cff6f75904e5b2d01fb1f68d97be2..150268a55c388a2df85a0e2744bf53ef37faa6e5 100644 (file)
--- a/helm/software/lambda-delta/complete_rg/crgTxt.mli
+++ b/helm/software/lambda-delta/complete_rg/crgTxt.mli
@@ -15,5 +15,5 @@ val initial_status: unit -> status
 
 val refresh_status: status -> status
 
-val crg_of_txt: (status -> 'a) -> (status -> Crg.entity -> 'a) -> 
-                status -> Txt.command -> 'a
+val crg_of_txt: (status -> 'a) -> (status -> Crg.entity -> 'a) ->
+                (Txt.command -> unit) -> status -> Txt.command -> 'a

diff --git a/helm/software/lambda-delta/toplevel/top.ml b/helm/software/lambda-delta/toplevel/top.ml
index 85587e8d8c148c5cb591ad5048396ec25ec7caa4..245c00d4a951cd5f600c05d6546c830040f6406c 100644 (file)
--- a/helm/software/lambda-delta/toplevel/top.ml
+++ b/helm/software/lambda-delta/toplevel/top.ml
@@ -180,13 +180,20 @@ let txt_xl = initial_lexer TxtLexer.token
 
 let aut_xl = initial_lexer AutLexer.token 
 
-let entity_of_input lexbuf = function
-   | Text     -> 
+let parbuf = ref [] (* parser buffer *)
+
+let gen_text command = 
+   parbuf := TxtEntity command :: !parbuf
+
+let entity_of_input lexbuf i = match i, !parbuf with
+   | Text, []       -> 
       begin match TxtParser.entry (token txt_xl) lexbuf with
          | Some e, unget -> txt_xl.unget <- unget; Some (TxtEntity e)
          | None, _       -> None
       end
-   | Automath -> 
+   | Text, hd :: tl ->
+      parbuf := tl; Some hd
+   | Automath, _    -> 
       begin match AutParser.entry (token aut_xl) lexbuf with
          | Some e, unget -> aut_xl.unget <- unget; Some (AutEntity e)
          | None, _       -> None
@@ -238,7 +245,7 @@ let process_0 st entity =
       match entity, !old with
          | AutEntity e, true  -> MA.meta_of_aut frr h st.mst e 
          | AutEntity e, false -> DA.crg_of_aut err g st.dst e
-        | TxtEntity e, false -> DT.crg_of_txt crr d st.tst e
+        | TxtEntity e, false -> DT.crg_of_txt crr d gen_text st.tst e
         | _                  -> assert false
    in
    let st = if !L.level > 2 then count_input st entity else st in