diff --git a/src/haz3lcore/lang/Form.re b/src/haz3lcore/lang/Form.re
index 9fe3c61928..bc7fb68dfb 100644
--- a/src/haz3lcore/lang/Form.re
+++ b/src/haz3lcore/lang/Form.re
@@ -331,7 +331,7 @@ let forms: list((string, t)) = [
 ];
 
 let get: String.t => t =
-  name => Util.ListUtil.assoc_err(name, forms, "Forms.get");
+  name => Util.ListUtil.assoc_err(name, forms, "Forms.get : " ++ name);
 
 let delims: list(Token.t) =
   forms
diff --git a/src/haz3lcore/lang/Precedence.re b/src/haz3lcore/lang/Precedence.re
index 6fc0dcfe73..b6344acfae 100644
--- a/src/haz3lcore/lang/Precedence.re
+++ b/src/haz3lcore/lang/Precedence.re
@@ -19,6 +19,7 @@ let unquote = 1;
 let cast = 2;
 let ap = 3;
 // _____(x)
+// - _____
 let neg = 4;
 // _____ ** 2
 let power = 5;
diff --git a/src/haz3lcore/pretty/ExpToSegment.re b/src/haz3lcore/pretty/ExpToSegment.re
index 377fde8043..b837f3d525 100644
--- a/src/haz3lcore/pretty/ExpToSegment.re
+++ b/src/haz3lcore/pretty/ExpToSegment.re
@@ -1,3 +1,4 @@
+open Util;
 open PrettySegment;
 open Base;
 
@@ -13,42 +14,419 @@ let text_to_pretty = (id, sort, str): pretty => {
   ]);
 };
 
