Re: [isabelle] 2014-RC1 issues



On Thu, 31 Jul 2014, Peter Lammich wrote:


Depends how you write your source text.  jEdit folds and Sidekick trees
assume that the first line provides the main information.  This is also
the reason why I write definitions and theorem statements these days a bit
differently than in the past, when Proof General was still there.

My main restriction when writing proof text comes from the document
generation to latex, where I want a readable layout. And this forces me
to have no lines longer than roughly 80 characters. As I have many
longer lemma statements, I need to format them manually into multiple
lines.

Keeping lines short (80-100 chars for source, 60-70 chars for LaTeX documents) is important, but it is still possible to put relevant information into the head-line of a fold or sidekick item, e.g. like this:

  lemma name: short_statement
    <proof>

  lemma name:
    long_statement
    <proof>

  definition name :: type_constraints
    where short_definition

  definition name :: type_constraints
    where
      short_definition

Proper support for folds is still missing, but the general side-conditions for it are already given in jEdit.


	Makarius




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