X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Focaml%2Fcic_notation%2FcicNotationRew.ml;h=e72bfacc8fc8f31da17982b27a0bda3be1b8f78e;hb=915c3e1993cad4dcadefe7e6886e6cb8feefae8b;hp=180a8c912f05484c451d856c30a3151586b71b58;hpb=ea7808d83a7d6e03c0e163f0691e268dcd7c2ea4;p=helm.git

diff --git a/helm/ocaml/cic_notation/cicNotationRew.ml b/helm/ocaml/cic_notation/cicNotationRew.ml
index 180a8c912..e72bfacc8 100644
--- a/helm/ocaml/cic_notation/cicNotationRew.ml
+++ b/helm/ocaml/cic_notation/cicNotationRew.ml
@@ -37,8 +37,6 @@ type term_info =
     uri: (Cic.id, string) Hashtbl.t;
   }
 
-let warning s = prerr_endline ("CicNotation WARNING: " ^ s)
-
 let get_types uri =
   let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
     match o with
@@ -81,9 +79,17 @@ let resolve_binder = function
   | `Forall -> "\\forall"
   | `Exists -> "\\exists"
 
+let binder_attributes = [None, "mathcolor", "blue"]
+let atop_attributes = [None, "linethickness", "0pt"]
+let indent_attributes = [None, "indent", "1em"]
+let keyword_attributes = [None, "mathcolor", "blue"]
+
 let pp_ast0 t k =
   let reset_href t = Ast.AttributedTerm (`Href [], t) in
   let builtin_symbol s = reset_href (Ast.Literal (`Symbol s)) in
+  let binder_symbol s =
+    Ast.AttributedTerm (`XmlAttrs binder_attributes, builtin_symbol s)
+  in
   let rec aux = function
     | Ast.Appl ts ->
         Ast.AttributedTerm (`Level (Parser.apply_prec, Parser.apply_assoc),
@@ -94,13 +100,13 @@ let pp_ast0 t k =
           Ast.Layout (Ast.Box ((Ast.HV, false, true), [
             aux_ty ty;
             Ast.Layout (Ast.Box ((Ast.H, false, false), [
-              builtin_symbol "\\to";
+              binder_symbol "\\to";
               k body]))])))
     | Ast.Binder (binder_kind, (id, ty), body) ->
         Ast.AttributedTerm (`Level (Parser.binder_prec, Parser.binder_assoc),
           Ast.Layout (Ast.Box ((Ast.HV, false, true), [
             Ast.Layout (Ast.Box ((Ast.H, false, false), [
-              builtin_symbol (resolve_binder binder_kind);
+              binder_symbol (resolve_binder binder_kind);
               k id;
               builtin_symbol ":";
               aux_ty ty ]));
@@ -118,7 +124,6 @@ let pp_ast0 t k =
   aux t
 
 let ast_of_acic0 term_info acic k =
-(*   prerr_endline "ast_of_acic0"; *)
   let k = k term_info in
   let register_uri id uri = Hashtbl.add term_info.uri id uri in
   let sort_of_id id =
@@ -265,7 +270,6 @@ let instantiate21 env (* precedence associativity *) l1 =
     | Ast.AttributedTerm (_, t) -> subst env t
     | Ast.Variable var ->
         let name, expected_ty = CicNotationEnv.declaration_of_var var in
-	  prerr_endline ("searching for " ^ name);
         let ty, value =
           try
             List.assoc name env
@@ -277,6 +281,8 @@ let instantiate21 env (* precedence associativity *) l1 =
         assert (CicNotationEnv.well_typed expected_ty value);
         [ CicNotationEnv.term_of_value value ]
     | Ast.Magic m -> subst_magic env m
+    | Ast.Literal (`Keyword k) as t ->
+        [ Ast.AttributedTerm (`XmlAttrs keyword_attributes, t) ]
     | Ast.Literal _ as t -> [ t ]
     | Ast.Layout l -> [ Ast.Layout (subst_layout env l) ]
     | t -> [ CicNotationUtil.visit_ast (subst_singleton env) t ]
@@ -325,7 +331,8 @@ let instantiate21 env (* precedence associativity *) l1 =
 	  end
     | _ -> assert false (* impossible *)
   and subst_layout env = function
-    | Ast.Box (kind, tl) -> Ast.Box (kind, List.concat (List.map (subst env) tl))
+    | Ast.Box (kind, tl) ->
+        Ast.Box (kind, List.concat (List.map (subst env) tl))
     | l -> CicNotationUtil.visit_layout (subst_singleton env) l
   in
     subst_singleton env l1
@@ -357,15 +364,9 @@ let rec pp_ast1 term =
 		  Hashtbl.find level1_patterns21 pid
 		with Not_found -> assert false
               in
-		prerr_endline ("IN " ^ CicNotationPp.pp_term term);
-		(* LUCA: il termine legato e' lo stesso termine di partenza per cui si innesca il loop infinito *)
-		let res = Ast.AttributedTerm (`Level (precedence, associativity),
-					      (instantiate21 (ast_env_of_env env) l1))
-		in
-		  prerr_endline "OUT";
-		  res
+		Ast.AttributedTerm (`Level (precedence, associativity),
+				(instantiate21 (ast_env_of_env env) l1))
       end
-  
 
 let instantiate32 term_info env symbol args =
   let rec instantiate_arg = function