Improved rendering of conjectures

diff --git a/helm/ocaml/content_pres/box.ml b/helm/ocaml/content_pres/box.ml
index 8b992e0416194867eebbb8f7984e38fd91e34cfb..7c50692621d99ff3fcff497209ce81c64193924d 100644 (file)
--- 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 56c0869640fd72ed4c9ea397506ba6a639bac252..d2ca17bddd15128a15c2e7146e4e4d7f58b33585 100644 (file)
--- 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 948eb7b9ac7c58293123397cc150de0f4705349a..abac7cb5deca46fd88f1acf4be241d8ca8b6b5fa 100644 (file)
--- 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 cc692abe9cda8427ca210302e2a9942e21cd224b..256238d3d460d617ec6f98c5804bc8a4b6517ae3 100644 (file)
--- 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 _ = []