-// /* We assume that parentheses have already been added as necessary, and
-//       that the expression has no DynamicErrorHoles, Casts, or FailedCasts
-//    */
-// let rec exp_to_pretty = (~inline, exp: Exp.t): pretty => {
-//   let go = exp_to_pretty(~inline);
-//   switch (exp |> Exp.term_of) {
-//   | Invalid(x) => text_to_pretty(exp |> Exp.rep_id, Sort.Exp, x)
-//   | EmptyHole =>
-//     let id = exp |> Exp.rep_id;
-//     p_just([Grout({id, shape: Convex})]);
-//   | Bool(b) => text_to_pretty(exp |> Exp.rep_id, Sort.Exp, Bool.to_string(b))
-//   | Int(n) => text_to_pretty(exp |> Exp.rep_id, Sort.Exp, Int.to_string(n))
-//   // TODO: do floats print right?
-//   | Float(f) =>
-//     text_to_pretty(exp |> Exp.rep_id, Sort.Exp, Float.to_string(f))
-//   | String(s) =>
-//     text_to_pretty(exp |> Exp.rep_id, Sort.Exp, "\"" ++ s ++ "\"")
-//   | Var(v) => text_to_pretty(exp |> Exp.rep_id, Sort.Exp, v)
-//   // TODO: add multi-line binop support?
-//   | BinOp(op, l, r) =>
-//     let id = exp |> Exp.rep_id;
-//     let+ l = go(l)
-//     and+ r = go(r);
-//     l
-//     @ [
-//       Tile({
-//         id,
-//         label: [Operators.bin_op_to_string(op)],
-//         mold: Mold.mk_bin(Precedence.of_bin_op(op), Sort.Exp, []),
-//         shards: [0],
-//         children: [l, r],
-//       }),
-//     ]
-//     @ r;
-//   };
-// };
+let mk_form = (form_name: string, id, children): Piece.t => {
+  let form: Form.t = Form.get(form_name);
+  assert(List.length(children) == List.length(form.mold.in_));
+  Tile({
+    id,
+    label: form.label,
+    mold: form.mold,
+    shards: List.init(List.length(children) + 1, n => n),
+    children,
+  });
+};
+
+/* We assume that parentheses have already been added as necessary, and
+      that the expression has no DynamicErrorHoles, Casts, or FailedCasts
+   */
+let rec exp_to_pretty = (~inline, exp: Exp.t): pretty => {
+  let go = exp_to_pretty(~inline);
+  switch (exp |> Exp.term_of) {
+  // Assume these have been removed by the parenthesizer
+  | DynamicErrorHole(_)
+  | Cast(_)
+  | FailedCast(_)
+  | Closure(_)
+  | Filter(_) => failwith("printing these not implemented yet")
+  // Other cases
+  | Invalid(x) => text_to_pretty(exp |> Exp.rep_id, Sort.Exp, x)
+  | EmptyHole =>
+    let id = exp |> Exp.rep_id;
+    p_just([Grout({id, shape: Convex})]);
+  | Bool(b) => text_to_pretty(exp |> Exp.rep_id, Sort.Exp, Bool.to_string(b))
+  | Int(n) => text_to_pretty(exp |> Exp.rep_id, Sort.Exp, Int.to_string(n))
+  // TODO: do floats print right?
+  | Float(f) =>
+    text_to_pretty(exp |> Exp.rep_id, Sort.Exp, Float.to_string(f))
+  | String(s) =>
+    text_to_pretty(exp |> Exp.rep_id, Sort.Exp, "\"" ++ s ++ "\"")
+  | Constructor(c) => text_to_pretty(exp |> Exp.rep_id, Sort.Exp, c)
+  | ListLit([]) => text_to_pretty(exp |> Exp.rep_id, Sort.Exp, "[]")
+  | Deferral(_) => text_to_pretty(exp |> Exp.rep_id, Sort.Exp, "deferral")
+  | ListLit([x, ...xs]) =>
+    let (id, ids) = (exp.ids |> List.hd, exp.ids |> List.tl);
+    let* x = go(x)
+    and* xs = xs |> List.map(go) |> all;
+    p_just([
+      mk_form(
+        "list_lit_exp",
+        id,
+        [
+          x
+          @ List.flatten(
+              List.map2(
+                (id, x) => [mk_form("comma_exp", id, [])] @ x,
+                ids,
+                xs,
+              ),
+            ),
+        ],
+      ),
+    ]);
+  | Var(v) => text_to_pretty(exp |> Exp.rep_id, Sort.Exp, v)
+  | BinOp(op, l, r) =>
+    let id = exp |> Exp.rep_id;
+    let+ l = go(l)
+    and+ r = go(r);
+    l
+    @ [
+      Tile({
+        id,
+        label: [Operators.bin_op_to_string(op)],
+        mold: Mold.mk_bin(Precedence.of_bin_op(op), Sort.Exp, []),
+        shards: [0],
+        children: [],
+      }),
+    ]
+    @ r;
+  | MultiHole(es) =>
+    let id = exp |> Exp.rep_id;
+    let+ es = es |> List.map(any_to_pretty(~inline)) |> all;
+    ListUtil.flat_intersperse(Grout({id, shape: Concave}), es);
+  | Fun(p, e, _, _) =>
+    let id = exp |> Exp.rep_id;
+    let+ p = pat_to_pretty(~inline, p)
+    and+ e = go(e);
+    [mk_form("fun_", id, [p])] @ e;
+  | TypFun(tp, e, _) =>
+    let id = exp |> Exp.rep_id;
+    let+ tp = tpat_to_pretty(~inline, tp)
+    and+ e = go(e);
+    [mk_form("typfun", id, [tp])] @ e;
+  | Tuple([]) =>
+    let id = exp |> Exp.rep_id;
+    p_just([mk_form("ap_exp_empty", id, [])]);
+  | Tuple([_]) => failwith("Singleton Tuples are not allowed")
+  | Tuple([x, ...xs]) =>
+    let ids = exp.ids;
+    let+ x = go(x)
+    and+ xs = xs |> List.map(go) |> all;
+    x
+    @ List.flatten(
+        List.map2((id, x) => [mk_form("comma_exp", id, [])] @ x, ids, xs),
+      );
+  | Let(p, e1, e2) =>
+    let id = exp |> Exp.rep_id;
+    let+ p = pat_to_pretty(~inline, p)
+    and+ e1 = go(e1)
+    and+ e2 = go(e2);
+    [mk_form("let_", id, [p, e1])] @ e2;
+  | FixF(p, e, _) =>
+    let id = exp |> Exp.rep_id;
+    let+ p = pat_to_pretty(~inline, p)
+    and+ e = go(e);
+    [mk_form("fix", id, [p])] @ e;
+  | TyAlias(tp, t, e) =>
+    let id = exp |> Exp.rep_id;
+    let+ tp = tpat_to_pretty(~inline, tp)
+    and+ t = typ_to_pretty(~inline, t)
+    and+ e = go(e);
+    [mk_form("tyalias", id, [tp, t])] @ e;
+  | Ap(Forward, e1, e2) =>
+    let id = exp |> Exp.rep_id;
+    let+ e1 = go(e1)
+    and+ e2 = go(e2);
+    e1 @ [mk_form("ap_exp", id, [e2])];
+  | Ap(Reverse, e1, e2) =>
+    let id = exp |> Exp.rep_id;
+    let+ e1 = go(e1)
+    and+ e2 = go(e2)
+    and+ op = text_to_pretty(id, Sort.Exp, "|>");
+    e1 @ op @ e2;
+  | TypAp(e, t) =>
+    let id = exp |> Exp.rep_id;
+    let+ e = go(e)
+    and+ tp = typ_to_pretty(~inline, t);
+    e @ [mk_form("ap_exp_typ", id, [tp])];
+  | DeferredAp(e, es) =>
+    let (id, ids) = (exp.ids |> List.hd, exp.ids |> List.tl);
+    let+ e = go(e)
+    and+ es = es |> List.map(go) |> all;
+    e
+    @ [
+      mk_form(
+        "ap_exp",
+        id,
+        [
+          List.flatten(
+            List.map2(
+              (id, e) => [mk_form("comma_exp", id, [])] @ e,
+              ids,
+              es,
+            ),
+          ),
+        ],
+      ),
+    ];
+  | If(e1, e2, e3) =>
+    let id = exp |> Exp.rep_id;
+    let+ e1 = go(e1)
+    and+ e2 = go(e2)
+    and+ e3 = go(e3);
+    [mk_form("if_", id, [e1, e2])] @ e3;
+  | Seq(e1, e2) =>
+    let id = exp |> Exp.rep_id;
+    let+ e1 = go(e1)
+    and+ e2 = go(e2);
+    e1 @ [mk_form("cell-join", id, [])] @ e2;
+  | Test(e) =>
+    let id = exp |> Exp.rep_id;
+    let+ e = go(e);
+    [mk_form("test", id, [])] @ e;
+  | Parens(e) =>
+    let id = exp |> Exp.rep_id;
+    let+ e = go(e);
+    [mk_form("parens_exp", id, [e])];
+  | Cons(e1, e2) =>
+    let id = exp |> Exp.rep_id;
+    let+ e1 = go(e1)
+    and+ e2 = go(e2);
+    e1 @ [mk_form("cons_exp", id, [])] @ e2;
+  | ListConcat(e1, e2) =>
+    let id = exp |> Exp.rep_id;
+    let+ e1 = go(e1)
+    and+ e2 = go(e2);
+    e1 @ [mk_form("list_concat", id, [])] @ e2;
+  | UnOp(Meta(Unquote), e) =>
+    let id = exp |> Exp.rep_id;
+    let+ e = go(e);
+    [mk_form("unquote", id, [])] @ e;
+  | UnOp(Bool(Not), e) =>
+    let id = exp |> Exp.rep_id;
+    let+ e = go(e);
+    [mk_form("not", id, [])] @ e;
+  | UnOp(Int(Minus), e) =>
+    let id = exp |> Exp.rep_id;
+    let+ e = go(e);
+    [mk_form("unary_minus", id, [])] @ e;
+  /* TODO: this isn't actually correct because we could the builtin
+     could have been overriden in this scope; worth fixing when we fix
+     closures. */
+  | BuiltinFun(f) => text_to_pretty(exp |> Exp.rep_id, Sort.Exp, f)
+  | Match(e, rs) =>
+    let (id, ids) = (exp.ids |> List.hd, exp.ids |> List.tl);
+    let+ e = go(e)
+    and+ rs: list(list((Segment.t, Segment.t))) = {
+      rs
+      |> List.map(((p, e)) => (pat_to_pretty(~inline, p), go(e)))
+      |> List.map(((x, y)) => ListUtil.cross(x, y))
+      |> all;
+    };
+    [
+      mk_form(
+        "case",
+        id,
+        [
+          e
+          @ (
+            List.map2(
+              (id, (p, e)) => [mk_form("rule", id, [p])] @ e,
+              ids,
+              rs,
+            )
+            |> List.flatten
+          ),
+        ],
+      ),
+    ];
+  };
+}
+and pat_to_pretty = (~inline, pat: Pat.t): pretty => {
+  let go = pat_to_pretty(~inline);
+  switch (pat |> Pat.term_of) {
+  | Invalid(t) => text_to_pretty(pat |> Pat.rep_id, Sort.Pat, t)
+  | EmptyHole =>
+    let id = pat |> Pat.rep_id;
+    p_just([Grout({id, shape: Convex})]);
+  | Wild => text_to_pretty(pat |> Pat.rep_id, Sort.Pat, "_")
+  | Var(v) => text_to_pretty(pat |> Pat.rep_id, Sort.Pat, v)
+  | Int(n) => text_to_pretty(pat |> Pat.rep_id, Sort.Pat, Int.to_string(n))
+  | Float(f) =>
+    text_to_pretty(pat |> Pat.rep_id, Sort.Pat, Float.to_string(f))
+  | Bool(b) => text_to_pretty(pat |> Pat.rep_id, Sort.Pat, Bool.to_string(b))
+  | String(s) =>
+    text_to_pretty(pat |> Pat.rep_id, Sort.Pat, "\"" ++ s ++ "\"")
+  | Constructor(c) => text_to_pretty(pat |> Pat.rep_id, Sort.Pat, c)
+  | ListLit([]) => text_to_pretty(pat |> Pat.rep_id, Sort.Pat, "[]")
+  | ListLit([x, ...xs]) =>
+    let (id, ids) = (pat.ids |> List.hd, pat.ids |> List.tl);
+    let* x = go(x)
+    and* xs = xs |> List.map(go) |> all;
+    p_just([
+      mk_form(
+        "list_lit_pat",
+        id,
+        [
+          x
+          @ List.flatten(
+              List.map2(
+                (id, x) => [mk_form("comma_pat", id, [])] @ x,
+                ids,
+                xs,
+              ),
+            ),
+        ],
+      ),
+    ]);
+  | Cons(p1, p2) =>
+    let id = pat |> Pat.rep_id;
+    let+ p1 = go(p1)
+    and+ p2 = go(p2);
+    p1 @ [mk_form("cons_pat", id, [])] @ p2;
+  | Tuple([]) => text_to_pretty(pat |> Pat.rep_id, Sort.Pat, "()")
+  | Tuple([_]) => failwith("Singleton Tuples are not allowed")
+  | Tuple([x, ...xs]) =>
+    let ids = pat.ids;
+    let+ x = go(x)
+    and+ xs = xs |> List.map(go) |> all;
+    x
+    @ List.flatten(
+        List.map2((id, x) => [mk_form("comma_pat", id, [])] @ x, ids, xs),
+      );
+  | Parens(p) =>
+    let id = pat |> Pat.rep_id;
+    let+ p = go(p);
+    [mk_form("parens_pat", id, [p])];
+  | MultiHole(es) =>
+    let id = pat |> Pat.rep_id;
+    let+ es = es |> List.map(any_to_pretty(~inline)) |> all;
+    ListUtil.flat_intersperse(Grout({id, shape: Concave}), es);
+  | Ap(p1, p2) =>
+    let id = pat |> Pat.rep_id;
+    let+ p1 = go(p1)
+    and+ p2 = go(p2);
+    p1 @ [mk_form("ap_pat", id, [p2])];
+  | Cast(p, t, _) =>
+    let id = pat |> Pat.rep_id;
+    let+ p = go(p)
+    and+ t = typ_to_pretty(~inline, t);
+    p @ [mk_form("typeann", id, [])] @ t;
+  };
+}
+and typ_to_pretty = (~inline, typ: Typ.t): pretty => {
+  let go = typ_to_pretty(~inline);
+  let go_constructor: ConstructorMap.variant(Typ.t) => pretty =
+    fun
+    | Variant(c, ids, None) => text_to_pretty(List.hd(ids), Sort.Typ, c)
+    | Variant(c, ids, Some(x)) => {
+        let+ constructor =
+          text_to_pretty(List.hd(List.tl(ids)), Sort.Typ, c);
+        constructor @ [mk_form("ap_typ", List.hd(ids), go(x))];
+      }
+    | BadEntry(x) => go(x);
+  switch (typ |> Typ.term_of) {
+  | Unknown(Hole(Invalid(s))) =>
+    text_to_pretty(typ |> Typ.rep_id, Sort.Typ, s)
+  | Unknown(Internal)
+  | Unknown(SynSwitch)
+  | Unknown(Hole(EmptyHole)) =>
+    let id = typ |> Typ.rep_id;
+    p_just([Grout({id, shape: Convex})]);
+  | Unknown(Hole(MultiHole(es))) =>
+    let id = typ |> Typ.rep_id;
+    let+ es = es |> List.map(any_to_pretty(~inline)) |> all;
+    ListUtil.flat_intersperse(Grout({id, shape: Concave}), es);
+  | Var(v) => text_to_pretty(typ |> Typ.rep_id, Sort.Typ, v)
+  | Int => text_to_pretty(typ |> Typ.rep_id, Sort.Typ, "Int")
+  | Float => text_to_pretty(typ |> Typ.rep_id, Sort.Typ, "Float")
+  | Bool => text_to_pretty(typ |> Typ.rep_id, Sort.Typ, "Bool")
+  | String => text_to_pretty(typ |> Typ.rep_id, Sort.Typ, "String")
+  | List(t) =>
+    let id = typ |> Typ.rep_id;
+    let+ t = go(t);
+    [mk_form("list_typ", id, [t])];
+  | Prod([]) => text_to_pretty(typ |> Typ.rep_id, Sort.Typ, "()")
+  | Prod([_]) => failwith("Singleton Prods are not allowed")
+  | Prod([t, ...ts]) =>
+    let+ t = go(t)
+    and+ ts = ts |> List.map(go) |> all;
+    t
+    @ List.flatten(
+        List.map2(
+          (id, t) => [mk_form("comma_typ", id, [])] @ t,
+          typ.ids,
+          ts,
+        ),
+      );
+  | Parens(t) =>
+    let id = typ |> Typ.rep_id;
+    let+ t = go(t);
+    [mk_form("parens_typ", id, [t])];
+  | Ap(t1, t2) =>
+    let id = typ |> Typ.rep_id;
+    let+ t1 = go(t1)
+    and+ t2 = go(t2);
+    t1 @ [mk_form("ap_typ", id, [t2])];
+  | Rec(tp, t) =>
+    let id = typ |> Typ.rep_id;
+    let+ tp = tpat_to_pretty(~inline, tp)
+    and+ t = go(t);
+    [mk_form("rec", id, [tp])] @ t;
+  | Forall(tp, t) =>
+    let id = typ |> Typ.rep_id;
+    let+ tp = tpat_to_pretty(~inline, tp)
+    and+ t = go(t);
+    [mk_form("forall", id, [tp])] @ t;
+  | Arrow(t1, t2) =>
+    let id = typ |> Typ.rep_id;
+    let+ t1 = go(t1)
+    and+ t2 = go(t2);
+    t1 @ [mk_form("arrow", id, [])] @ t2;
+  | Sum([]) => failwith("Empty Sums are not allowed")
+  | Sum([t]) =>
+    let id = typ |> Typ.rep_id;
+    let+ t = go_constructor(t);
+    [mk_form("typ_sum_single", id, [])] @ t;
+  | Sum([t, ...ts]) =>
+    let+ t = go_constructor(t)
+    and+ ts = ts |> List.map(go_constructor) |> all;
+    t
+    @ List.flatten(
+        List.map2(
+          (id, t) => [mk_form("typ_plus", id, [])] @ t,
+          typ.ids,
+          ts,
+        ),
+      );
+  };
+}
+and tpat_to_pretty = (~inline, tpat: TPat.t): pretty => {
+  switch (tpat |> IdTagged.term_of) {
+  | Invalid(t) => text_to_pretty(tpat |> TPat.rep_id, Sort.Typ, t)
+  | EmptyHole =>
+    let id = tpat |> TPat.rep_id;
+    p_just([Grout({id, shape: Convex})]);
+  | MultiHole(xs) =>
+    let id = tpat |> TPat.rep_id;
+    let+ xs = xs |> List.map(any_to_pretty(~inline)) |> all;
+    ListUtil.flat_intersperse(Grout({id, shape: Concave}), xs);
+  | Var(v) => text_to_pretty(tpat |> TPat.rep_id, Sort.Typ, v)
+  };
+}
+and any_to_pretty = (~inline, any: Any.t): pretty => {
+  switch (any) {
+  | Exp(e) => exp_to_pretty(~inline, e)
+  | Pat(p) => pat_to_pretty(~inline, p)
+  | Typ(t) => typ_to_pretty(~inline, t)
+  | TPat(tp) => tpat_to_pretty(~inline, tp)
+  | Any(_)
+  | Nul(_)
+  | Rul(_) =>
+    //TODO: print out invalid rules properly
+    let id = any |> Any.rep_id;
+    p_just([Grout({id, shape: Convex})]);
+  };
+};
 
 // Use Precedence.re to work out where your construct goes here.
 let rec external_precedence = (exp: Exp.t): Precedence.t => {
@@ -162,8 +540,12 @@ let rec parenthesize = (exp: Exp.t): Exp.t => {
   | BuiltinFun(_) => exp
 
   // Forms that currently need to stripped before oututting
-  | Closure(_, x) => x
-  | DynamicErrorHole(x, _) => x
+  | Closure(_, x)
+  | DynamicErrorHole(x, _)
+  | Tuple([x])
+  | Filter(_, x)
+  | Cast(x, _, _)
+  | FailedCast(x, _, _) => x |> parenthesize
 
   // Other forms
   | Fun(p, e, c, n) =>
@@ -248,12 +630,12 @@ let rec parenthesize = (exp: Exp.t): Exp.t => {
     )
     |> rewrap
   | Test(e) => Test(parenthesize(e) |> paren_at(Precedence.min)) |> rewrap
-  | Filter(f, e) =>
-    Filter(
-      f, // TODO: Filters
-      parenthesize(e) |> paren_at(Precedence.min),
-    )
-    |> rewrap
+  // | Filter(f, e) =>
+  //   Filter(
+  //     f, // TODO: Filters
+  //     parenthesize(e) |> paren_at(Precedence.min),
+  //   )
+  //   |> rewrap
   | Parens(e) =>
     Parens(parenthesize(e) |> paren_at(Precedence.min)) |> rewrap
   | Cons(e1, e2) =>
@@ -295,17 +677,9 @@ let rec parenthesize = (exp: Exp.t): Exp.t => {
     )
     |> rewrap
   | MultiHole(_) => exp // TODO: Parenthesize through multiholes
-  | Cast(e, t1, t2) =>
-    // TODO: Types
-    Cast(parenthesize(e) |> paren_assoc_at(Precedence.cast), t1, t2)
-    |> rewrap
-  | FailedCast(e, t1, t2) =>
-    // TODO: Types
-    FailedCast(parenthesize(e) |> paren_assoc_at(Precedence.cast), t1, t2)
-    |> rewrap
   };
 }
 and parenthesize_pat = (pat: Pat.t): Pat.t => {
   // TODO: patterns
-  pat;
+  pat /* TODO: Ensure each expr has enough ids*/;
 };
