diff --git a/src/haz3lcore/Measured.re b/src/haz3lcore/Measured.re
index 5ed9d0264d..206f13311e 100644
--- a/src/haz3lcore/Measured.re
+++ b/src/haz3lcore/Measured.re
@@ -435,3 +435,13 @@ let segment_width = (seg: Segment.t): int =>
     of_segment(seg).rows,
     0,
   );
+
+let width_cost = (seg: Segment.t, max_width: int): int =>
+  IntMap.fold(
+    (_, {max_col, _}: Rows.shape, acc) => {
+      let overflow = max(max_col - max_width, 0);
+      acc + overflow * overflow;
+    },
+    of_segment(seg).rows,
+    0,
+  );
diff --git a/src/haz3lcore/pretty/ExpToSegment.re b/src/haz3lcore/pretty/ExpToSegment.re
index 30284d4616..5505840624 100644
--- a/src/haz3lcore/pretty/ExpToSegment.re
+++ b/src/haz3lcore/pretty/ExpToSegment.re
@@ -15,9 +15,7 @@ let should_add_space = (s1, s2) =>
   | _ when String.starts_with(s2, ~prefix=" ") => false
   | _ when String.ends_with(s1, ~suffix="\n") => false
   | _ when String.starts_with(s2, ~prefix="\n") => false
-  | _ =>
-    print_endline("(\"" ++ s1 ++ "\")(\"" ++ s2 ++ "\")");
-    true;
+  | _ => true
   };
 
 let text_to_pretty = (id, sort, str): pretty => {
@@ -39,7 +37,6 @@ let mk_form = (form_name: string, id, children): Piece.t => {
   let children =
     Aba.map_abas(
       ((l, child, r)) => {
-        let _ = print_endline("l: " ++ l ++ " r: " ++ r);
         let lspace = should_add_space(l, child |> Segment.first_string);
         let rspace = should_add_space(child |> Segment.last_string, r);
         (lspace ? [Secondary(Secondary.mk_space(Id.mk()))] : [])
@@ -106,7 +103,7 @@ let rec exp_to_pretty = (~inline, exp: Exp.t): pretty => {
     let (id, ids) = (exp.ids |> List.hd, exp.ids |> List.tl);
     let* x = go(x)
     and* xs = xs |> List.map(go) |> all;
-    p_just([
+    let form = (x, xs) =>
       mk_form(
         "list_lit_exp",
         id,
@@ -120,8 +117,25 @@ let rec exp_to_pretty = (~inline, exp: Exp.t): pretty => {
               ),
             ),
         ],
-      ),
-    ]);
+      );
+    p_just([form(x, xs)])
+    |> p_orif(
+         !inline,
+         p_just(
+           {
+             let x = [Secondary(Secondary.mk_newline(Id.mk()))] @ x;
+             let xs =
+               xs
+               |> List.map(x =>
+                    [Secondary(Secondary.mk_newline(Id.mk()))] @ x
+                  )
+               |> ListUtil.map_last_only(x =>
+                    x @ [Secondary(Secondary.mk_newline(Id.mk()))]
+                  );
+             [form(x, xs)];
+           },
+         ),
+       );
   | Var(v) => text_to_pretty(exp |> Exp.rep_id, Sort.Exp, v)
   | BinOp(op, l, r) =>
     // TODO: Add optional newlines
diff --git a/src/haz3lcore/pretty/PrettySegment.re b/src/haz3lcore/pretty/PrettySegment.re
index 5a0d687eae..d874740ddb 100644
--- a/src/haz3lcore/pretty/PrettySegment.re
+++ b/src/haz3lcore/pretty/PrettySegment.re
@@ -7,7 +7,12 @@ let p_concat = (pretty2, pretty1) =>
   List.map(piece1 => List.map(piece2 => piece1 @ piece2, pretty2), pretty1)
   |> List.flatten;
 let p_or = (pretty2, pretty1) => pretty1 @ pretty2;
-let p_orif = (cond, pretty2, pretty1) => if (cond) {pretty1} else {pretty2};
+let p_orif = (cond, pretty2, pretty1) =>
+  if (cond) {
+    pretty1 @ pretty2;
+  } else {
+    pretty2;
+  };
 let p_just = segment => [segment];
 
 let p_concat = (pretties: list(pretty)) =>
@@ -26,3 +31,16 @@ let rec all =
       let rest = all(xs);
       List.flatten(List.map(x => List.map(rest => [x, ...rest], rest), x));
     };
+
+let select: pretty => Segment.t =
+  seg =>
+    ListUtil.minimum(
+      s => {
+        let u =
+          Measured.width_cost(s, 80) * 100 + Measured.segment_height(s);
+        print_endline(string_of_int(u));
+        u;
+      },
+      seg,
+    )
+    |> Option.get;
diff --git a/src/haz3lweb/view/dhcode/DHCode.re b/src/haz3lweb/view/dhcode/DHCode.re
index 788b10fc39..e05fbd73b2 100644
--- a/src/haz3lweb/view/dhcode/DHCode.re
+++ b/src/haz3lweb/view/dhcode/DHCode.re
@@ -187,7 +187,8 @@ let view =
     ) => {
   let parenthesized = ExpToSegment.parenthesize(d);
   let options = ExpToSegment.exp_to_pretty(~inline=false, parenthesized);
-  let option = List.hd(options);
+  let _ = print_endline("options: " ++ string_of_int(List.length(options)));
+  let option = PrettySegment.select(options);
   let editor = Editor.init(~read_only=true, Zipper.unzip(option));
   let code_text_view =
     Code.view(~sort=Sort.root, ~font_metrics, ~settings, editor);
diff --git a/src/util/ListUtil.re b/src/util/ListUtil.re
index 1998599688..1b7e9d0bc6 100644
--- a/src/util/ListUtil.re
+++ b/src/util/ListUtil.re
@@ -547,3 +547,21 @@ let rec split_last = (xs: list('x)): (list('x), 'x) =>
     let (prefix, last) = split_last(xs);
     ([x, ...prefix], last);
   };
+
+let minimum = (f: 'a => int, xs: list('a)): option('a) =>
+  switch (xs) {
+  | [] => None
+  | [x, ...xs] =>
+    let rec loop = (best: 'a, best_f: int, xs: list('a)): option('a) =>
+      switch (xs) {
+      | [] => Some(best)
+      | [x, ...xs] =>
+        let f_x = f(x);
+        if (f_x < best_f) {
+          loop(x, f_x, xs);
+        } else {
+          loop(best, best_f, xs);
+        };
+      };
+    loop(x, f(x), xs);
+  };