[isabelle] HTML string of term



Hi,

Is there a way to obtain a string from a term ready to be presented in a
html page in Isabelle 2016?

I have the following code which works in Isabelle 2015:

fun html_string_of_term ctxt t =
    let
      val ctxt' = ctxt |> Config.put show_markup false
                       |> Config.put show_question_marks false
    in HTML.html_mode (Syntax.string_of_term ctxt') t end

but it seems that the method HTML.html_mode no longer exists in isabelle
2016.

Thanks,
-- 
Dr. Omar MontaÃo Rivas
Profesor-Investigador UPSLP
e-mail: omar.montano at upslp.edu.mx
Tel. +52 (444) 8126367 ext. 225
URL: http://atit.upslp.edu.mx/index.php/omarmrivas



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.