Re: [isabelle] Isabelle2013-2-RC2 available for testing

On Sun, 1 Dec 2013, Yannick Duchêne (Hibou57) wrote:

in the outline in the Sidekick, the keyword “end” appears for each construct terminated with an “end”. It's a bit like noise. May be an option could be to filter out this “end” or else tell the parser to handle “end” as if it was inside the construct.

Current Isabelle SideKick does not take any structure of Isar commands into account, neither proof blocks nor begin/end within theory specifications. Only some document markup commands are handled: chapter, section, subsection etc., which sometimes helps a little to keep an overview.

Right now the SideKick mode for the Isabelle NEWS file is of more practical importance.


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