Added support for hyperlinks in the goal view of the web interface.

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

diff --git a/matitaB/components/content/notationUtil.ml b/matitaB/components/content/notationUtil.ml
index eeb1cd5c6f6992b80b32004f52ed09e3e19bd96c..d047eb58e17f66a649ca89276c0ebacf6cc8c715 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)) 
@@ -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 (_,Some (_,desc)) -> [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 -> "<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