]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/lambda-delta/toplevel/top.ml
- pipeline support for generated entities in text mode completed
[helm.git] / helm / software / lambda-delta / toplevel / top.ml
index 85587e8d8c148c5cb591ad5048396ec25ec7caa4..245c00d4a951cd5f600c05d6546c830040f6406c 100644 (file)
@@ -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