X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Flambda-delta%2Ftoplevel%2Ftop.ml;h=245c00d4a951cd5f600c05d6546c830040f6406c;hb=2589e631ad9c04a89cb7730d6bca913aed016f98;hp=85587e8d8c148c5cb591ad5048396ec25ec7caa4;hpb=55d6dde568f1daf1fa6902428bda7caec147375a;p=helm.git

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