diff --git a/src/haz3lcore/pretty/PrettySegment.re b/src/haz3lcore/pretty/PrettySegment.re
index 67b5e089a2..5a0d687eae 100644
--- a/src/haz3lcore/pretty/PrettySegment.re
+++ b/src/haz3lcore/pretty/PrettySegment.re
@@ -18,3 +18,11 @@ let (and+) = (pretty1, pretty2) => ListUtil.cross(pretty1, pretty2);
 
 let ( let* ) = (pretty, f) => List.map(f, pretty) |> List.flatten;
 let ( and* ) = (pretty1, pretty2) => ListUtil.cross(pretty1, pretty2);
+
+let rec all =
+  fun
+  | [] => [[]]
+  | [x, ...xs] => {
+      let rest = all(xs);
+      List.flatten(List.map(x => List.map(rest => [x, ...rest], rest), x));
+    };
diff --git a/src/haz3lweb/view/Cell.re b/src/haz3lweb/view/Cell.re
index 58cbd24771..368044cdbf 100644
--- a/src/haz3lweb/view/Cell.re
+++ b/src/haz3lweb/view/Cell.re
@@ -186,7 +186,7 @@ let live_eval =
     DHCode.view(
       ~locked,
       ~inject,
-      ~settings=settings.core.evaluation,
+      ~settings,
       ~selected_hole_instance=None,
       ~font_metrics,
       ~width=80,
@@ -241,7 +241,7 @@ let footer =
   | Stepper(s) =>
     StepperView.stepper_view(
       ~inject,
-      ~settings=settings.core.evaluation,
+      ~settings,
       ~font_metrics,
       ~result_key,
       ~read_only=false,
diff --git a/src/haz3lweb/view/StepperView.re b/src/haz3lweb/view/StepperView.re
index c3ff3c528d..54bdf28e97 100644
--- a/src/haz3lweb/view/StepperView.re
+++ b/src/haz3lweb/view/StepperView.re
@@ -89,7 +89,7 @@ let settings_modal = (~inject, settings: CoreSettings.Evaluation.t) => {
 let stepper_view =
     (
       ~inject,
-      ~settings: CoreSettings.Evaluation.t,
+      ~settings,
       ~font_metrics,
       ~result_key,
       ~read_only: bool,
@@ -119,7 +119,8 @@ let stepper_view =
         ),
       ],
     );
-  let history = Stepper.get_history(~settings, stepper);
+  let history =
+    Stepper.get_history(~settings=settings.core.evaluation, stepper);
   switch (history) {
   | [] => []
   | [hd, ...tl] =>
@@ -127,7 +128,8 @@ let stepper_view =
       Widgets.button_d(
         Icons.undo,
         inject(UpdateAction.StepperAction(result_key, StepBackward)),
-        ~disabled=!Stepper.can_undo(~settings, stepper),
+        ~disabled=
+          !Stepper.can_undo(~settings=settings.core.evaluation, stepper),
         ~tooltip="Step Backwards",
       );
     let button_hide_stepper =
@@ -135,7 +137,11 @@ let stepper_view =
         inject(UpdateAction.ToggleStepper(result_key))
       );
     let toggle_show_history =
-      Widgets.toggle(~tooltip="Show History", "h", settings.stepper_history, _ =>
+      Widgets.toggle(
+        ~tooltip="Show History",
+        "h",
+        settings.core.evaluation.stepper_history,
+        _ =>
         inject(Set(Evaluation(ShowRecord)))
       );
     let eval_settings =
@@ -171,7 +177,7 @@ let stepper_view =
     let rec previous_step =
             (~hidden: bool, step: Stepper.step_info): list(Node.t) => {
       let hidden_steps =
-        settings.show_hidden_steps
+        settings.core.evaluation.show_hidden_steps
           ? Stepper.hidden_steps_of_info(step)
             |> List.rev_map(previous_step(~hidden=true))
             |> List.flatten
@@ -204,7 +210,7 @@ let stepper_view =
       |> List.rev_append(
            _,
            (
-             settings.show_hidden_steps
+             settings.core.evaluation.show_hidden_steps
                ? hd
                  |> Stepper.hidden_steps_of_info
                  |> List.map(previous_step(~hidden=true))
@@ -214,6 +220,9 @@ let stepper_view =
            @ [current],
          )
     )
-    @ (settings.show_settings ? settings_modal(~inject, settings) : []);
+    @ (
+      settings.core.evaluation.show_settings
+        ? settings_modal(~inject, settings.core.evaluation) : []
+    );
   };
 };
diff --git a/src/haz3lweb/view/dhcode/DHCode.re b/src/haz3lweb/view/dhcode/DHCode.re
index 820c7862a3..788b10fc39 100644
--- a/src/haz3lweb/view/dhcode/DHCode.re
+++ b/src/haz3lweb/view/dhcode/DHCode.re
@@ -129,7 +129,7 @@ let view_of_layout =
   );
 };
 
