X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fcomponents%2Fcontent%2FnotationUtil.ml;h=dc914932a62bc60085b0d9c3e7e9ddfc62aaff30;hb=ed36a3d3f81cf251c41bbe1d208376bb0709c600;hp=eeb1cd5c6f6992b80b32004f52ed09e3e19bd96c;hpb=a2412e41cda18a25d780ae631ee02d6ae05c52b1;p=helm.git
diff --git a/matitaB/components/content/notationUtil.ml b/matitaB/components/content/notationUtil.ml
index eeb1cd5c6..dc914932a 100644
--- a/matitaB/components/content/notationUtil.ml
+++ b/matitaB/components/content/notationUtil.ml
@@ -27,7 +27,8 @@
module Ast = NotationPt
-let visit_ast ?(special_k = fun _ -> assert false)
+let visit_ast ?(special_k = fun _ -> assert false)
+ ?(clear_interpretation= false)
?(map_xref_option= fun x -> x) ?(map_case_indty= fun x -> x)
?(map_case_outtype=
fun k x -> match x with None -> None | Some x -> Some (k x))
@@ -58,13 +59,16 @@ let visit_ast ?(special_k = fun _ -> assert false)
| Ast.Literal _
| Ast.Magic _
| Ast.Variable _) as t -> special_k t
- | (Ast.Ident _
+ | Ast.Ident (id,_) when clear_interpretation -> Ast.Ident (id,`Ambiguous)
+ | Ast.Symbol (s,_) when clear_interpretation -> Ast.Symbol (s,None)
+ | Ast.Num (n,_) when clear_interpretation -> Ast.Num (n,None)
+ | ( Ast.Ident _
+ | Ast.Symbol _
+ | Ast.Num _
| Ast.NRef _
| Ast.NCic _
| Ast.Implicit _
- | Ast.Num _
| Ast.Sort _
- | Ast.Symbol _
| Ast.UserInput) as t -> t
and aux_opt = function
| None -> None
@@ -153,7 +157,7 @@ let keywords_of_term t =
let rec aux = function
| Ast.AttributedTerm (_, t) -> aux t
| Ast.Layout l -> Ast.Layout (visit_layout aux l)
- | Ast.Literal (`Keyword k) as t ->
+ | Ast.Literal (_,`Keyword (k,_)) as t ->
add_keyword k;
t
| Ast.Literal _ as t -> t
@@ -175,8 +179,7 @@ let rec strip_attributes t =
let rec get_idrefs =
function
- | Ast.AttributedTerm (`IdRef id, t) -> id :: get_idrefs t
- | Ast.AttributedTerm (_, t) -> get_idrefs t
+ | Ast.Symbol (csym,Some (uri,desc)) -> [csym,uri,desc]
| _ -> []
let meta_names_of_term term =
@@ -271,10 +274,25 @@ let ncombine ll =
done;
List.rev !lists
+let href s = function
+ | None, None -> s
+ | Some u, None -> "" ^ s ^ ""
+ | None, Some desc ->
+ "" ^ s ^ ""
+ | Some u, Some desc ->
+ "" ^ s ^ ""
+
let string_of_literal = function
- | `Symbol s
- | `Keyword s
- | `Number s -> s
+ | `Symbol (s,x)
+ | `Keyword (s,x)
+ | `Number (s,x) -> href s x
+
+let html_of_literal = function
+ | `Symbol (s,x)
+ | `Keyword (s,x)
+ | `Number (s,x) ->
+ href (Netencoding.Html.encode ~in_enc:`Enc_utf8 ()
+ (Utf8Macro.unicode_of_tex s)) x
let boxify = function
| [ a ] -> a