Re: [isabelle] HTML string of term



Dear Cornelius,

I am afraid I still have no solution.

best,

2016-07-02 7:09 GMT-05:00 C. Diekmann <diekmann at in.tum.de>:

> 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
>



-- 
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.