-let view =
+let _view =
     (
       ~locked as _=false, // NOTE: When we add mouse events to this, ignore them if locked
       ~inject,
@@ -167,3 +167,35 @@ let view =
 };
 
 type font_metrics = FontMetrics.t;
+
+let view =
+    (
+      ~locked as _=false, // NOTE: When we add mouse events to this, ignore them if locked
+      ~inject as _,
+      ~settings,
+      ~selected_hole_instance as _: option(Id.t),
+      ~font_metrics: FontMetrics.t,
+      ~width as _: int,
+      ~pos as _=0,
+      ~previous_step as _: option((EvaluatorStep.step, Id.t))=None, // The step that will be displayed above this one
+      ~hidden_steps as _: list((EvaluatorStep.step, Id.t))=[], // The hidden steps between the above and the current one
+      ~chosen_step as _: option(EvaluatorStep.step)=None, // The step that will be taken next
+      ~next_steps as _: list((int, Id.t))=[],
+      ~result_key: string,
+      ~infomap as _,
+      d: DHExp.t,
+    ) => {
+  let parenthesized = ExpToSegment.parenthesize(d);
+  let options = ExpToSegment.exp_to_pretty(~inline=false, parenthesized);
+  let option = List.hd(options);
+  let editor = Editor.init(~read_only=true, Zipper.unzip(option));
+  let code_text_view =
+    Code.view(~sort=Sort.root, ~font_metrics, ~settings, editor);
+  let code_view =
+    Node.div(
+      ~attr=
+        Attr.many([Attr.id(result_key), Attr.classes(["code-container"])]),
+      [code_text_view],
+    );
+  code_view;
+};
diff --git a/src/haz3lweb/view/dhcode/layout/DHDoc_Exp.re b/src/haz3lweb/view/dhcode/layout/DHDoc_Exp.re
index fa4242f8f8..0ed67e9a63 100644
--- a/src/haz3lweb/view/dhcode/layout/DHDoc_Exp.re
+++ b/src/haz3lweb/view/dhcode/layout/DHDoc_Exp.re
@@ -241,9 +241,9 @@ let mk =
       | Ap(Reverse, d1, d2) =>
         let (doc1, doc2) = (go'(d1), go'(d2));
         DHDoc_common.mk_rev_Ap(doc2, doc1);
