[isabelle-dev] \nexists

Makarius makarius at sketis.net
Tue Jul 19 15:52:28 CEST 2016


On 19/07/16 10:17, Lars Hupel wrote:
>>> How can I extract this information from within Isabelle/Scala? How would
>>> this information be presented?
>>
>> It is emitted into the session log file. Build.parse_log may serve as an
>> example how to access it.
> 
> Is there no structured way of accessing this information? At least it's
> Scala but it's also still the moral equivalent of grepping files, a
> technique I've managed to avoid so far.

It is already a bit more formal, due to the \f markers and the YXML data
representation.

One day it should all become PIDE document markup, i.e. YXML everywhere
without plain text in between.


	Makarius





More information about the isabelle-dev mailing list