From adb0fc58f7de5c1741cf18bed8a2251e8313f103 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Thu, 25 Feb 2010 19:42:00 +0000 Subject: [PATCH] - pipeline support for generated entities in text mode completed --- helm/software/lambda-delta/complete_rg/crgTxt.ml | 2 +- helm/software/lambda-delta/complete_rg/crgTxt.mli | 4 ++-- helm/software/lambda-delta/toplevel/top.ml | 15 +++++++++++---- 3 files changed, 14 insertions(+), 7 deletions(-) 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 -- 2.39.2