Re: [isabelle] HTML string of term



Dear Omar,

did you find a solution? I would also be very interested in a function

  fun html_string_of_term ctxt t

Best,
  Cornelius

2016-07-01 16:33 GMT+02:00 Omar Montano Rivas <omarmrivas at gmail.com>:
>
> Thanks Peter!
>
> But still, it is not obvious to me how to obtain a similar
> html_string_of_term function in Isabelle 2016.
>
> 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
>
> Should I try to get 'keywords' and 'spans' from a term? What I am trying
to
> do is to report the performance of an inductive prover in html format (I
> attach a report generated with Isabelle 2015).
>
> Best,
>
>
> 2016-06-30 19:35 GMT-05:00 Peter Gammie <peteg42 at gmail.com>:
>
> > Omar,
> >
> > Digging into the hg repo, I found:
> >
> > changeset:   61379:c57820ceead3
> > user:        wenzelm
> > date:        Fri Oct 09 21:16:00 2015 +0200
> > summary:     more direct HTML presentation, without print mode;
> >
> > and this part of that patch may answer your question:
> >
> > diff --git a/src/Pure/PIDE/resources.ML b/src/Pure/PIDE/resources.ML
> > --- a/src/Pure/PIDE/resources.ML
> > +++ b/src/Pure/PIDE/resources.ML
> > @@ -159,7 +159,7 @@
> >      fun init () =
> >        begin_theory master_dir header parents
> >        |> Present.begin_theory update_time
> > -          (fn () => HTML.html_mode (implode o map
> > (Thy_Syntax.present_span keywords)) spans);
> > +        (fn () => implode (map (HTML.present_span keywords) spans));
> >
> >      val (results, thy) =
> >        cond_timeit true (âtheory " ^ quote name)
> >
> > cheers,
> > peter
> >
> > > On 1 Jul 2016, at 04:14, Omar Montano Rivas <omarmrivas at gmail.com>
> > wrote:
> > >
> > > 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
> >
> > --
> > http://peteg.org/
> >
> >
>
>
> --
> 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.