Breaking up long lines when pretty-printing

[marcoeilers]

As suggested in issue #544, this PR adds points for potential line breaks to the pretty printer, which enable the pretty-printer to break up long lines into multiple lines with proper indentation. Our pretty printer actually had that ability all along and had a target line width of 75 characters, but couldn't use it due to lack of possible line breaks.

After:

function TreeNode_isRoot(self_1: Ref): Ref
  requires issubtype(typeof(self_1), TreeNode())
  requires self_1 != null
  requires acc(tree(self_1), write)
  ensures issubtype(typeof(result), bool())
{
  __prim__bool___box__((unfolding acc(tree(self_1), write) in
    !object___bool__(self_1.TreeNode_parent)))
}

method main(_cthread_175: Ref, _caller_measures_175: Seq[Measure$], _residue_175: Perm)
  returns (_current_wait_level_175: Perm)
  requires _cthread_175 != null
  requires issubtype(typeof(_cthread_175), Thread_0())
  requires [true,
    perm(MustTerminate(_cthread_175)) == none &&
    ((forperm _r_28: Ref [MustInvokeBounded(_r_28)] :: false) &&
    ((forperm _r_28: Ref [MustInvokeUnbounded(_r_28)] :: false) &&
    ((forperm _r_28: Ref [_r_28.MustReleaseBounded] :: false) &&
    (forperm _r_28: Ref [_r_28.MustReleaseUnbounded] :: false))))]
  ensures [true,
    (forperm _r_27: Ref [MustInvokeBounded(_r_27)] :: false) &&
    ((forperm _r_27: Ref [MustInvokeUnbounded(_r_27)] :: false) &&
    ((forperm _r_27: Ref [_r_27.MustReleaseBounded] :: false) &&
    (forperm _r_27: Ref [_r_27.MustReleaseUnbounded] :: false)))]
{
  var BinarySearchTree_res: Ref
  var target: Ref
  module_names_0 := (module_names_0 union
    Set(_single(2147777202629415036263)))
  assert true &&
    (_single(134778768439155653066375051740024039746) in module_names_0)
  BinarySearchTree_res := new()
  inhale typeof(BinarySearchTree_res) == BinarySearchTree()
  inhale acc(_MaySet(BinarySearchTree_res, 170170373251925421444582457427464176135250765572418), write)
  inhale acc(_MaySet(BinarySearchTree_res, 148310513873082034654315146951689972238776244529474), write)
  _cwl_175 := BinarySearchTree___init__(_cthread_175, _method_measures_175,
    _residue_175, BinarySearchTree_res)
  inhale mytree() == BinarySearchTree_res
  module_names_0 := (module_names_0 union Set(_single(111486386338157)))
  _cwl_175 := BinarySearchTree___setitem__(_cthread_175, _method_measures_175,
    _residue_175, _asserting(_asserting(mytree(), true), true &&
    (_single(111486386338157) in module_names_0)), __prim__int___box__(3), str___create__(3,
    6579570))
  _cwl_175 := BinarySearchTree___setitem__(_cthread_175, _method_measures_175,
    _residue_175, _asserting(_asserting(mytree(), true), true &&
    (_single(111486386338157) in module_names_0)), __prim__int___box__(4), str___create__(4,
    1702194274))
  goto __end
  label __end
  assert (forall i: Int ::i > 0)
}

Before:

function TreeNode_isRoot(self_1: Ref): Ref
  requires issubtype(typeof(self_1), TreeNode())
  requires self_1 != null
  requires acc(tree(self_1), write)
  ensures issubtype(typeof(result), bool())
{
  __prim__bool___box__((unfolding acc(tree(self_1), write) in !object___bool__(self_1.TreeNode_parent)))
}

method main(_cthread_175: Ref, _caller_measures_175: Seq[Measure$], _residue_175: Perm) returns (_current_wait_level_175: Perm)
  requires _cthread_175 != null
  requires issubtype(typeof(_cthread_175), Thread_0())
  requires [true, perm(MustTerminate(_cthread_175)) == none && ((forperm _r_28: Ref [MustInvokeBounded(_r_28)] :: false) && ((forperm _r_28: Ref [MustInvokeUnbounded(_r_28)] :: false) && ((forperm _r_28: Ref [_r_28.MustReleaseBounded] :: false) && (forperm _r_28: Ref [_r_28.MustReleaseUnbounded] :: false))))]
  ensures [true, (forperm _r_27: Ref [MustInvokeBounded(_r_27)] :: false) && ((forperm _r_27: Ref [MustInvokeUnbounded(_r_27)] :: false) && ((forperm _r_27: Ref [_r_27.MustReleaseBounded] :: false) && (forperm _r_27: Ref [_r_27.MustReleaseUnbounded] :: false)))]
{
  var BinarySearchTree_res: Ref
  module_names_0 := (module_names_0 union Set(_single(6872323072689856351)))
  assert true && (_single(7306086878001066580) in module_names_0)
  BinarySearchTree_res := new()
  inhale typeof(BinarySearchTree_res) == BinarySearchTree()
  inhale acc(_MaySet(BinarySearchTree_res, 170170373251925421444582457427464176135250765572418), write)
  inhale acc(_MaySet(BinarySearchTree_res, 148310513873082034654315146951689972238776244529474), write)
  _cwl_175 := BinarySearchTree___init__(_cthread_175, _method_measures_175, _residue_175, BinarySearchTree_res)
  inhale mytree() == BinarySearchTree_res
  module_names_0 := (module_names_0 union Set(_single(111486386338157)))
  _cwl_175 := BinarySearchTree___setitem__(_cthread_175, _method_measures_175, _residue_175, _asserting(_asserting(mytree(), true), true && (_single(111486386338157) in module_names_0)), __prim__int___box__(3), str___create__(3, 6579570))
  _cwl_175 := BinarySearchTree___setitem__(_cthread_175, _method_measures_175, _residue_175, _asserting(_asserting(mytree(), true), true && (_single(111486386338157) in module_names_0)), __prim__int___box__(4), str___create__(4, 1702194274))
  goto __end
  label __end
  assert forall i: Int :: i > 0
}

[jcp19]

LGTM; all changes look reasonable and, testing it with SCION, I can already see that the output is a lot easier to grok