From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Thu, 25 Feb 2010 19:42:00 +0000 (+0000)
Subject: - pipeline support for generated entities in text mode completed
X-Git-Tag: make_still_working~3025
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=adb0fc58f7de5c1741cf18bed8a2251e8313f103;p=helm.git

- 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 e0f5feb1a..34727aff9 100644
--- 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 90105b57f..150268a55 100644
--- 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 85587e8d8..245c00d4a 100644
--- 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