let hvbox = box Ast.HV
let hovbox = box Ast.HOV
let break = Ast.Layout Ast.Break
-let reset_href t = Ast.AttributedTerm (`Href [], t)
+(* let reset_href t = Ast.AttributedTerm (`Href [], t) *)
+let reset_href t = t
let builtin_symbol s = reset_href (Ast.Literal (`Symbol s))
let keyword k = reset_href (add_keyword_attrs (Ast.Literal (`Keyword k)))
let number s =
let sort_of_id id =
try
Hashtbl.find term_info.sort id
- with Not_found -> assert false
+ with Not_found ->
+ prerr_endline (sprintf "warning: sort of id %s not found, using Type" id);
+ `Type
in
let aux_substs substs =
Some
with Not_found -> assert false
in
let ast = instantiate32 term_info env' symbol args in
- match uris with
- | [] -> ast
- | _ -> Ast.AttributedTerm (`Href uris, ast)
+ Ast.AttributedTerm (`IdRef (CicUtil.id_of_annterm annterm),
+ (match uris with
+ | [] -> ast
+ | _ -> Ast.AttributedTerm (`Href uris, ast)))
let load_patterns32 t =
set_compiled32 (lazy (CicNotationMatcher.Matcher32.compiler t))