From 546b8519396c265560a7d1e72d5c716648000987 Mon Sep 17 00:00:00 2001
From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Fri, 20 Jan 2006 12:47:16 +0000
Subject: [PATCH] Improved rendering of conjectures

---
 helm/ocaml/content_pres/box.ml            |  1 +
 helm/ocaml/content_pres/box.mli           |  1 +
 helm/ocaml/content_pres/content2pres.ml   | 26 +++++++++++++----------
 helm/ocaml/content_pres/renderingAttrs.ml | 16 ++++++++------
 4 files changed, 27 insertions(+), 17 deletions(-)

diff --git a/helm/ocaml/content_pres/box.ml b/helm/ocaml/content_pres/box.ml
index 8b992e041..7c5069262 100644
--- a/helm/ocaml/content_pres/box.ml
+++ b/helm/ocaml/content_pres/box.ml
@@ -120,6 +120,7 @@ let b_object b = Object ([],b)
 let b_indent = indent
 let b_space = Space [None, "width", "0.5em"]
 let b_kw = b_text (RenderingAttrs.object_keyword_attributes `BoxML)
+let b_toggle items = Action ([ None, "type", "toggle"], items)
 
 let pp_attr attr =
   let pp (ns, n, v) =
diff --git a/helm/ocaml/content_pres/box.mli b/helm/ocaml/content_pres/box.mli
index 56c086964..d2ca17bdd 100644
--- a/helm/ocaml/content_pres/box.mli
+++ b/helm/ocaml/content_pres/box.mli
@@ -73,6 +73,7 @@ val b_object: 'expr -> 'expr box
 val b_indent: 'expr box -> 'expr box
 val b_space: 'expr box
 val b_kw: string -> 'expr box
+val b_toggle: 'expr box list -> 'expr box (** action which toggle among items *)
 
 val pp_attr: attr -> string
 
diff --git a/helm/ocaml/content_pres/content2pres.ml b/helm/ocaml/content_pres/content2pres.ml
index 948eb7b9a..abac7cb5d 100644
--- a/helm/ocaml/content_pres/content2pres.ml
+++ b/helm/ocaml/content_pres/content2pres.ml
@@ -160,10 +160,10 @@ and proof2pres term2pres p =
          match concl with
             None -> body
           | Some ac ->
-             B.Action
-               ([None,"type","toggle"],
-                [(make_concl ~attrs:[Some "helm", "xref", p.Con.proof_id]
-                   "proof of" ac); body])
+             let concl =
+               make_concl ~attrs:[ Some "helm", "xref", p.Con.proof_id ]
+                 "proof of" ac in
+             B.b_toggle [ concl; body ]
         in
         B.V ([],
           [B.Text ([],"(" ^ name ^ ")");
@@ -665,8 +665,11 @@ exception ToDo
 let counter = ref 0
 
 let conjecture2pres term2pres (id, n, context, ty) =
-  (B.b_h [Some "helm", "xref", id]
-     (((List.map
+ B.b_indent
+  (B.b_hv [Some "helm", "xref", id]
+     ((B.b_toggle [
+        B.b_h [] [B.b_text [] "{...}"; B.b_space];
+        B.b_hv [] (List.map
           (function
              | None ->
 		 B.b_h []
@@ -707,11 +710,12 @@ let conjecture2pres term2pres (id, n, context, ty) =
 					| Some n -> n)) ;
                        B.b_text [] (Utf8Macro.unicode_of_tex "\\Assign");
                        proof2pres term2pres p])
-          (List.rev context)) @
-         [ B.b_text [] (Utf8Macro.unicode_of_tex "\\vdash");
-           B.b_object (p_mi [] (string_of_int n)) ;
-           B.b_text [] ":" ;
-           term2pres ty ])))
+          (List.rev context)) ] ::
+         [ B.b_h []
+           [ B.b_text [] (Utf8Macro.unicode_of_tex "\\vdash");
+             B.b_object (p_mi [] (string_of_int n)) ;
+             B.b_text [] ":" ;
+             term2pres ty ]])))
 
 let metasenv2pres term2pres = function
   | None -> []
diff --git a/helm/ocaml/content_pres/renderingAttrs.ml b/helm/ocaml/content_pres/renderingAttrs.ml
index cc692abe9..256238d3d 100644
--- a/helm/ocaml/content_pres/renderingAttrs.ml
+++ b/helm/ocaml/content_pres/renderingAttrs.ml
@@ -28,17 +28,21 @@
 type xml_attribute = string option * string * string
 type markup = [ `MathML | `BoxML ]
 
+let color1 = "blue"
+(* let color2 = "red" *)
+let color2 = "blue"
+
 let keyword_attributes = function
-  | `MathML -> [ None, "mathcolor", "blue" ]
-  | `BoxML -> [ None, "color", "blue" ]
+  | `MathML -> [ None, "mathcolor", color1 ]
+  | `BoxML -> [ None, "color", color1 ]
 
 let builtin_symbol_attributes = function
-  | `MathML -> [ None, "mathcolor", "blue" ]
-  | `BoxML -> [ None, "color", "blue" ]
+  | `MathML -> [ None, "mathcolor", color1 ]
+  | `BoxML -> [ None, "color", color1 ]
 
 let object_keyword_attributes = function
-  | `MathML -> [ None, "mathcolor", "red" ]
-  | `BoxML -> [ None, "color", "red" ]
+  | `MathML -> [ None, "mathcolor", color2 ]
+  | `BoxML -> [ None, "color", color2 ]
 
 let symbol_attributes _ = []
 let ident_attributes _ = []
-- 
2.39.2