interim version (added smallLexer)

[helm.git] / matitaB / components / content_pres / termContentPres.ml

diff --git a/matitaB/components/content_pres/termContentPres.ml b/matitaB/components/content_pres/termContentPres.ml
index 53f0265b7ffff0a33d10cd5974bf4e9e9feef558..27b55ebc1353e4594e0e5311f3aca72283e205f8 100644 (file)
--- a/matitaB/components/content_pres/termContentPres.ml
+++ b/matitaB/components/content_pres/termContentPres.ml
@@ -467,7 +467,7 @@ let rec pp_ast1 status term =
         NotationEnv.OptValue (Some (pp_value v))
     | NotationEnv.ListValue vl ->
         NotationEnv.ListValue (List.map pp_value vl)
-    | NotationEnv.LocValue _ as v -> v
+    | NotationEnv.DisambiguationValue _ as v -> v
   in
   let ast_env_of_env env =
     List.map (fun (var, (ty, value)) -> (var, (ty, pp_value value))) env
@@ -575,7 +575,7 @@ let tail_names names env =
   in
   aux [] env
 
-let instantiate_level2 status env loc term =
+let instantiate_level2 status env (loc,uri,desc) term =
 (*   prerr_endline ("istanzio: " ^ NotationPp.pp_term term); *)
   let fresh_env = ref [] in
   let lookup_fresh_name n =
@@ -607,7 +607,7 @@ let instantiate_level2 status env loc term =
     | Ast.Num _
     | Ast.Sort _
     | Ast.UserInput -> term
-    | Ast.Symbol _ -> Ast.AttributedTerm (`Loc loc, term)
+    | Ast.Symbol (s,_) -> aux_symbol s loc (uri,desc)
 
     | Ast.Magic magic -> aux_magic env magic
     | Ast.Variable var -> aux_variable env var
@@ -615,6 +615,10 @@ let instantiate_level2 status env loc term =
     | Ast.Cast (t, ty) -> Ast.Cast (aux env t, aux env ty)
 
     | _ -> assert false
+  and aux_symbol s loc = function
+  | _, None -> Ast.AttributedTerm (`Loc loc, Ast.Symbol (s, None))
+  | uri, Some desc -> 
+      Ast.AttributedTerm (`Loc loc, Ast.Symbol (s, Some (uri,desc)))
   and aux_opt env = function
     | Some term -> Some (aux env term)
     | None -> None