Formatter

[jwiesler]

The current Java formatter used in the sequent view is a mess. This PR tries to improve on that.

Current changes:

• Remove IOException out of the interface of all pretty printing functions since it is never thrown.
• Rewrite PrettyPrinter on top of Layouter
• Many changes to the interface of pretty printers
• Bring internal taclet printer to same format as key file formatter
• Warning when "decreases" clause is missing for loop spec (5b7829d and 5b7829d)
• Fix double click on proof management tree (d7efb02)

[wadoon]

My question would be: "Why writing/polishing the old Java pretty printing if libraries (e.g., google-java-format) are available?"

[jwiesler]

It isn't just Java formatting it's Java formatting with jml asserts, method-frames, modalities and all the other stuff.

[wadoon]

It isn't just Java formatting it's Java formatting with jml asserts, method-frames, modalities and all the other stuff.

Yes, and I would not built on top the Java parsing (which is realisied with Javac). I would go for the backend (the translation of Java AST into a document structure).

[jwiesler]

I would go for the backend (the translation of Java AST into a document structure).

What does that even mean?

There exist classes to layout the remaining formulas for a given document width which are general enough to handle the Java part as well.
I don't see where using another library for the Java part would make this any easier.

[jwiesler]

This is done, the parsability problems are fixed.

Making single line pretty printed terms more readable in the GUI is postponed until a later changed.