update in ground_2 and basic_2

[helm.git] / matitaB / components / content / notationUtil.ml

diff --git a/matitaB/components/content/notationUtil.ml b/matitaB/components/content/notationUtil.ml
index 3d80e8fd51427a0d091335a95e186b1b4553d91f..dc914932a62bc60085b0d9c3e7e9ddfc62aaff30 100644 (file)
--- 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)) 
@@ -52,23 +53,22 @@ let visit_ast ?(special_k = fun _ -> assert false)
             definitions
         in
         Ast.LetRec (kind, definitions, k term)
-    | Ast.Ident (name, Some substs) ->
-        Ast.Ident (name, Some (aux_substs substs))
-    | Ast.Uri (name, Some substs) -> Ast.Uri (name, Some (aux_substs substs))
     | Ast.Meta (index, substs) -> Ast.Meta (index, List.map aux_opt substs)
     | (Ast.AttributedTerm _
       | Ast.Layout _
       | 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.Uri _
       | Ast.UserInput) as t -> t
   and aux_opt = function
     | None -> None
@@ -80,8 +80,6 @@ let visit_ast ?(special_k = fun _ -> assert false)
       Ast.Pattern (head, hrefs, vars), term ->
         Ast.Pattern (head, k_xref hrefs, List.map aux_capture_variable vars), k term
     | Ast.Wildcard, term -> Ast.Wildcard, k term
-  and aux_subst (name, term) = (name, k term)
-  and aux_substs substs = List.map aux_subst substs
   in
   aux
 
@@ -159,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
@@ -181,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 =
@@ -205,8 +202,6 @@ let meta_names_of_term term =
     | Ast.LetRec (_, definitions, body) ->
         List.iter aux_definition definitions ;
         aux body
-    | Ast.Uri (_, Some substs) -> aux_substs substs
-    | Ast.Ident (_, Some substs) -> aux_substs substs
     | Ast.Meta (_, substs) -> aux_meta_substs substs
 
     | Ast.Implicit _
@@ -214,7 +209,6 @@ let meta_names_of_term term =
     | Ast.Num _
     | Ast.Sort _
     | Ast.Symbol _
-    | Ast.Uri _
     | Ast.UserInput -> ()
 
     | Ast.Magic magic -> aux_magic magic
@@ -236,7 +230,6 @@ let meta_names_of_term term =
     List.iter aux_capture_var params ;
     aux_capture_var var ;
     aux term
-  and aux_substs substs = List.iter (fun (_, term) -> aux term) substs
   and aux_meta_substs meta_substs = List.iter aux_opt meta_substs
   and aux_variable = function
     | Ast.NumVar name -> add_name name
@@ -281,10 +274,25 @@ let ncombine ll =
   done;
   List.rev !lists
 
+let href s = function
+ | None, None -> s
+ | Some u, None -> "<A href=\"" ^ u ^ "\">" ^ s ^ "</A>"
+ | None, Some desc -> 
+     "<A href=\"cic:/fakeuri.con\" title=\"" ^ desc ^ "\">" ^ s ^ "</A>"
+ | Some u, Some desc -> 
+     "<A href=\"" ^ u ^ "\" title=\"" ^ desc ^ "\">" ^ s ^ "</A>"
+
 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
@@ -354,6 +362,9 @@ let fresh_id () =
   (* FG: "η" is not an identifier (it is rendered, but not be parsed) *)
 let fresh_name () = "eta" ^ string_of_int (fresh_id ())
 
+(* XXX FIXME: was used to add instance indices to symbols/numbers
+ * do we even need a similar operation? 
+ * currently an identity function! *)
 let rec freshen_term ?(index = ref 0) term =
   let freshen_term = freshen_term ~index in
   let fresh_instance () = incr index; !index in
@@ -366,8 +377,8 @@ let rec freshen_term ?(index = ref 0) term =
     | _ -> assert false
   in
   match term with
-  | Ast.Symbol (s, instance) -> Ast.Symbol (s, fresh_instance ())
-  | Ast.Num (s, instance) -> Ast.Num (s, fresh_instance ())
+  | Ast.Symbol (s, x) -> Ast.Symbol (s, x (* fresh_instance () *))
+  | Ast.Num (s, x) -> Ast.Num (s, x (* fresh_instance () *))
   | t -> visit_ast ~special_k freshen_term t
 
 let freshen_obj obj =