-      | UnOp(Meta(Unquote), d) => DHDoc_common.mk_Ap(text("$"), go'(d))
-      | UnOp(Bool(Not), d) => DHDoc_common.mk_Ap(text("!"), go'(d))
-      | UnOp(Int(Minus), d) => DHDoc_common.mk_Ap(text("-"), go'(d))
+      | UnOp(Meta(Unquote), d) => Doc.hcats([text("$"), go'(d)])
+      | UnOp(Bool(Not), d) => Doc.hcats([text("!"), go'(d)])
+      | UnOp(Int(Minus), d) => Doc.hcats([text("-"), go'(d)])
       | BinOp(Int(op), d1, d2) =>
         // TODO assumes all bin int ops are left associative
         let (doc1, doc2) = mk_left_associative_operands(d1, d2);
diff --git a/src/util/ListUtil.re b/src/util/ListUtil.re
index b06a5a3980..1998599688 100644
--- a/src/util/ListUtil.re
+++ b/src/util/ListUtil.re
@@ -517,3 +517,33 @@ let rec unzip = (lst: list(('a, 'b))): (list('a), list('b)) => {
 
 let cross = (xs, ys) =>
   List.concat(List.map(x => List.map(y => (x, y), ys), xs));
+
+let rec intersperse = (sep, xs) =>
+  switch (xs) {
+  | [] => []
+  | [x] => [x]
+  | [x, ...xs] => [x, sep, ...intersperse(sep, xs)]
+  };
+
+let rec flat_intersperse = (sep, xss) =>
+  switch (xss) {
+  | [] => []
+  | [xs] => xs
+  | [xs, ...xss] => xs @ [sep, ...flat_intersperse(sep, xss)]
+  };
+
+let rec map_last_only = (f, xs) =>
+  switch (xs) {
+  | [] => []
+  | [x] => [f(x)]
+  | [x, ...xs] => [x, ...map_last_only(f, xs)]
+  };
+
+let rec split_last = (xs: list('x)): (list('x), 'x) =>
+  switch (xs) {
+  | [] => failwith("ListUtil.split_last")
+  | [x] => ([], x)
+  | [x, ...xs] =>
+    let (prefix, last) = split_last(xs);
+    ([x, ...prefix], last);
+  };