Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] HTML string of term

Email Gateway (Aug 22 2022 at 13:30):

From: Omar Montano Rivas <omarmrivas@gmail.com>
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,

Email Gateway (Aug 22 2022 at 13:42):

From: Omar Montano Rivas <omarmrivas@gmail.com>
Dear Cornelius,

I am afraid I still have no solution.

best,

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

Email Gateway (Aug 22 2022 at 13:46):

From: Omar Montano Rivas <omarmrivas@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,
induct_auto_breadth_first.html

Email Gateway (Aug 22 2022 at 13:48):

From: "C. Diekmann" <diekmann@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@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@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@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@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@upslp.edu.mx
Tel. +52 (444) 8126367 ext. 225
URL: http://atit.upslp.edu.mx/index.php/omarmrivas

Last updated: Apr 26 2024 at 12:28 UTC