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

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

diff --git a/matitaB/components/content/notationPp.ml b/matitaB/components/content/notationPp.ml
index 082a5ddf81d16d40ca9249b93300b72eb8f54df7..50ccb16b47fb6cbaf1cf0c85acc0cfc7841f79f0 100644 (file)
--- a/matitaB/components/content/notationPp.ml
+++ b/matitaB/components/content/notationPp.ml
@@ -45,14 +45,12 @@ let pp_binder = function
 let pp_literal =
   if debug_printing then
     (function (* debugging version *)
-      | `Symbol s -> sprintf "symbol(%s)" s
-      | `Keyword s -> sprintf "keyword(%s)" s
-      | `Number s -> sprintf "number(%s)" s)
-  else
-    (function
-      | `Symbol s
-      | `Keyword s
-      | `Number s -> s)
+      | `Symbol _ as t -> 
+          sprintf "symbol(%s)" (NotationUtil.string_of_literal t)
+      | `Keyword _ as t -> 
+          sprintf "keyword(%s)" (NotationUtil.string_of_literal t)
+      | `Number _ as t -> sprintf "number(%s)" (NotationUtil.string_of_literal t))
+  else NotationUtil.string_of_literal
 
 let pp_pos =
   function