X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcontent_pres%2Fsequent2pres.ml;h=549f5c7c58d6437216b9c1d9320d19856938ee62;hb=11b2157bacf59cfc561c2ef6f92ee41ee2c1a006;hp=88c804b7d6a199fce46ae1b836960d8f6b024a1d;hpb=55b82bd235d82ff7f0a40d980effe1efde1f5073;p=helm.git

diff --git a/helm/software/components/content_pres/sequent2pres.ml b/helm/software/components/content_pres/sequent2pres.ml
index 88c804b7d..549f5c7c5 100644
--- a/helm/software/components/content_pres/sequent2pres.ml
+++ b/helm/software/components/content_pres/sequent2pres.ml
@@ -47,7 +47,7 @@ let b_ink a = Box.Ink a
 module K = Content
 module P = Mpresentation
 
-let sequent2pres term2pres (_,_,context,ty) =
+let sequent2pres0 term2pres (_,_,context,ty) =
    let context2pres context = 
      let rec aux accum =
      function 
@@ -64,7 +64,7 @@ let sequent2pres term2pres (_,_,context,ty) =
                (match dec_name with
                   None -> "_"
                 | Some n -> n)) ;
-               Box.b_text [] ":" ;
+               Box.b_space; Box.b_text [] ":"; Box.b_space;
                term2pres ty] in
          aux (r::accum) tl
      | (Some (`Definition d))::tl ->
@@ -77,30 +77,44 @@ let sequent2pres term2pres (_,_,context,ty) =
               [ Box.b_object (p_mi []
                 (match def_name with
                    None -> "_"
-                 | Some n -> n)) ;
-                 Box.b_text [] (Utf8Macro.unicode_of_tex "\\def") ;
-                term2pres bo] in
+                 | Some n -> n)) ; Box.b_space ;
+                Box.b_text [] (Utf8Macro.unicode_of_tex "\\def") ;
+                Box.b_space; term2pres bo] in
          aux (r::accum) tl
       | _::_ -> assert false in
       aux [] context in
- let pres_context = (Box.b_v [] (context2pres context)) in
+ let pres_context =
+  if context <> [] then [Box.b_v [] (context2pres context)] else [] in
  let pres_goal = term2pres ty in 
  (Box.b_h [] [
    Box.b_space; 
    (Box.b_v []
-      [Box.b_space;
-       pres_context;
+      (Box.b_space ::
+       pres_context @ [
        b_ink [None,"width","4cm"; None,"height","2px"]; (* sequent line *)
        Box.b_space; 
-       pres_goal])])
+       pres_goal]))])
 
 let sequent2pres ~ids_to_inner_sorts =
-  sequent2pres
+  sequent2pres0
     (fun annterm ->
       let ast, ids_to_uris =
-        TermAcicContent.ast_of_acic ids_to_inner_sorts annterm
+       TermAcicContent.ast_of_acic ~output_type:`Term ids_to_inner_sorts annterm
       in
       CicNotationPres.box_of_mpres
-        (CicNotationPres.render ids_to_uris
+        (CicNotationPres.render
+          ~lookup_uri:(CicNotationPres.lookup_uri ids_to_uris)
           (TermContentPres.pp_ast ast)))
 
+let nsequent2pres ~ids_to_nrefs ~subst =
+ 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
+  sequent2pres0
+    (fun ast ->
+      CicNotationPres.box_of_mpres
+       (CicNotationPres.render ~lookup_uri
+         (TermContentPres.pp_ast ast)))