1) the home button of CicBrowser now works also for NG

[helm.git] / helm / software / components / content_pres / content2pres.ml

diff --git a/helm/software/components/content_pres/content2pres.ml b/helm/software/components/content_pres/content2pres.ml
index 8fe5657b32feeb2cba52a68d8d704199f54d202e..282cfe26ee1655329ab3600802211bc020f6dcf9 100644 (file)
--- a/helm/software/components/content_pres/content2pres.ml
+++ b/helm/software/components/content_pres/content2pres.ml
@@ -835,7 +835,7 @@ let conjecture2pres term2pres (id, n, context, ty) =
                            (match dec_name with
                                 None -> "_"
                               | Some n -> n));
-                       B.b_text [] ":";
+                       B.b_text [] ":"; B.b_space; 
                        term2pres ty ]
              | Some (`Definition d) ->
                  let
@@ -848,6 +848,7 @@ let conjecture2pres term2pres (id, n, context, ty) =
                                          None -> "_"
                                        | Some n -> n)) ;
                        B.b_text [] (Utf8Macro.unicode_of_tex "\\Assign");
+                       B.b_space;
                        term2pres bo]
              | Some (`Proof p) ->
                  let proof_name = p.Content.proof_name in
@@ -857,12 +858,16 @@ let conjecture2pres term2pres (id, n, context, ty) =
                                          None -> "_"
                                        | Some n -> n)) ;
                        B.b_text [] (Utf8Macro.unicode_of_tex "\\Assign");
+                       B.b_space;
                        proof2pres true term2pres p])
           (List.rev context)))) ] ::
          [ B.b_h []
-           [ B.b_text [] (Utf8Macro.unicode_of_tex "\\vdash");
+           [ B.b_space; 
+             B.b_text [] (Utf8Macro.unicode_of_tex "\\vdash");
+             B.b_space;
              B.b_object (p_mi [] (string_of_int n)) ;
              B.b_text [] ":" ;
+             B.b_space;
              term2pres ty ]])))
 
 let metasenv2pres term2pres = function
@@ -924,7 +929,7 @@ let joint_def2pres term2pres def =
   | `Inductive ind -> inductive2pres term2pres ind
   | _ -> assert false (* ZACK or raise ToDo? *)
 
-let content2pres 
+let content2pres0
   ?skip_initial_lambdas ?(skip_thm_and_qed=false) term2pres 
   (id,params,metasenv,obj) 
 =
@@ -971,11 +976,24 @@ let content2pres
 let content2pres 
   ?skip_initial_lambdas ?skip_thm_and_qed ~ids_to_inner_sorts 
 =
-  content2pres ?skip_initial_lambdas ?skip_thm_and_qed
+  content2pres0 ?skip_initial_lambdas ?skip_thm_and_qed
     (fun ?(prec=90) annterm ->
       let ast, ids_to_uris =
        TermAcicContent.ast_of_acic ~output_type:`Term ids_to_inner_sorts annterm
       in
        CicNotationPres.box_of_mpres
-        (CicNotationPres.render ids_to_uris ~prec
+        (CicNotationPres.render
+          ~lookup_uri:(CicNotationPres.lookup_uri ids_to_uris) ~prec
           (TermContentPres.pp_ast ast)))
+
+let ncontent2pres ?skip_initial_lambdas ?skip_thm_and_qed ~ids_to_nrefs =
+ let lookup_uri id =
+  try
+   let nref = Hashtbl.find ids_to_nrefs id in
+    Some (NReference.string_of_reference nref)
+  with Not_found -> None
+ in
+  content2pres0 ?skip_initial_lambdas ?skip_thm_and_qed
+    (fun ?(prec=90) ast ->
+      CicNotationPres.box_of_mpres
+       (CicNotationPres.render ~lookup_uri ~prec (TermContentPres.pp_ast ast)))