X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fcontent_pres%2FtermContentPres.ml;h=49d9241b96e8290ebef312443be7fa20811de9e3;hb=e880d6eab5e1700f4a625ddcd7d0fa8f0cce2dcc;hp=6846c30b5b9e608fe96af08fbb60b740ccf24b19;hpb=894d518aa760c9f816ddb0dc2b3fa88e1fe20a94;p=helm.git

diff --git a/matita/components/content_pres/termContentPres.ml b/matita/components/content_pres/termContentPres.ml
index 6846c30b5..49d9241b9 100644
--- a/matita/components/content_pres/termContentPres.ml
+++ b/matita/components/content_pres/termContentPres.ml
@@ -143,7 +143,7 @@ let pp_ast0 status t k =
         in
         let match_box =
           hvbox false false [
-           hvbox false true [
+           hvbox false false [
             hvbox false true [keyword "match"; space; break; top_pos (k what)];
             break;
             hvbox false true indty_box;
@@ -210,10 +210,11 @@ let pp_ast0 status t k =
               keyword "let"; space;
               hvbox false true [
                 aux_var var; space;
-                builtin_symbol "\\def"; break; top_pos (k s) ];
-              break; space; keyword "in"; space ];
+                builtin_symbol "\\def"; break; top_pos (k s); space; keyword "in"; space ];
+              ];
             break;
             k t ])
+(*
     | Ast.LetRec (rec_kind, funs, where) ->
         let rec_op =
           match rec_kind with `Inductive -> "rec" | `CoInductive -> "corec"
@@ -261,6 +262,7 @@ let pp_ast0 status t k =
           ((hvbox false false
             (fst_row :: List.flatten tl_rows
              @ [ break; keyword "in"; break; k where ])))
+*)
     | Ast.Implicit `JustOne -> builtin_symbol "?"
     | Ast.Implicit `Vector -> builtin_symbol "…"
     | Ast.Meta (n, l) ->
@@ -300,14 +302,14 @@ module IntMap = Map.Make(struct type t = int let compare = compare end);;
 
 type db = {
  level1_patterns21: NotationPt.term IntMap.t;
- compiled21: ((NotationPt.term -> (NotationEnv.t * NotationPt.term list * int) option)) Lazy.t option;
+ compiled21: ((NotationPt.term -> (NotationEnv.t * NotationPt.term list * int) option)) Lazy.t;
  pattern21_matrix: (NotationPt.term * pattern_id) list;
  counter: pattern_id
 }
 
 let initial_db = {
  level1_patterns21 = IntMap.empty;
- compiled21 = None;
+ compiled21 = lazy (Content2presMatcher.Matcher21.compiler []);
  pattern21_matrix = [];
  counter = ~-1 
 }
@@ -329,13 +331,11 @@ class virtual status =
  end
 
 let get_compiled21 status =
-  match status#content_pres_db.compiled21 with
-  | None -> assert false
-  | Some f -> Lazy.force f
+  Lazy.force status#content_pres_db.compiled21
 
 let set_compiled21 status f =
  status#set_content_pres_db
-  { status#content_pres_db with compiled21 = Some f }
+  { status#content_pres_db with compiled21 = f }
 
 let add_idrefs =
   List.fold_right (fun idref t -> Ast.AttributedTerm (`IdRef idref, t))
@@ -596,9 +596,11 @@ let instantiate_level2 status env term =
           List.map (aux_branch env) patterns)
     | Ast.LetIn (var, t1, t3) ->
         Ast.LetIn (aux_capture_var env var, aux env t1, aux env t3)
+(*    
     | Ast.LetRec (kind, definitions, body) ->
         Ast.LetRec (kind, List.map (aux_definition env) definitions,
           aux env body)
+*)    
     | Ast.Uri (name, None) -> Ast.Uri (name, None)
     | Ast.Uri (name, Some substs) ->
         Ast.Uri (name, Some (aux_substs env substs))