From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Wed, 10 Jan 2007 19:36:37 +0000 (+0000)
Subject: procedural: buggy ast renderer fixed
X-Git-Tag: make_still_working~6528
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=013e0ab5c86d7c4c7560f06ffe0ae3b424737db2;p=helm.git

procedural: buggy ast renderer fixed
---

diff --git a/helm/software/components/content_pres/acic2Procedural.ml b/helm/software/components/content_pres/acic2Procedural.ml
index 18ded2e79..9b8dbf063 100644
--- a/helm/software/components/content_pres/acic2Procedural.ml
+++ b/helm/software/components/content_pres/acic2Procedural.ml
@@ -236,7 +236,7 @@ let mk_obj st = function
       let text = Printf.sprintf "tactics: %u" count in
       P.Theorem (s, t, text) :: ast @ [P.Qed ""]
    | _                                                               ->
-      [P.Note "not a theorem"]
+      failwith "not a theorem"
 
 (* interface functions ******************************************************)
 
diff --git a/helm/software/components/content_pres/proceduralTypes.ml b/helm/software/components/content_pres/proceduralTypes.ml
index be1dbee73..0ef73e248 100644
--- a/helm/software/components/content_pres/proceduralTypes.ml
+++ b/helm/software/components/content_pres/proceduralTypes.ml
@@ -155,23 +155,23 @@ let rec render_step sep a = function
    | Elim (t, xu, s)      -> mk_note s :: cont sep (mk_elim t xu :: a)
    | Apply (t, s)         -> mk_note s :: cont sep (mk_apply t :: a)
    | Branch ([], s)       -> a
-   | Branch ([ps], s)     -> cont sep (render_steps a ps)
+   | Branch ([ps], s)     -> render_steps sep a ps
    | Branch (pss, s)      ->
       let a =  mk_ob :: a in
-      let body = mk_cb :: list_rev_map_concat render_steps mk_vb a pss in
+      let body = mk_cb :: list_rev_map_concat (render_steps None) mk_vb a pss in
       mk_note s :: cont sep body
 
-and render_steps a = function
+and render_steps sep a = function
    | []                                          -> a
-   | [p]                                         -> render_step None a p
-   | (Note _ | Theorem _ | Qed _ as p) :: ps     ->
-      render_steps (render_step None a p) ps 
-   | p :: ((Branch ([], _) :: _) as ps) ->
-      render_steps (render_step None a p) ps
+   | [p]                                         -> render_step sep a p
+   | p :: Branch ([], _) :: ps                   ->
+      render_steps sep a (p :: ps)
    | p :: ((Branch (_ :: _ :: _, _) :: _) as ps) ->
-      render_steps (render_step (Some mk_sc) a p) ps
+      render_steps sep (render_step (Some mk_sc) a p) ps
    | p :: ps                                     ->
-      render_steps (render_step (Some mk_dot) a p) ps
+      render_steps sep (render_step (Some mk_dot) a p) ps
+
+let render_steps a = render_steps None a
 
 (* counting *****************************************************************)