Re: [isabelle] Recommended use of try and try0



On 11.03.2013 17:22, Jasmin Christian Blanchette wrote:
Hi Gottfried,
I found this in the mailing list archives:

    ML_command "Toplevel.timing := true"

I think that's what it is. I'm still using Proof General, and there it's activated by going to "Isabelle>  Settings>  Global Timing".

When I put that in, the Isar commands have an orange line under them. If I hover over them, some give timing information, and some don't. If I change "by" to "apply", then I get timing information, but "by" by itself doesn't give any timing information.

I don't know what the feature looks like in jEdit.

In jEdit you will get somehow unpredictable behaviour, as Toplevel.timing is global state. In particular, there is no clean way to disable it.

  -- Lars




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