X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcontent_pres%2FtermContentPres.ml;h=110c78e46e43820fc4ae280e80090f9b35c40544;hb=683978a2627cf1ce15673360f26806593d22f7b5;hp=4c8bbc7d4e4af42ff8defbee358438dd0f139cf5;hpb=55b82bd235d82ff7f0a40d980effe1efde1f5073;p=helm.git

diff --git a/helm/software/components/content_pres/termContentPres.ml b/helm/software/components/content_pres/termContentPres.ml
index 4c8bbc7d4..110c78e46 100644
--- a/helm/software/components/content_pres/termContentPres.ml
+++ b/helm/software/components/content_pres/termContentPres.ml
@@ -75,6 +75,7 @@ let vbox = box Ast.V
 let hvbox = box Ast.HV
 let hovbox = box Ast.HOV
 let break = Ast.Layout Ast.Break
+let space = Ast.Literal (`Symbol " ")
 let builtin_symbol s = Ast.Literal (`Symbol s)
 let keyword k = add_keyword_attrs (Ast.Literal (`Keyword k))
 
@@ -128,24 +129,26 @@ let pp_ast0 t k =
           match outty_opt with
           | None -> []
           | Some outty ->
-              [ keyword "return"; break; remove_level_info (k outty)]
+              [ space; keyword "return"; space; break; remove_level_info (k outty)]
         in
         let indty_box =
           match indty_opt with
           | None -> []
-          | Some (indty, href) -> [ keyword "in"; break; ident_w_href href indty ]
+          | Some (indty, href) -> [ space; keyword "in"; space; break; ident_w_href href indty ]
         in
         let match_box =
           hvbox false false [
            hvbox false true [
-            hvbox false true [ keyword "match"; break; top_pos (k what) ];
+            hvbox false true [keyword "match"; space; break; top_pos (k what)];
             break;
             hvbox false true indty_box;
             break;
             hvbox false true outty_box
            ];
            break;
-           keyword "with"
+           space;
+           keyword "with";
+           space
          ]
         in
         let mk_case_pattern (head, href, vars) =
@@ -196,33 +199,52 @@ let pp_ast0 t k =
         add_level_info Ast.let_in_prec Ast.let_in_assoc
           (hvbox false true [
             hvbox false true [
-              keyword "let";
+              keyword "let"; space;
               hvbox false true [
-                aux_var var; builtin_symbol "\\def"; break; top_pos (k s) ];
-              break; keyword "in" ];
+                aux_var var; space; builtin_symbol "\\def"; break; top_pos (k s) ];
+              break; space; keyword "in" ];
             break;
             k t ])
     | Ast.LetRec (rec_kind, funs, where) ->
         let rec_op =
           match rec_kind with `Inductive -> "rec" | `CoInductive -> "corec"
         in
-        let mk_fun (var, body, _) = aux_var var, k body in
+        let mk_fun (args, (name,ty), body, rec_param) =
+         List.map aux_var args ,k name, HExtlib.map_option k ty, k body,  
+           fst (List.nth args rec_param)
+        in
         let mk_funs = List.map mk_fun in
         let fst_fun, tl_funs =
           match mk_funs funs with hd :: tl -> hd, tl | [] -> assert false
         in
         let fst_row =
-          let (name, body) = fst_fun in
-          hvbox false true [
-            keyword "let"; keyword rec_op; name; builtin_symbol "\\def"; break;
-            top_pos body ]
+          let (params, name, ty, body, rec_param) = fst_fun in
+          hvbox false true ([
+            keyword "let";
+            space;
+            keyword rec_op;
+            space;
+            name] @
+            params @
+            [space; keyword "on" ; space ; rec_param ;space ] @
+            (match ty with None -> [] | Some ty -> [builtin_symbol ":"; ty]) @
+            [ builtin_symbol "\\def";
+            break;
+            top_pos body ])
         in
         let tl_rows =
           List.map
-            (fun (name, body) ->
+            (fun (params, name, ty, body, rec_param) ->
               [ break;
-                hvbox false true [
-                  keyword "and"; name; builtin_symbol "\\def"; break; body ] ])
+                hvbox false true ([
+                  keyword "and";
+                  name] @
+                  params @
+                  [space; keyword "on" ; space; rec_param ;space ] @
+                  (match ty with
+                      None -> []
+                    | Some ty -> [builtin_symbol ":"; ty]) @
+                  [ builtin_symbol "\\def"; break; body ])])
             tl_funs
         in
         add_level_info Ast.let_in_prec Ast.let_in_assoc
@@ -232,12 +254,9 @@ let pp_ast0 t k =
     | Ast.Implicit -> builtin_symbol "?"
     | Ast.Meta (n, l) ->
         let local_context l =
-          CicNotationUtil.dress (builtin_symbol ";")
-            (List.map (function None -> builtin_symbol "_" | Some t -> k t) l)
+            List.map (function None -> None | Some t -> Some (k t)) l
         in
-        hbox false false
-          ([ builtin_symbol "?"; number (string_of_int n) ]
-            @ (if l <> [] then local_context l else []))
+        Ast.Meta(n, local_context l)
     | Ast.Sort sort -> aux_sort sort
     | Ast.Num _
     | Ast.Symbol _
@@ -558,8 +577,8 @@ let instantiate_level2 env term =
     (aux_pattern env pattern, aux env term)
   and aux_pattern env (head, hrefs, vars) =
     (head, hrefs, List.map (aux_capture_var env) vars)
-  and aux_definition env (var, term, i) =
-    (aux_capture_var env var, aux env term, i)
+  and aux_definition env (params, var, term, i) =
+    (List.map (aux_capture_var env) params, aux_capture_var env var, aux env term, i)
   and aux_substs env substs =
     List.map (fun (name, term) -> (name, aux env term)) substs
   and aux_meta_substs env meta_substs = List.map (aux_opt env) meta_substs