X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcontent_pres%2FtermContentPres.ml;h=68cc4ccbb391e913a21b5fac7ca99419ae781c2d;hb=f9abd21eb0d26cf9b632af4df819225be4d091e3;hp=3fae0f52b05a00ea529b3b3acc96e8b4f46ef2d1;hpb=cf4a3f9226194e0f6dc9572dea1090e2bfa55219;p=helm.git

diff --git a/helm/software/components/content_pres/termContentPres.ml b/helm/software/components/content_pres/termContentPres.ml
index 3fae0f52b..68cc4ccbb 100644
--- a/helm/software/components/content_pres/termContentPres.ml
+++ b/helm/software/components/content_pres/termContentPres.ml
@@ -88,13 +88,21 @@ let binder_symbol s =
   add_xml_attrs (RenderingAttrs.builtin_symbol_attributes `MathML)
     (builtin_symbol s)
 
-let string_of_sort_kind = function
-  | `Prop -> "Prop"
-  | `Set -> "Set"
-  | `CProp _ -> "CProp"
-  | `Type _ -> "Type"
-  | `NType s -> "Type[" ^ s ^ "]"
-  | `NCProp s -> "CProp[" ^ s ^ "]"
+let xml_of_sort x = 
+  let to_string x = Ast.Ident (x, None) in
+  let identify x = 
+    add_xml_attrs (RenderingAttrs.keyword_attributes `MathML) (to_string x)
+  in
+  let lvl t = Ast.AttributedTerm (`Level 90,t) in
+  match x with
+  | `Prop -> identify "Prop"
+  | `Set -> identify "Set"
+  | `CProp _ -> identify "CProp"
+  | `Type _ -> identify "Type"
+  | `NType s -> lvl(Ast.Layout (Ast.Sub (identify "Type",to_string s)))
+  | `NCProp s -> lvl(Ast.Layout (Ast.Sub (identify "CProp",to_string s)))
+;;
+
 
 let map_space f l =
  HExtlib.list_concat
@@ -268,9 +276,7 @@ let pp_ast0 t k =
     | Ast.Literal _
     | Ast.UserInput as leaf -> leaf
     | t -> CicNotationUtil.visit_ast ~special_k k t
-  and aux_sort sort_kind =
-    add_xml_attrs (RenderingAttrs.keyword_attributes `MathML)
-      (Ast.Ident (string_of_sort_kind sort_kind, None))
+  and aux_sort sort_kind = xml_of_sort sort_kind
   and aux_ty = function
     | None -> builtin_symbol "?"
     | Some ty -> k ty