]> matita.cs.unibo.it Git - helm.git/blobdiff - matitaB/components/content/notationUtil.mli
Added support for hyperlinks in the goal view of the web interface.
[helm.git] / matitaB / components / content / notationUtil.mli
index ac291a2cebc72156afa5ffb44c54380a4a158832..981030d49d8cc160e1a7f0245bcba4962f23e1a5 100644 (file)
@@ -33,6 +33,7 @@ val keywords_of_term: NotationPt.term -> string list
 
 val visit_ast:
   ?special_k:(NotationPt.term -> NotationPt.term) ->
+  ?clear_interpretation:bool ->
   ?map_xref_option:(NotationPt.href option -> NotationPt.href option) ->
   ?map_case_indty:(NotationPt.case_indtype option ->
           NotationPt.case_indtype option) ->
@@ -67,6 +68,7 @@ val get_idrefs: NotationPt.term -> string list
 val ncombine: 'a list list -> 'a list list
 
 val string_of_literal: NotationPt.literal -> string
+val html_of_literal: NotationPt.literal -> string 
 
 val dress:  sep:'a -> 'a list -> 'a list
 val dressn: sep:'a list -> 'a list -> 'a list