diff --git a/src/haz3lcore/Animation.re b/src/haz3lcore/Animation.re
new file mode 100644
index 0000000000..eddf2cad6b
--- /dev/null
+++ b/src/haz3lcore/Animation.re
@@ -0,0 +1,232 @@
+open Util;
+open Js_of_ocaml;
+
+/* This implements arbitrary gpu-accelerated css position
+ * and scale transition animations via the the FLIP technique
+ * (https://aerotwist.com/blog/flip-your-animations/).
+ *
+ * From the client perspective, it suffices to call the request
+ * method with a list of the DOM element ids to animate, as well
+ * as some animation settings (keyframes, duration, easing).
+ *
+ * Some common keyframes are provided in the module at the bottom */
+
+/* This is an extremely partial implementation of the Web Animations
+ * API, which currently does not have Js_of_ocaml wrappers */
+module Js = {
+  /* CSS property-value pairs */
+  type keyframe = (string, string);
+
+  type options = {
+    duration: int,
+    easing: string,
+  };
+
+  /* Options for CSS Animations API animate method */
+  type animation = {
+    options,
+    keyframes: list(keyframe),
+  };
+
+  /* Position & dimensions for a DOM element */
+  type box = {
+    top: float,
+    left: float,
+    height: float,
+    width: float,
+  };
+
+  let box_of = (elem: Js.t(Dom_html.element)): box => {
+    let container_rect = elem##getBoundingClientRect;
+    {
+      top: container_rect##.top,
+      left: container_rect##.left,
+      height: Js.Optdef.get(container_rect##.height, _ => (-1.0)),
+      width: Js.Optdef.get(container_rect##.width, _ => (-1.0)),
+    };
+  };
+
+  let client_height = (): float =>
+    Js.Optdef.get(
+      Js.Unsafe.get(Dom_html.document, "documentElement")##.clientHeight, _ =>
+      0.0
+    );
+
+  let inner_height = (): float =>
+    Js.Optdef.get(Js.Unsafe.get(Dom_html.window, "innerHeight"), _ => 0.0);
+
+  let check_visible = (client_height, inner_height, box: box): bool => {
+    let viewHeight = max(client_height, inner_height);
+    !(box.top +. box.height < 0.0 || box.top -. viewHeight >= 0.0);
+  };
+
+  let keyframes_unsafe = (keyframes: list(keyframe)): Js.t(Js.js_array('a)) =>
+    keyframes
+    |> List.map(((prop: string, value: string)) =>
+         Js.Unsafe.obj([|(prop, Js.Unsafe.inject(Js.string(value)))|])
+       )
+    |> Array.of_list
+    |> Js.array;
+
+  let options_unsafe = ({duration, easing}: options): Js.t(Js.js_array('a)) =>
+    [
+      ("duration", Js.Unsafe.inject(duration)),
+      ("easing", Js.Unsafe.inject(Js.string(easing))),
+    ]
+    |> Array.of_list
+    |> Js.Unsafe.obj;
+
+  let animate_unsafe =
+      (
+        keyframes: list(keyframe),
+        options: options,
+        elem: Js.t(Dom_html.element),
+      ) =>
+    Js.Unsafe.meth_call(
+      elem,
+      "animate",
+      [|
+        Js.Unsafe.inject(keyframes_unsafe(keyframes)),
+        Js.Unsafe.inject(options_unsafe(options)),
+      |],
+    );
+
+  let animate = ({options, keyframes}, elem: Js.t(Dom_html.element)) =>
+    if (keyframes != []) {
+      switch (animate_unsafe(keyframes, options, elem)) {
+      | exception exn =>
+        print_endline("Animation: " ++ Printexc.to_string(exn))
+      | () => ()
+      };
+    };
+};
+
+open Js;
+
+/* If an element is new, report its new metrics.
+ * Otherwise, report both new & old metrics */
+type change =
+  | New(box)
+  //| Removed(box)
+  | Existing(box, box);
+
+/* Specify a transition for an element */
+type transition = {
+  /* A unique id used as attribute for
+   * the relevant DOM element */
+  id: string,
+  /* The animation function recieves the diffs
+   * for the element's position and scale across a
+   * change, which it may use to calculate the
+   * parameters for a resulting animation */
+  animate: change => animation,
+};
+
+/* Internally, transitions must track the initial
+ * metrics for an element, gathered in the `Request ` phase */
+type transition_internal = {
+  id: string,
+  animate: change => animation,
+  box: option(box),
+};
+
+/* Elements and their corresponding animations are tracked
+ * here between when the action is used (`request`) and
+ * when the animation is executed (`go`) */
+let tracked_elems: ref(list(transition_internal)) = ref([]);
+
+let animate_elem = (({box, animate, _}, elem, new_box)): unit =>
+  switch (box, new_box) {
+  | (Some(init), Some(final)) =>
+    Js.animate(animate(Existing(init, final)), elem)
+  | (None, Some(final)) => Js.animate(animate(New(final)), elem)
+  | (Some(_init), None) =>
+    //TODO: Removed case (requires retaining old element somehow)
+    ()
+  | (None, None) => ()
+  };
+
+let filter_visible_elements = (tracked_elems: list(transition_internal)) => {
+  let client_height = client_height();
+  let inner_height = inner_height();
+  List.filter_map(
+    (tr: transition_internal) => {
+      switch (JsUtil.get_elem_by_id_opt(tr.id)) {
+      | None => None
+      | Some(elem) =>
+        let new_box = box_of(elem);
+        check_visible(client_height, inner_height, new_box)
+          ? Some((tr, elem, Some(new_box))) : None;
+      }
+    },
+    tracked_elems,
+  );
+};
+
+/* Execute animations. This is called during the
+ * render phase, after recalc but before repaint */
+let go = (): unit =>
+  if (tracked_elems^ != []) {
+    tracked_elems^ |> filter_visible_elements |> List.iter(animate_elem);
+    tracked_elems := [];
+  };
+
+/* Request animations. Call this during the MVU update */
+let request = (transitions: list(transition)): unit => {
+  tracked_elems :=
+    List.map(
+      ({id, animate}: transition) =>
+        {
+          id,
+          box: Option.map(box_of, JsUtil.get_elem_by_id_opt(id)),
+          animate,
+        },
+      transitions,
+    )
+    @ tracked_elems^;
+};
+
+module Keyframes = {
+  let transform_translate = (top: float, left: float): keyframe => (
+    "transform",
+    Printf.sprintf("translate(%fpx, %fpx)", left, top),
+  );
+
+  let translate = (init: box, final: box): list(keyframe) => {
+    [
+      transform_translate(init.top -. final.top, init.left -. final.left),
+      transform_translate(0., 0.),
+    ];
+  };
+
+  let transform_scale_uniform = (scale: float): keyframe => (
+    "transform",
+    Printf.sprintf("scale(%f, %f)", scale, scale),
+  );
+
+  let scale_from_zero: list(keyframe) = [
+    transform_scale_uniform(0.0),
+    transform_scale_uniform(1.0),
+  ];
+};
+
+let easeOutExpo = "cubic-bezier(0.16, 1, 0.3, 1)";
+let easeInOutBack = "cubic-bezier(0.68, -0.6, 0.32, 1.6)";
+let easeInOutExpo = "cubic-bezier(0.87, 0, 0.13, 1)";
+
+module Actions = {
+  let move = id => {
+    id,
+    animate: change => {
+      options: {
+        duration: 125,
+        easing: easeOutExpo,
+      },
+      keyframes:
+        switch (change) {
+        | New(_) => Keyframes.scale_from_zero
+        | Existing(init, final) => Keyframes.translate(init, final)
+        },
+    },
+  };
+};
diff --git a/src/haz3lcore/Measured.re b/src/haz3lcore/Measured.re
index a3052cd961..64707c82fe 100644
--- a/src/haz3lcore/Measured.re
+++ b/src/haz3lcore/Measured.re
@@ -266,15 +266,18 @@ let is_indented_map = (seg: Segment.t) => {
   go(seg);
 };
 
-let last_of_token = (token: string, origin: Point.t): Point.t =>
-  /* Supports multi-line tokens e.g. projector placeholders */
-  Point.{
-    col: origin.col + StringUtil.max_line_width(token),
-    row: origin.row + StringUtil.num_linebreaks(token),
-  };
+/* Tab projectors add linebreaks after the end of their line */
+let deferred_linebreaks: ref(list(int)) = ref([]);
+
+let consume_deferred_linebreaks = () => {
+  let max_deferred_linebreaks = List.fold_left(max, 0, deferred_linebreaks^);
+  deferred_linebreaks := [];
+  max_deferred_linebreaks;
+};
 
 let of_segment =
     (seg: Segment.t, shape_of_proj: Base.projector => ProjectorCore.shape): t => {
+  deferred_linebreaks := [];
   let is_indented = is_indented_map(seg);
 
   // recursive across seg's bidelimited containers
@@ -308,11 +311,6 @@ let of_segment =
              );
         (origin, map);
       | [hd, ...tl] =>
-        let extra_rows = (token, origin, map) => {
-          let row_indent = container_indent + contained_indent;
-          let num_extra_rows = StringUtil.num_linebreaks(token);
-          add_n_rows(origin, row_indent, num_extra_rows, map);
-        };
         let (contained_indent, origin, map) =
           switch (hd) {
           | Secondary(w) when Secondary.is_linebreak(w) =>
@@ -323,16 +321,16 @@ let of_segment =
               } else {
                 contained_indent + (Id.Map.find(w.id, is_indented) ? 2 : 0);
               };
+            let num_extra_rows = 1 + consume_deferred_linebreaks();
             let last =
-              Point.{row: origin.row + 1, col: container_indent + indent};
+              Point.{
+                row: origin.row + num_extra_rows,
+                col: container_indent + indent,
+              };
             let map =
               map
               |> add_w(w, {origin, last})
-              |> add_row(
-                   origin.row,
-                   {indent: row_indent, max_col: origin.col},
-                 )
-              |> add_n_rows(origin, row_indent, 1);
+              |> add_n_rows(origin, row_indent, num_extra_rows);
             (indent, last, map);
           | Secondary(w) =>
             let wspace_length =
@@ -349,14 +347,20 @@ let of_segment =
             let shape = shape_of_proj(p);
             let num_extra_rows =
               switch (shape.vertical) {
-              | Inline => 0
-              | Block(num_lbs) => num_lbs
+              | Inline
+              | Tab(0)
+              | Block(0) => 0
+              | Tab(num_lb) =>
+                deferred_linebreaks := [num_lb, ...deferred_linebreaks^];
+                num_lb;
+              | Block(num_lb) => num_lb + consume_deferred_linebreaks()
               };
             let last = {
               col: origin.col + shape.horizontal,
               row:
                 switch (shape.vertical) {
                 | Inline => origin.row
+                | Tab(_) => origin.row
                 | Block(num_lb) => origin.row + num_lb
                 },
             };
@@ -366,6 +370,18 @@ let of_segment =
               |> add_pr(p, {origin, last});
             (contained_indent, last, map);
           | Tile(t) =>
+            let extra_rows = (token, origin, map) => {
+              let row_indent = container_indent + contained_indent;
+              let num_lb = StringUtil.num_linebreaks(token);
+              let num_extra_rows =
+                StringUtil.num_linebreaks(token) + num_lb == 0
+                  ? 0 : consume_deferred_linebreaks();
+              add_n_rows(origin, row_indent, num_extra_rows, map);
+            };
+            let last_of_token = (token: string, origin: Point.t): Point.t => {
+              col: origin.col + StringUtil.max_line_width(token),
+              row: origin.row + StringUtil.num_linebreaks(token),
+            };
             let add_shard = (origin, shard, map) => {
               let token = List.nth(t.label, shard);
               let map = extra_rows(token, origin, map);
diff --git a/src/haz3lcore/projectors/ProjectorCore.re b/src/haz3lcore/projectors/ProjectorCore.re
index 847d8da568..7dd5f75448 100644
--- a/src/haz3lcore/projectors/ProjectorCore.re
+++ b/src/haz3lcore/projectors/ProjectorCore.re
@@ -23,6 +23,7 @@ type kind =
   | Checkbox
   | Slider
   | SliderF
+  | Card
   | TextArea;
 
 /* A projector shape determines the space left for
@@ -30,10 +31,16 @@ type kind =
  * in a text editor. All projectors have a horizontal
  * extend (in characters), and the vertical extent may
  * be either 1 character (Inline), or it may insert
- * an additional number of linebreaks */
+ * an additional number of linebreaks, either immediately
+ * after the projector (Block style) or defer them to
+ * the next linebreak (Tab style). In the latter case,
+ * if there are multiple Tab projectors on a line, the
+ * total extra linebreaks inserted is the maxium required
+ * to accomodate them */
 [@deriving (show({with_path: false}), sexp, yojson)]
 type vertical =
   | Inline
+  | Tab(int)
   | Block(int);
 
 [@deriving (show({with_path: false}), sexp, yojson)]
@@ -51,7 +58,13 @@ type t('syntax) = {
   model: string,
 };
 
-let livelit_projectors: list(kind) = [Checkbox, Slider, SliderF, TextArea];
+let livelit_projectors: list(kind) = [
+  Card,
+  Checkbox,
+  Slider,
+  SliderF,
+  TextArea,
+];
 
 let projectors: list(kind) = livelit_projectors @ [Fold, Info, Probe];
 
@@ -60,7 +73,8 @@ let default: shape = inline(0);
 
 let token = (shape: shape): string =>
   switch (shape.vertical) {
-  | Inline => String.make(shape.horizontal, ' ')
+  | Inline
+  | Tab(_) => String.make(shape.horizontal, ' ')
   | Block(num_lb) =>
     String.make(num_lb, '\n') ++ String.make(shape.horizontal, ' ')
   };
diff --git a/src/haz3lcore/projectors/ProjectorInit.re b/src/haz3lcore/projectors/ProjectorInit.re
index 17570dabd2..bdfdb8be13 100644
--- a/src/haz3lcore/projectors/ProjectorInit.re
+++ b/src/haz3lcore/projectors/ProjectorInit.re
@@ -13,6 +13,7 @@ let to_module = (kind: ProjectorCore.kind): (module Cooked) =>
   | SliderF => (module Cook(SliderFProj.M))
   | Checkbox => (module Cook(CheckboxProj.M))
   | TextArea => (module Cook(TextAreaProj.M))
+  | Card => (module Cook(CardProj.M))
   };
 
 let init =
diff --git a/src/haz3lcore/projectors/implementations/CardProj.re b/src/haz3lcore/projectors/implementations/CardProj.re
new file mode 100644
index 0000000000..a050f389f3
--- /dev/null
+++ b/src/haz3lcore/projectors/implementations/CardProj.re
@@ -0,0 +1,841 @@
+open Util;
+open Virtual_dom.Vdom;
+open ProjectorBase;
+
+[@deriving (show({with_path: false}), sexp, yojson)]
+type mode =
+  | Show
+  | Choose
+  | Flipped;
+
+[@deriving (show({with_path: false}), sexp, yojson)]
+type model = {mode};
+[@deriving (show({with_path: false}), sexp, yojson)]
+type action =
+  | SetMode(mode);
+
+let model_of_sexp = (sexp: Sexplib.Sexp.t): model =>
+  switch (model_of_sexp(sexp)) {
+  | exception _ => {mode: Show}
+  | m => m
+  };
+
+[@deriving (show({with_path: false}), sexp, yojson)]
+type suit =
+  | Unknown(string)
+  | Hearts
+  | Diamonds
+  | Clubs
+  | Spades;
+
+[@deriving (show({with_path: false}), sexp, yojson)]
+type rank =
+  | Unknown(string)
+  | Ace
+  | Two
+  | Three
+  | Four
+  | Five
+  | Six
+  | Seven
+  | Eight
+  | Nine
+  | Ten
+  | Jack
+  | Queen
+  | King;
+
+[@deriving (show({with_path: false}), sexp, yojson)]
+type card = (suit, rank);
+
+[@deriving (show({with_path: false}), sexp, yojson)]
+type hand = list(card);
+
+[@deriving (show({with_path: false}), sexp, yojson)]
+type collection =
+  | Card(card)
+  | Hand(hand);
+
+[@deriving (show({with_path: false}), sexp, yojson)]
+type sort =
+  | Exp
+  | Pat;
+
+[@deriving (show({with_path: false}), sexp, yojson)]
+type syntax = (sort, collection);
+
+let sort_of = (sort: Sort.t): sort =>
+  switch (sort) {
+  | Sort.Exp => Exp
+  | Sort.Pat => Pat
+  | _ =>
+    print_endline("WARNING:Card: Invalid sort: " ++ Sort.show(sort));
+    Exp;
+  };
+
+let to_sort = (sort: sort): Sort.t =>
+  switch (sort) {
+  | Exp => Sort.Exp
+  | Pat => Sort.Pat
+  };
+
+module SyntaxTerm = {
+  module Exp = {
+    let get_wrap = (term: Term.Exp.t): option(Term.Exp.t) =>
+      switch (term) {
+      | {term: Wrap(term, _), _} => Some(term)
+      | _ => None
+      };
+
+    let get_tuple = (term: Term.Exp.t): option(list(Term.Exp.t)) =>
+      switch (term) {
+      | {term: Tuple(terms), _} => Some(terms)
+      | _ => None
+      };
+
+    let get_two_tuple = (term: Term.Exp.t): option((Term.Exp.t, Term.Exp.t)) =>
+      switch (get_tuple(term)) {
+      | Some([term1, term2]) => Some((term1, term2))
+      | _ => None
+      };
+
+    let get_constructor = (term: Term.Exp.t): option(string) =>
+      switch (term) {
+      | {term: Constructor(str, _), _} => Some(str)
+      | _ => None
+      };
+
+    let get_listlit = (term: Term.Exp.t): option(list(Term.Exp.t)) =>
+      switch (term) {
+      | {term: ListLit(terms), _} => Some(terms)
+      | _ => None
+      };
+
+    let mk_constructor = (str: string): Term.Exp.t =>
+      IdTagged.fresh(
+        Constructor(str, Unknown(Internal) |> Typ.temp): Term.Exp.term,
+      );
+
+    let mk_tuple = (children: list(Term.Exp.t)): Term.Exp.t =>
+      IdTagged.fresh(Tuple(children): Term.Exp.term);
+
+    let mk_listlit = (children: list(Term.Exp.t)): Term.Exp.t =>
+      IdTagged.fresh(ListLit(children): Term.Exp.term);
+
+    let mk_wrap = (term: Term.Exp.t): Term.Exp.t =>
+      IdTagged.fresh(Wrap(term, Paren): Term.Exp.term);
+  };
+
+  module Pat = {
+    let get_wrap = (term: Term.Pat.t): option(Term.Pat.t) =>
+      switch (term) {
+      | {term: Wrap(term, _), _} => Some(term)
+      | _ => None
+      };
+
+    let get_tuple = (term: Term.Pat.t): option(list(Term.Pat.t)) =>
+      switch (term) {
+      | {term: Tuple(terms), _} => Some(terms)
+      | _ => None
+      };
+
+    let get_two_tuple = (term: Term.Pat.t): option((Term.Pat.t, Term.Pat.t)) =>
+      switch (get_tuple(term)) {
+      | Some([term1, term2]) => Some((term1, term2))
+      | _ => None
+      };
+
+    let get_constructor = (term: Term.Pat.t): option(string) => {
+      switch (term) {
+      | {term: Constructor(str, _), _} => Some(str)
+      | {term: Var(str), _} => Some(str)
+      | {term: Wild, _} => Some("_")
+      | _ => None
+      };
+    };
+
+    let get_listlit = (term: Term.Pat.t): option(list(Term.Pat.t)) =>
+      switch (term) {
+      | {term: ListLit(terms), _} => Some(terms)
+      | _ => None
+      };
+
+    let mk_constructor = (str: string): Term.Pat.t =>
+      IdTagged.fresh(
+        Constructor(str, Unknown(Internal) |> Typ.temp): Term.Pat.term,
+      );
+
+    let mk_tuple = (children: list(Term.Pat.t)): Term.Pat.t =>
+      IdTagged.fresh(Tuple(children): Term.Pat.term);
+
+    let mk_listlit = (children: list(Term.Pat.t)): Term.Pat.t =>
+      IdTagged.fresh(ListLit(children): Term.Pat.term);
+
+    let mk_wrap = (term: Term.Pat.t): Term.Pat.t =>
+      IdTagged.fresh(Wrap(term, Paren): Term.Pat.term);
+  };
+
+  let suit_of_exp = (suit): option(suit) =>
+    switch (suit |> Sexplib.Sexp.of_string |> suit_of_sexp) {
+    | exception _ => None
+    | s => Some(s)
+    };
+  let rank_of_exp = (rank): option(rank) =>
+    switch (rank |> Sexplib.Sexp.of_string |> rank_of_sexp) {
+    | exception _ => None
+    | r => Some(r)
+    };
+  let suit_of_pat = (suit): option(suit) =>
+    switch (suit |> Sexplib.Sexp.of_string |> suit_of_sexp) {
+    | exception _ => Some(Unknown(suit))
+    | s => Some(s)
+    };
+  let rank_of_pat = (rank): option(rank) =>
+    switch (rank |> Sexplib.Sexp.of_string |> rank_of_sexp) {
+    | exception _ => Some(Unknown(rank))
+    | r => Some(r)
+    };
+
+  let exp_to_card = (term: Term.Exp.t): option(card) => {
+    open OptUtil.Syntax;
+    let* tuple = Exp.get_wrap(term);
+    let* (t1, t2) = Exp.get_two_tuple(tuple);
+    let* c1 = Exp.get_constructor(t1);
+    let* c2 = Exp.get_constructor(t2);
+    let* suit = suit_of_exp(c1);
+    let* rank = rank_of_exp(c2);
+    Some((suit, rank));
+  };
+
+  let pat_to_card = (term: Term.Pat.t): option(card) => {
+    open OptUtil.Syntax;
+    let* tuple = Pat.get_wrap(term);
+    let* (t1, t2) = Pat.get_two_tuple(tuple);
+    let* c1 = Pat.get_constructor(t1);
+    let* c2 = Pat.get_constructor(t2);
+    let* suit = suit_of_pat(c1);
+    let* rank = rank_of_pat(c2);
+    Some((suit, rank));
+  };
+
+  let any_to_syntax = (any: Any.t): option(syntax) => {
+    OptUtil.Syntax.(
+      switch (any) {
+      | Exp(term) =>
+        let term = Term.Exp.strip_wraps(term);
+        switch (exp_to_card(term)) {
+        | Some(card) => Some((Exp, Card(card)))
+        | None =>
+          let+ listlit = Exp.get_listlit(term);
+          let cards = List.filter_map(exp_to_card, listlit);
+          (Exp, Hand(cards));
+        };
+      | Pat(term) =>
+        let term = Term.Pat.strip_wraps(term);
+        switch (pat_to_card(term)) {
+        | Some(card) => Some((Exp, Card(card)))
+        | None =>
+          let+ listlit = Pat.get_listlit(term);
+          let cards = List.filter_map(pat_to_card, listlit);
+          (Exp, Hand(cards));
+        };
+      | _ => None
+      }
+    );
+  };
+
+  let suit_to_exp = (suit: suit): Term.Exp.t =>
+    Exp.mk_constructor(suit |> sexp_of_suit |> Sexplib.Sexp.to_string);
+
+  let rank_to_exp = (rank: rank): Term.Exp.t =>
+    Exp.mk_constructor(rank |> sexp_of_rank |> Sexplib.Sexp.to_string);
+
+  let card_to_exp = ((suit, rank): card): Term.Exp.t =>
+    Exp.mk_tuple([suit_to_exp(suit), rank_to_exp(rank)]);
+
+  let hand_to_exp = (hand: hand): Term.Exp.t =>
+    Exp.mk_listlit(List.map(card_to_exp, hand));
+
+  let suit_to_pat = (suit: suit): Term.Pat.t =>
+    Pat.mk_constructor(suit |> sexp_of_suit |> Sexplib.Sexp.to_string);
+
+  let rank_to_pat = (rank: rank): Term.Pat.t =>
+    Pat.mk_constructor(rank |> sexp_of_rank |> Sexplib.Sexp.to_string);
+
+  let card_to_pat = ((suit, rank): card): Term.Pat.t =>
+    Pat.mk_tuple([suit_to_pat(suit), rank_to_pat(rank)]);
+
+  let hand_to_pat = (hand: hand): Term.Pat.t =>
+    Pat.mk_listlit(List.map(card_to_pat, hand));
+
+  let syntax_to_any = (syntax: syntax): Term.Any.t =>
+    switch (syntax) {
+    | (Exp, Card(card)) => Exp(card_to_exp(card))
+    | (Exp, Hand(hand)) => Exp(hand_to_exp(hand))
+    | (Pat, Card(card)) => Pat(card_to_pat(card))
+    | (Pat, Hand(hand)) => Pat(hand_to_pat(hand))
+    };
+
+  let put = (info, syntax): Piece.t =>
+    info.utility.lift_syntax(_ => syntax_to_any(syntax), info.syntax);
+
+  let get_opt = (any: Any.t): option(syntax) =>
+    switch (any |> any_to_syntax) {
+    | Some(syntax) => Some(syntax)
+    | None => None
+    };
+
+  let get = (info: info): syntax =>
+    switch ([info.syntax] |> info.utility.seg_to_term |> get_opt) {
+    | Some(syntax) => syntax
+    | None => failwith("Cards: Get: not cards")
+    };
+
+  let width_of_syntax = (syntax: syntax): int =>
+    switch (syntax) {
+    | (_, Card(_)) => 1
+    | (_, Hand(hand)) => List.length(hand)
+    };
+
+  let width_of_any = (info: info): int =>
+    switch (any_to_syntax([info.syntax] |> info.utility.seg_to_term)) {
+    | None => 0
+    | Some((_, Card(_)))
+    | Some((_, Hand([_]))) => 4
+    | Some((_, Hand(hand))) =>
+      //TODO: Better formula / card dimensions / offset
+      4 + List.length(hand) - (List.length(hand) + 66) / 24
+    };
+};
+
+// module Syntax = {
+//   let suit_of_piece = (p: Piece.t): suit =>
+//     switch (p) {
+//     | Tile({label: [str], _}) =>
+//       switch (str |> Sexplib.Sexp.of_string |> suit_of_sexp) {
+//       | exception _ => Unknown(p)
+//       | s => s
+//       }
+//     | _ => Unknown(p)
+//     };
+
+//   let rank_of_piece = (p: Piece.t): rank =>
+//     switch (p) {
+//     | Tile({label: [str], _}) =>
+//       switch (str |> Sexplib.Sexp.of_string |> rank_of_sexp) {
+//       | exception _ => Unknown(p)
+//       | r => r
+//       }
+//     | _ => Unknown(p)
+//     };
+
+//   let rm_secondary = (segment: Segment.t): Segment.t =>
+//     List.filter(p => !Piece.is_secondary(p), segment);
+
+//   let piece_to_card =
+//     Core.Memo.general(~cache_size_bound=1000, (piece: Piece.t) =>
+//       (
+//         switch (piece) {
+//         | Tile({
+//             label: ["(", ")"],
+//             children:
+//               [[Tile({label: ["(", ")"], children: [segment], _})]],
+//             _,
+//           })
+//         //TODO: better unwrapping
+//         | Tile({label: ["(", ")"], children: [segment], _}) =>
+//           switch (rm_secondary(segment)) {
+//           | [left_child, Tile({label: [","], _}), right_child] =>
+//             Some((suit_of_piece(left_child), rank_of_piece(right_child)))
+//           | _ => None
+//           }
+//         | _ => None
+//         }:
+//           option(card)
+//       )
+//     );
+
+//   let piece_to_hand = (piece: Piece.t): option(hand) => {
+//     switch (piece) {
+//     | Tile({
+//         label: ["(", ")"],
+//         children: [[Tile({label: ["[", "]"], children: [segment], _})]],
+//         _,
+//       })
+//     | Tile({label: ["[", "]"], children: [segment], _}) =>
+//       segment |> rm_secondary |> List.filter_map(piece_to_card) |> Option.some
+//     | _ => None
+//     };
+//   };
+
+//   let piece_to_syntax = (piece: Piece.t): option(syntax) => {
+//     let sort = piece |> Piece.sort |> fst |> sort_of;
+//     switch (piece_to_hand(piece)) {
+//     | Some(hand) => Some((sort, Hand(hand)))
+//     | None =>
+//       open OptUtil.Syntax;
+//       let+ card = piece_to_card(piece);
+//       (sort, Card(card));
+//     };
+//   };
+
+//   let mk_tuple = (sort: Sort.t, children): Piece.t =>
+//     Tile({
+//       id: Id.mk(),
+//       label: ["(", ")"],
+//       mold: Mold.mk_op(sort, [sort]),
+//       shards: [0, 1],
+//       children: [children],
+//     });
+
+//   let mk_text = (str): Piece.t =>
+//     Tile({
+//       id: Id.mk(),
+//       label: [str],
+//       mold: Mold.mk_op(Sort.Exp, []),
+//       shards: [0],
+//       children: [],
+//     });
+
+//   let piece_of_suit = (suit: suit): Piece.t =>
+//     switch (suit) {
+//     | Unknown(p) => p
+//     | _ => suit |> sexp_of_suit |> Sexplib.Sexp.to_string |> mk_text
+//     };
+
+//   let piece_of_rank = (rank: rank) =>
+//     switch (rank) {
+//     | Unknown(p) => p
+//     | _ => rank |> sexp_of_rank |> Sexplib.Sexp.to_string |> mk_text
+//     };
+
+//   let card_to_piece_exp = ((suit, rank): card): Piece.t =>
+//     [
+//       piece_of_suit(suit),
+//       Piece.mk_tile(Form.get("comma_exp"), []),
+//       piece_of_rank(rank),
+//     ]
+//     |> mk_tuple(Sort.Exp)
+//     |> (x => [x])
+//     |> mk_tuple(Sort.Exp);
+
+//   let card_to_piece_pat = ((suit, rank): card): Piece.t =>
+//     [
+//       piece_of_suit(suit),
+//       Piece.mk_tile(Form.get("comma_pat"), []),
+//       piece_of_rank(rank),
+//     ]
+//     |> mk_tuple(Sort.Pat)
+//     |> (x => [x])
+//     |> mk_tuple(Sort.Pat);
+
+//   let hand_to_piece_exp = (hand: hand): Piece.t =>
+//     mk_tuple(Sort.Exp, List.map(card_to_piece_exp, hand));
+
+//   let hand_to_piece_pat = (hand: hand): Piece.t =>
+//     mk_tuple(Sort.Pat, List.map(card_to_piece_pat, hand));
+
+//   let syntax_to_piece = (syntax: syntax): Piece.t =>
+//     switch (syntax) {
+//     | (Exp, Card(card)) => card_to_piece_exp(card)
+//     | (Pat, Card(card)) => card_to_piece_pat(card)
+//     | (Exp, Hand(hand)) => hand_to_piece_exp(hand)
+//     | (Pat, Hand(hand)) => hand_to_piece_pat(hand)
+//     };
+
+//   let put = syntax_to_piece;
+
+//   let get_opt = piece_to_syntax;
+
+//   let get = (piece: Piece.t): syntax =>
+//     switch (get_opt(piece)) {
+//     | None => failwith("ERROR: Card: Not card or hand")
+//     | Some(syntax) => syntax
+//     };
+
+//   let width_of_syntax = (syntax: syntax): int =>
+//     switch (syntax) {
+//     | (_, Card(_)) => 1
+//     | (_, Hand(hand)) => List.length(hand)
+//     };
+
+//   let width_of_piece = (piece: Piece.t): int =>
+//     switch (piece_to_syntax(piece)) {
+//     | None => 0
+//     | Some((_, Card(_)))
+//     | Some((_, Hand([_]))) => 4
+//     | Some((_, Hand(hand))) =>
+//       //TODO: Better formula / card dimensions / offset
+//       4 + List.length(hand) - (List.length(hand) + 66) / 24
+//     };
+// };
+
+let suit_to_int = (suit: suit): int =>
+  switch (suit) {
+  | Hearts => 0
+  | Clubs => 1
+  | Diamonds => 2
+  | Spades => 3
+  | Unknown(_) => 4
+  };
+
+let rank_to_int = (rank: rank): int =>
+  switch (rank) {
+  | Two => 1
+  | Three => 2
+  | Four => 3
+  | Five => 4
+  | Six => 5
+  | Seven => 6
+  | Eight => 7
+  | Nine => 8
+  | Ten => 9
+  | Jack => 10
+  | Queen => 11
+  | King => 12
+  | Ace => 13
+  | Unknown(_) => 14
+  };
+
+module Card = {
+  /* Card images are stored in a spritesheet. The sheet image
+   * has four rows (hearts, clubs, diamonds, spades) and 14
+   * columns (first is misc, then 2-10, then J Q K A) */
+
+  let width = 35; /* Width of each card in pixels */
+  let height = 47; /* Height of each card in pixels */
+
+  let card_to_offset = (_sort: Sort.t, (suit, rank): card): (int, int) => (
+    rank_to_int(rank) * width,
+    suit_to_int(suit) * height,
+  );
+
+  let background_offset = (~flipped, sort: Sort.t, card: card): Css_gen.t => {
+    let (offset_x, offset_y) =
+      flipped
+        ? switch (sort_of(sort)) {
+          | Exp => (0, 0)
+          | Pat => (0, height)
+          }
+        : card_to_offset(sort, card);
+    Css_gen.create(
+      ~field="background-position",
+      ~value=Printf.sprintf("%dpx %dpx", - offset_x, - offset_y),
+    );
+  };
+
+  let view = (sort: Sort.t, card: card): Node.t =>
+    Node.div(
+      ~attrs=[Attr.classes(["card-scene", Sort.show(sort)])],
+      [
+        Node.div(
+          ~attrs=[
+            Attr.classes(["card-sprite", "front", Sort.show(sort)]),
+            Attr.style(background_offset(~flipped=false, sort, card)),
+          ],
+          [],
+        ),
+        Node.div(
+          ~attrs=[
+            Attr.classes(["card-sprite", "back", Sort.show(sort)]),
+            Attr.style(background_offset(~flipped=true, sort, card)),
+          ],
+          [],
+        ),
+      ],
+    );
+};
+
+module Chooser = {
+  let col_width = 8;
+  let row_height = 14;
+
+  let grid = (sort: sort): list(list(card)) => {
+    let maybe_rank =
+      switch (sort) {
+      | Exp => []
+      | Pat => [Unknown("_")] //TODO
+      };
+    let maybe_suit: list(suit) =
+      switch (sort) {
+      | Exp => []
+      | Pat => [Unknown("_")] //TODO
+      };
+    let suits: list(suit) = [Hearts, Spades, Diamonds, Clubs] @ maybe_suit;
+    let ranks: list(rank) =
+      [
+        Two,
+        Three,
+        Four,
+        Five,
+        Six,
+        Seven,
+        Eight,
+        Nine,
+        Ten,
+        Jack,
+        Queen,
+        King,
+        Ace,
+      ]
+      @ maybe_rank;
+    List.map(
+      (suit: suit) => List.map((rank: rank) => (suit, rank), ranks),
+      suits,
+    );
+  };
+
+  let card_wrapper =
+      (info, ~indicated, parent, sort: Sort.t, col: int, row: int, card: card)
+      : Node.t =>
+    Node.div(
+      ~attrs=[
+        Attr.classes(["card-wrapper"] @ (indicated ? ["indicated"] : [])),
+        Attr.on_mousedown(_ => {
+          print_endline("setting syntax");
+          //TODO: make this work for hands
+          Effect.Many([
+            parent(
+              SetSyntax(
+                SyntaxTerm.put(info, (sort_of(sort), Card(card))),
+              ),
+            ),
+            // Effect.Prevent_default,
+            // Effect.Stop_propagation,
+          ]);
+        }),
+        Attr.create(
+          "style",
+          Printf.sprintf(
+            "position: absolute; left: %dpx; top: %dpx; z-index: %d;",
+            col * col_width,
+            row * row_height,
+            100 + row + col,
+          ),
+        ),
+      ],
+      [Card.view(sort, card)],
+    );
+
+  let view = (info, parent, sort: Sort.t, card: card): Node.t =>
+    Node.div(
+      ~attrs=[Attr.classes(["chooser", Sort.show(sort)])],
+      List.mapi(
+        (r, row) =>
+          List.mapi(
+            (col, c) =>
+              card_wrapper(
+                info,
+                parent,
+                ~indicated=c == card,
+                sort,
+                col,
+                r,
+                c,
+              ),
+            row,
+          ),
+        grid(sort_of(sort)),
+      )
+      |> List.concat,
+    );
+};
+
+module Singleton = {
+  let view =
+      (
+        info,
+        mode,
+        parent,
+        local: action => Ui_effect.t(unit),
+        sort: Sort.t,
+        card: card,
+      )
+      : Node.t => {
+    let on_mousedown = evt =>
+      switch (JsUtil.is_double_click(evt)) {
+      | _ when JsUtil.shift_held(evt) =>
+        switch (mode) {
+        | Choose
+        | Flipped => local(SetMode(Show))
+        | Show => local(SetMode(Choose))
+        }
+      | _ =>
+        switch (mode) {
+        | Flipped
+        | Choose => local(SetMode(Show))
+        | _ => local(SetMode(Flipped))
+        }
+      };
+
+    Node.div(
+      ~attrs=[
+        Attr.classes(
+          ["card-wrapper"]
+          @ (
+            switch (mode) {
+            | Show => ["show"]
+            | Flipped => ["flipped"]
+            | Choose => ["choose"]
+            }
+          ),
+        ),
+        Attr.on_mousedown(on_mousedown),
+      ],
+      [
+        switch (mode) {
+        | Show => Card.view(sort, card)
+        | Choose => Chooser.view(info, parent, sort, card)
+        | Flipped => Card.view(sort, card)
+        },
+      ],
+    );
+  };
+};
+
+module CardInHand = {
+  let view =
+      (
+        info,
+        _elem_ids,
+        mode,
+        parent,
+        local: action => Ui_effect.t(unit),
+        sort: Sort.t,
+        card: card,
+      )
+      : Node.t => {
+    let on_mousedown = evt =>
+      switch (JsUtil.is_double_click(evt)) {
+      | _ when JsUtil.shift_held(evt) =>
+        switch (mode) {
+        | Choose
+        | Flipped => local(SetMode(Show))
+        | Show => local(SetMode(Choose))
+        }
+      | _ => Effect.Ignore
+      };
+
+    Node.div(
+      ~attrs=[
+        Attr.classes(
+          ["card-wrapper"]
+          @ (
+            switch (mode) {
+            | Show => ["show"]
+            | Flipped => ["flipped"]
+            | Choose => ["choose"]
+            }
+          ),
+        ),
+        Attr.on_mousedown(on_mousedown),
+      ],
+      [
+        switch (mode) {
+        | Show => Card.view(sort, card)
+        | Choose => Chooser.view(info, parent, sort, card)
+        | Flipped => Card.view(sort, card)
+        },
+      ],
+    );
+  };
+};
+
+let hand_elem_ids = (id, hand: hand): list(string) =>
+  List.mapi(
+    (i, _) => Id.cls(id) ++ "card-index-" ++ string_of_int(i),
+    hand,
+  );
+
+module Hand = {
+  // a card, but each subsequent card should be absoluted positioned 20px to the right of the last and higher in z-index:
+  let card_wrapper =
+      (
+        info,
+        id,
+        elem_ids,
+        mode,
+        parent: external_action => Ui_effect.t(unit),
+        local: action => Ui_effect.t(unit),
+        sort: Sort.t,
+        index: int,
+        card: card,
+      )
+      : Node.t =>
+    Node.div(
+      ~attrs=[
+        Attr.id(Id.cls(id) ++ "card-index-" ++ string_of_int(index)),
+        Attr.class_("card-wrapper"),
+        Attr.create(
+          "style",
+          Printf.sprintf(
+            "position: absolute; left: %dpx; z-index: %d;",
+            mode == Flipped ? 0 : index * 8,
+            100 + index,
+          ),
+        ),
+      ],
+      [CardInHand.view(info, elem_ids, mode, parent, local, sort, card)],
+    );
+
+  let view = (info, mode, parent, local, sort: Sort.t, hand: hand): Node.t => {
+    Node.div(
+      ~attrs=[Attr.classes(["hand", Sort.show(sort)])],
+      List.mapi(
+        card_wrapper(
+          info,
+          info.id,
+          hand_elem_ids(info.id, hand),
+          mode,
+          parent,
+          local,
+          sort,
+        ),
+        hand,
+      ),
+    );
+  };
+};
+
+[@deriving (show({with_path: false}), sexp, yojson)]
+type m = model;
+[@deriving (show({with_path: false}), sexp, yojson)]
+type a = action;
+
+module M: Projector = {
+  [@deriving (show({with_path: false}), sexp, yojson)]
+  type model = m;
+  [@deriving (show({with_path: false}), sexp, yojson)]
+  type action = a;
+  let init: model = {mode: Show};
+  let can_project = (_, info) => SyntaxTerm.get_opt(info) != None;
+  let can_focus = false;
+  let dynamics = false;
+  let placeholder = (_, info): ProjectorCore.shape => {
+    horizontal: SyntaxTerm.width_of_any(info),
+    vertical: Tab(1),
+  };
+  let update = (_model, _, action) =>
+    switch (action) {
+    | SetMode(mode) => {mode: mode}
+    };
+  let view =
+      (
+        model,
+        info,
+        ~local,
+        ~parent: external_action => Ui_effect.t(unit),
+        ~view_seg as _,
+      ) => {
+    switch (SyntaxTerm.get(info)) {
+    | (sort, Card(card)) =>
+      Singleton.view(info, model.mode, parent, local, to_sort(sort), card)
+    | (sort, Hand(hand)) =>
+      Hand.view(info, model.mode, parent, local, to_sort(sort), hand)
+    };
+  };
+  let offside_view = None;
+  let overlay_view = None;
+  let underlay_view = None;
+  let focus = _ => ();
+};
diff --git a/src/haz3lcore/statics/Term.re b/src/haz3lcore/statics/Term.re
index 7c4513b99c..c5b4cad9b4 100644
--- a/src/haz3lcore/statics/Term.re
+++ b/src/haz3lcore/statics/Term.re
@@ -303,6 +303,17 @@ module Pat = {
          | None => {id: Id.invalid, name}
          }
        );
+
+  let rec strip_wraps = (p: t): t => {
+    switch (p.term) {
+    | Wrap(inner, _) =>
+      switch (inner.term) {
+      | Tuple(_) => p
+      | _ => strip_wraps(inner)
+      }
+    | _ => p
+    };
+  };
 };
 
 module Exp = {
@@ -778,6 +789,19 @@ module Exp = {
     | _ => None
     };
   };
+
+  /* Strips outer parentheses, unless the
+   * innermost outer parenthesis is on a tuple */
+  let rec strip_wraps = (e: t): t => {
+    switch (e.term) {
+    | Wrap(inner, _) =>
+      switch (inner.term) {
+      | Tuple(_) => e
+      | _ => strip_wraps(inner)
+      }
+    | _ => e
+    };
+  };
 };
 
 module Rul = {
diff --git a/src/haz3lcore/statics/TermBase.re b/src/haz3lcore/statics/TermBase.re
index a3c0ab7f6f..ad182675a8 100644
--- a/src/haz3lcore/statics/TermBase.re
+++ b/src/haz3lcore/statics/TermBase.re
@@ -173,6 +173,8 @@ module rec Any: {
   [@deriving (show({with_path: false}), sexp, yojson)]
   type t = any_t;
 
+  let sort: t => Sort.t;
+
   let map_term:
     (
       ~f_exp: (Exp.t => Exp.t, Exp.t) => Exp.t=?,
@@ -190,6 +192,17 @@ module rec Any: {
   [@deriving (show({with_path: false}), sexp, yojson)]
   type t = any_t;
 
+  let sort = (any: t): Sort.t =>
+    switch (any) {
+    | Exp(_) => Exp
+    | Pat(_) => Pat
+    | Typ(_) => Typ
+    | TPat(_) => TPat
+    | Rul(_) => Rul
+    | Nul(_) => Nul
+    | Any(_) => Any
+    };
+
   let map_term =
       (
         ~f_exp=continue,
diff --git a/src/haz3lcore/tiles/ProjectorShape.re b/src/haz3lcore/tiles/ProjectorShape.re
new file mode 100644
index 0000000000..4ee99bce13
--- /dev/null
+++ b/src/haz3lcore/tiles/ProjectorShape.re
@@ -0,0 +1,27 @@
+open Util;
+
+/* A projector shape determines the space left for
+ * that projector, and how text flows around a projector
+ * in a text editor. All projectors have a horizontal
+ * extend (in characters), and the vertical extent may
+ * be either 1 character (Inline), or it may insert
+ * an additional number of linebreaks, either immediately
+ * after the projector (Block style) or defer them to
+ * the next linebreak (Tab style). In the latter case,
+ * if there are multiple Tab projectors on a line, the
+ * total extra linebreaks inserted is the maxium required
+ * to accomodate them */
+[@deriving (show({with_path: false}), sexp, yojson)]
+type vertical =
+  | Inline
+  | Tab(int)
+  | Block(int);
+
+[@deriving (show({with_path: false}), sexp, yojson)]
+type t = {
+  horizontal: int,
+  vertical,
+};
+
+let inline = (width: int): t => {horizontal: width, vertical: Inline};
+let default: t = inline(0);
diff --git a/src/haz3lcore/zipper/action/Perform.re b/src/haz3lcore/zipper/action/Perform.re
index f385093b35..c7a5f19b0f 100644
--- a/src/haz3lcore/zipper/action/Perform.re
+++ b/src/haz3lcore/zipper/action/Perform.re
@@ -89,11 +89,14 @@ let go_z =
 
   switch (a) {
   | Paste(String(clipboard)) =>
+    Animation.request([Animation.Actions.move("caret")]);
     switch (paste(z, clipboard)) {
     | None => Error(CantPaste)
     | Some(z) => Ok(z)
-    }
-  | Paste(Segment(segment)) => Ok(paste_segment(z, segment))
+    };
+  | Paste(Segment(segment)) =>
+    Animation.request([Animation.Actions.move("caret")]);
+    Ok(paste_segment(z, segment));
   | Cut =>
     /* System clipboard handling is done in Page.view handlers */
     switch (Destruct.go(Left, z)) {
@@ -125,7 +128,8 @@ let go_z =
       z,
     )
   | Move(d) =>
-    Move.go(d, z) |> Result.of_option(~error=Action.Failure.Cant_move)
+    Animation.request([Animation.Actions.move("caret")]);
+    Move.go(d, z) |> Result.of_option(~error=Action.Failure.Cant_move);
   | Jump(jump_target) =>
     (
       switch (jump_target) {
@@ -139,7 +143,9 @@ let go_z =
       }
     )
     |> Result.of_option(~error=Action.Failure.Cant_move)
-  | Unselect(Some(d)) => Ok(Zipper.directional_unselect(d, z))
+  | Unselect(Some(d)) =>
+    Animation.request([Animation.Actions.move("caret")]);
+    Ok(Zipper.directional_unselect(d, z));
   | Unselect(None) =>
     let z = Zipper.directional_unselect(z.selection.focus, z);
     Ok(z);
@@ -153,27 +159,31 @@ let go_z =
     | None => Error(Action.Failure.Cant_select)
     }
   | Select(Term(Current)) =>
+    Animation.request([Animation.Actions.move("caret")]);
     switch (Select.current_term(z)) {
     | None => Error(Cant_select)
     | Some(z) => Ok(z)
-    }
+    };
   | Select(Smart(n)) =>
+    Animation.request([Animation.Actions.move("caret")]);
     switch (smart_select(n, z)) {
     | None => Error(Cant_select)
     | Some(z) => Ok(z)
-    }
+    };
   | Select(Term(Id(id, d))) =>
+    Animation.request([Animation.Actions.move("caret")]);
     switch (Select.term(id, z)) {
     | Some(z) =>
       let z = d == Right ? z : Zipper.toggle_focus(z);
       Ok(z);
     | None => Error(Action.Failure.Cant_select)
-    }
+    };
   | Select(Tile(Current)) =>
+    Animation.request([Animation.Actions.move("caret")]);
     switch (Select.current_tile(z)) {
     | None => Error(Cant_select)
     | Some(z) => Ok(z)
-    }
+    };
   | Select(Tile(Id(id, d))) =>
     switch (Select.tile(id, z)) {
     | Some(z) =>
@@ -182,7 +192,8 @@ let go_z =
     | None => Error(Action.Failure.Cant_select)
     }
   | Select(Resize(d)) =>
-    Select.go(d, z) |> Result.of_option(~error=Action.Failure.Cant_select)
+    Animation.request([Animation.Actions.move("caret")]);
+    Select.go(d, z) |> Result.of_option(~error=Action.Failure.Cant_select);
   | Destruct(d) =>
     z
     |> Destruct.go(d)
diff --git a/src/haz3lweb/Main.re b/src/haz3lweb/Main.re
index 747cff3098..7889c8a823 100644
--- a/src/haz3lweb/Main.re
+++ b/src/haz3lweb/Main.re
@@ -161,11 +161,13 @@ let start = {
   // Triggers after every update
   let after_display = {
     Bonsai.Effect.of_sync_fun(
-      () =>
+      () => {
         if (scroll_to_caret.contents) {
           scroll_to_caret := false;
           JsUtil.scroll_cursor_into_view_if_needed();
-        },
+        };
+        Haz3lcore.Animation.go();
+      },
       (),
     );
   };
diff --git a/src/haz3lweb/app/common/ProjectorView.re b/src/haz3lweb/app/common/ProjectorView.re
index 118c1eb97e..317a31f985 100644
--- a/src/haz3lweb/app/common/ProjectorView.re
+++ b/src/haz3lweb/app/common/ProjectorView.re
@@ -18,6 +18,7 @@ let name = (p: ProjectorCore.kind): string =>
   | Slider => "slider"
   | SliderF => "sliderf"
   | TextArea => "text"
+  | Card => "card"
   };
 
 /* This must be updated and kept 1-to-1 with the above
@@ -32,6 +33,7 @@ let of_name = (p: string): ProjectorCore.kind =>
   | "slider" => Slider
   | "sliderf" => SliderF
   | "text" => TextArea
+  | "card" => Card
   | _ => failwith("Unknown projector kind")
   };
 
diff --git a/src/haz3lweb/app/editors/code/Code.re b/src/haz3lweb/app/editors/code/Code.re
index 421b1ce84f..4c6cb0bfca 100644
--- a/src/haz3lweb/app/editors/code/Code.re
+++ b/src/haz3lweb/app/editors/code/Code.re
@@ -6,6 +6,15 @@ open Util.Web;
 
 /* Helpers for rendering code text with holes and syntax highlighting */
 
+/* Tab projectors add linebreaks after the end of their line */
+let deferred_linebreaks: ref(list(int)) = ref([]);
+
+let consume_deferred_linebreaks = () => {
+  let max_deferred_linebreaks = List.fold_left(max, 0, deferred_linebreaks^);
+  deferred_linebreaks := [];
+  max_deferred_linebreaks;
+};
+
 let of_delim' =
   Core.Memo.general(
     ~cache_size_bound=10000,
@@ -23,9 +32,11 @@ let of_delim' =
       //let label = is_in_buffer ? AssistantExpander.mark(label) : label;
       let token = List.nth(label, i);
       /* Add indent to multiline tokens: */
+      let num_lb = StringUtil.num_linebreaks(token);
       let token =
-        StringUtil.num_linebreaks(token) == 0
+        num_lb == 0
           ? token : token ++ StringUtil.repeat(indent, Unicode.nbsp);
+      //TODO: deffered linebreaks
       [
         span(
           ~attrs=[Attr.classes(["token", cls, plurality])],
@@ -50,27 +61,38 @@ let of_delim =
 let space = " "; //Unicode.nbsp;
 
 let of_secondary =
-  Core.Memo.general(
-    ~cache_size_bound=10000, ((content, secondary_icons, indent)) =>
-    if (String.equal(Secondary.get_string(content), Form.linebreak)) {
-      let str = secondary_icons ? ">" : "";
-      [
-        span_c("linebreak", [text(str)]),
-        Node.text("\n"),
-        Node.text(StringUtil.repeat(indent, space)),
-      ];
-    } else if (String.equal(Secondary.get_string(content), Form.space)) {
-      let str = secondary_icons ? "·" : space;
-      [span_c("whitespace", [text(str)])];
-    } else if (Secondary.content_is_comment(content)) {
-      [span_c("comment", [Node.text(Secondary.get_string(content))])];
-    } else {
-      [span_c("secondary", [Node.text(Secondary.get_string(content))])];
-    }
-  );
+    //Core.Memo.general(  ~cache_size_bound=10000,
+    ((content, secondary_icons, indent)) =>
+  if (String.equal(Secondary.get_string(content), Form.linebreak)) {
+    let str = secondary_icons ? ">" : "";
+    [span_c("linebreak", [text(str)])]
+    @ List.init(1 + consume_deferred_linebreaks(), _ => Node.text("\n"))
+    @ [Node.text(StringUtil.repeat(indent, space))];
+  } else if (String.equal(Secondary.get_string(content), Form.space)) {
+    let str = secondary_icons ? "·" : space;
+    [span_c("whitespace", [text(str)])];
+  } else if (Secondary.content_is_comment(content)) {
+    [span_c("comment", [Node.text(Secondary.get_string(content))])];
+  } else {
+    [span_c("secondary", [Node.text(Secondary.get_string(content))])];
+  };
+//);
 
-let of_projector = (expected_sort, indent, token) =>
+let of_projector = (expected_sort, indent, shape: ProjectorCore.shape) => {
+  let token =
+    switch (shape.vertical) {
+    | Inline
+    | Tab(0)
+    | Block(0) => ProjectorCore.token(shape)
+    | Tab(num_lb) =>
+      deferred_linebreaks := [num_lb, ...deferred_linebreaks^];
+      ProjectorCore.token(shape);
+    | Block(_) =>
+      String.make(consume_deferred_linebreaks(), '\n')
+      ++ ProjectorCore.token(shape)
+    };
   of_delim'(([token], false, expected_sort, true, true, indent, 0));
+};
 
 module Text =
        (
@@ -81,6 +103,8 @@ module Text =
            let font_metrics: FontMetrics.t;
          },
        ) => {
+  deferred_linebreaks := [];
+
   let m = p => Measured.find_p(~msg="Text", p, M.map);
   let rec of_segment =
           (buffer_ids, no_sorts, sort, seg: Segment.t): list(Node.t) => {
@@ -112,7 +136,7 @@ module Text =
       of_projector(
         expected_sort,
         m(Projector(p)).origin.col,
-        p |> M.shape_of_proj |> ProjectorCore.token,
+        M.shape_of_proj(p),
       )
     };
   }
diff --git a/src/haz3lweb/app/editors/decoration/Deco.re b/src/haz3lweb/app/editors/decoration/Deco.re
index 16ac2a6b19..43d429190e 100644
--- a/src/haz3lweb/app/editors/decoration/Deco.re
+++ b/src/haz3lweb/app/editors/decoration/Deco.re
@@ -133,6 +133,7 @@ module HighlightSegment =
       let num_lb =
         switch (shape.vertical) {
         | Inline => 0
+        | Tab(num_lbs) => num_lbs
         | Block(num_lbs) => num_lbs
         };
       if (num_lb == 0) {
diff --git a/src/haz3lweb/www/img/cards-pixel-pattern.png b/src/haz3lweb/www/img/cards-pixel-pattern.png
new file mode 100644
index 0000000000..afc9219ad1
Binary files /dev/null and b/src/haz3lweb/www/img/cards-pixel-pattern.png differ
diff --git a/src/haz3lweb/www/style/projectors/proj-base.css b/src/haz3lweb/www/style/projectors/proj-base.css
index fc4c6ca070..eaed214ca2 100644
--- a/src/haz3lweb/www/style/projectors/proj-base.css
+++ b/src/haz3lweb/www/style/projectors/proj-base.css
@@ -3,6 +3,7 @@
 @import "panel.css";
 @import "proj-probe.css";
 @import "proj-type.css";
+@import "proj-cards.css";
 
 /* Default projector styles */
 
diff --git a/src/haz3lweb/www/style/projectors/proj-cards.css b/src/haz3lweb/www/style/projectors/proj-cards.css
new file mode 100644
index 0000000000..1c3bfb4655
--- /dev/null
+++ b/src/haz3lweb/www/style/projectors/proj-cards.css
@@ -0,0 +1,187 @@
+/* CARD SPRITES */
+
+:root {
+  --card-width: 35px;
+  --card-height: 47px;
+}
+
+/* Turn off caret when a block projector is focused */
+.code-deco:has(~ .projectors .projector.card.indicated) #caret .caret-path {
+  fill: #0000;
+}
+.code-deco:has(~ .projectors .projector.card.indicated) .indication {
+  display: none;
+}
+
+.projector.card {
+  perspective: 300px;
+}
+
+.projector.card.selected {
+  filter: brightness(0.72) sepia(1) hue-rotate(12deg) saturate(1.5);
+}
+.projector.card {
+  z-index: var(--projector-z); /* hack? to get above selection shard */
+}
+
+.projector.card > svg,
+.projector.card.indicated > svg {
+  display: none;
+}
+
+/* Singleton */
+.projector.card > .card-wrapper {
+  width: 100%;
+  height: 100%;
+  display: flex;
+  flex-direction: row;
+  justify-content: center;
+}
+
+.projector.card .card-scene {
+  width: var(--card-width);
+  height: var(--card-height);
+  transition: transform 0.25s;
+  transform-style: preserve-3d;
+  position: relative;
+  cursor: pointer;
+}
+
+@keyframes flip-card {
+  0% {
+    transform: rotateY(180deg);
+  }
+  50% {
+    transform: rotateY(160deg);
+  }
+  75% {
+    transform: rotateY(70deg);
+  }
+  100% {
+    transform: none;
+  }
+}
+
+.projector.card .flipped .card-scene {
+  transform: rotateY(180deg);
+  /* animation: flip-card 0.35s;
+  animation-direction: alternate-reverse; */
+}
+
+.card-sprite.back {
+  transform: rotateY(180deg);
+}
+
+.projector.card .card-sprite {
+  position: absolute;
+  backface-visibility: hidden;
+  display: flex;
+  justify-content: flex-start;
+  align-items: flex-start;
+  cursor: pointer;
+  width: var(--card-width);
+  height: var(--card-height);
+  image-rendering: pixelated;
+  background-image: url("../../img/cards-pixel-pattern.png");
+  filter: drop-shadow(-0.5px 0px 0px black) drop-shadow(0px -0.5px 0px black)
+    drop-shadow(1px 0px 0px black) drop-shadow(0px 1px 0px black);
+}
+
+.projector.card.Pat .card-sprite {
+  filter: drop-shadow(-1px 0px 0px var(--PAT))
+    drop-shadow(0px -1px 0px var(--PAT)) drop-shadow(1px 0px 0px var(--PAT))
+    drop-shadow(0px 1px 0px var(--PAT));
+}
+
+@keyframes blink-shadow {
+  0%,
+  50% {
+    filter: drop-shadow(0px -0.5px 0px black) drop-shadow(1px 0px 0px black)
+      drop-shadow(0px 1px 0px black) drop-shadow(-2px 0px 0px red);
+  }
+  51%,
+  100% {
+    filter: drop-shadow(-0.5px 0px 0px black) drop-shadow(0px -0.5px 0px black)
+      drop-shadow(1px 0px 0px black) drop-shadow(0px 1px 0px black);
+  }
+}
+
+@keyframes blink-shadow-right {
+  0%,
+  50% {
+    filter: drop-shadow(-0.5px 0px 0px black) drop-shadow(0px -0.5px 0px black)
+      drop-shadow(0px 1px 0px black) drop-shadow(2px 0px 0px red);
+  }
+  51%,
+  100% {
+    filter: drop-shadow(-0.5px 0px 0px black) drop-shadow(0px -0.5px 0px black)
+      drop-shadow(1px 0px 0px black) drop-shadow(0px 1px 0px black);
+  }
+}
+
+.projector.card.indicated.Left > .card-wrapper > .card-scene > .card-sprite,
+.projector.card.indicated.Left .hand > *:first-child .card-sprite {
+  animation: blink-shadow 1s infinite !important;
+}
+
+.projector.card.indicated.Right > .card-wrapper > .card-scene > .card-sprite,
+.projector.card.indicated.Right .hand > *:last-child .card-sprite {
+  animation: blink-shadow-right 1s infinite !important;
+}
+
+/* HAND */
+
+.card .hand {
+  display: flex;
+  flex-direction: row;
+  gap: 2px;
+  width: 100%;
+  height: 100%;
+}
+
+@keyframes rock-back-and-forth {
+  0% {
+    transform: rotate(0deg);
+  }
+  50% {
+    transform: rotate(4deg);
+  }
+}
+
+.projector.card.indicated .hand .card-scene:hover {
+  animation: rock-back-and-forth 0.25s infinite;
+}
+
+.projector.card .hand .card-sprite {
+  transition: transform 0.1s ease-in-out;
+}
+
+.projector.card.indicated .hand .card-sprite:hover {
+  translate: 0px -9px;
+  filter: drop-shadow(-1px 0px 0px black) drop-shadow(0px -1px 0px black)
+    drop-shadow(1.5px 0px 0px black) drop-shadow(0px 1.5px 0px black)
+    drop-shadow(2px 2px 0px #6666);
+}
+
+/* CHOOSER */
+
+.projector.card .chooser {
+  display: grid;
+  grid-template-columns: repeat(13, 1fr);
+}
+.projector.card:has(.chooser) {
+  justify-content: flex-start;
+  align-items: flex-start;
+}
+
+.projector.card .chooser .card-wrapper:hover {
+  animation: rock-back-and-forth 0.25s infinite;
+}
+
+.projector.card .chooser .card-wrapper.indicated {
+  filter: invert(1);
+}
+.projector.card .chooser .card-wrapper:hover {
+  filter: invert(1);
+  translate: 0px -5px;
+}
diff --git a/src/util/JsUtil.re b/src/util/JsUtil.re
index e84c34b69e..c891e8df9f 100644
--- a/src/util/JsUtil.re
+++ b/src/util/JsUtil.re
@@ -3,15 +3,15 @@ open Virtual_dom.Vdom;
 
 let get_elem_by_id = id => {
   let doc = Dom_html.document;
-  Js.Opt.get(
-    doc##getElementById(Js.string(id)),
-    () => {
-      print_endline(id);
-      assert(false);
-    },
-  );
+  Js.Opt.get(doc##getElementById(Js.string(id)), () => {assert(false)});
 };
 
+let get_elem_by_id_opt = id =>
+  switch (get_elem_by_id(id)) {
+  | exception _ => None
+  | e => Some(e)
+  };
+
 let get_elem_by_selector = selector => {
   let doc = Dom_html.document;
   Js.Opt.get(