GrafiteAstPp: \n's finally fixed

[helm.git] / components / acic_procedural / proceduralTypes.ml

diff --git a/components/acic_procedural/proceduralTypes.ml b/components/acic_procedural/proceduralTypes.ml
index ae153fe3d1d5b2b3abbe25f2c5bbd33ec8b49368..a1d120f807a161ac7aeb472e17d5518a63f28dcf 100644 (file)
--- a/components/acic_procedural/proceduralTypes.ml
+++ b/components/acic_procedural/proceduralTypes.ml
@@ -45,6 +45,10 @@ let list_map2_filter map l1 l2 =
   in 
   filter [] (list_rev_map2 map l1 l2)
 
+let list_init f i =
+   let rec aux a j = if j < 0 then a else aux (f j :: a) (pred j) in
+   aux [] i
+
 (****************************************************************************)
 
 type name     = string
@@ -81,8 +85,14 @@ let floc = H.dummy_floc
 
 let mk_note str = G.Comment (floc, G.Note (floc, str))
 
-let mk_nlnote str a =
-   if str = "" then mk_note "" :: a else mk_note str :: mk_note "" :: a
+let mk_tacnote str a =
+   if str = "" then mk_note "" :: a else mk_note "" :: mk_note str :: a
+
+let mk_notenote str a =
+   if str = "" then a else mk_note str :: a
+
+let mk_thnote str a =
+   if str = "" then a else mk_note "" :: mk_note str :: a
 
 let mk_theorem name t = 
    let obj = N.Theorem (`Theorem, name, t, None) in
@@ -158,22 +168,22 @@ let mk_vb = G.Shift floc
 (* rendering ****************************************************************)
 
 let rec render_step sep a = function
-   | Note s                  -> mk_note s :: a
-   | Theorem (n, t, s)       -> mk_theorem n t :: mk_note s :: a 
-   | Qed s                   -> mk_qed :: mk_nlnote s a
-   | Id s                    -> mk_id sep :: mk_nlnote s a
-   | Intros (c, ns, s)       -> mk_intros c ns sep :: mk_nlnote s a
-   | Cut (n, t, s)           -> mk_cut n t sep :: mk_nlnote s a
-   | LetIn (n, t, s)         -> mk_letin n t sep :: mk_nlnote s a
-   | Rewrite (b, t, w, e, s) -> mk_rewrite b t w e sep :: mk_nlnote s a
-   | Elim (t, xu, e, s)      -> mk_elim t xu e sep :: mk_nlnote s a
-   | Apply (t, s)            -> mk_apply t sep :: mk_nlnote s a
-   | Change (t, _, w, e, s)  -> mk_change t w e sep :: mk_nlnote s a
-   | ClearBody (n, s)        -> mk_clearbody n sep :: mk_nlnote s a
+   | Note s                  -> mk_notenote s a
+   | Theorem (n, t, s)       -> mk_theorem n t :: mk_thnote s a 
+   | Qed s                   -> mk_qed :: mk_tacnote s a
+   | Id s                    -> mk_id sep :: mk_tacnote s a
+   | Intros (c, ns, s)       -> mk_intros c ns sep :: mk_tacnote s a
+   | Cut (n, t, s)           -> mk_cut n t sep :: mk_tacnote s a
+   | LetIn (n, t, s)         -> mk_letin n t sep :: mk_tacnote s a
+   | Rewrite (b, t, w, e, s) -> mk_rewrite b t w e sep :: mk_tacnote s a
+   | Elim (t, xu, e, s)      -> mk_elim t xu e sep :: mk_tacnote s a
+   | Apply (t, s)            -> mk_apply t sep :: mk_tacnote s a
+   | Change (t, _, w, e, s)  -> mk_change t w e sep :: mk_tacnote s a
+   | ClearBody (n, s)        -> mk_clearbody n sep :: mk_tacnote s a
    | Branch ([], s)          -> a
    | Branch ([ps], s)        -> render_steps sep a ps
    | Branch (ps :: pss, s)   ->      
-      let a = mk_ob :: mk_nlnote s a in
+      let a = mk_ob :: mk_tacnote s a in
       let a = List.fold_left (render_steps mk_vb) a (List.rev pss) in
       mk_punctation sep :: render_steps mk_cb a ps