diff --git a/src/haz3lcore/FontMetrics.re b/src/haz3lcore/FontMetrics.re
new file mode 100644
index 0000000000..dbc5e612f5
--- /dev/null
+++ b/src/haz3lcore/FontMetrics.re
@@ -0,0 +1,25 @@
+open Util;
+open Js_of_ocaml;
+
+[@deriving (show({with_path: false}), sexp, yojson)]
+type t = {
+  row_height: float,
+  col_width: float,
+};
+
+let init = {row_height: 10., col_width: 10.};
+
+let get_goal =
+    (
+      ~font_metrics: t,
+      text_box: Js.t(Dom_html.element),
+      e: Js.t(Dom_html.mouseEvent),
+    )
+    : Point.t => {
+  open Float;
+  let x_rel = of_int(e##.clientX) -. text_box##getBoundingClientRect##.left;
+  let y_rel = of_int(e##.clientY) -. text_box##getBoundingClientRect##.top;
+  let row = to_int(y_rel /. font_metrics.row_height);
+  let col = to_int(round(x_rel /. font_metrics.col_width));
+  {row, col};
+};
diff --git a/src/haz3lcore/Measured.re b/src/haz3lcore/Measured.re
index 61dad8a831..a524971079 100644
--- a/src/haz3lcore/Measured.re
+++ b/src/haz3lcore/Measured.re
@@ -282,7 +282,7 @@ let last_of_token = (token: string, origin: Point.t): Point.t =>
     row: origin.row + StringUtil.num_linebreaks(token),
   };
 
-let of_segment = (seg: Segment.t, info_map: Statics.Map.t): t => {
+let of_segment = (seg: Segment.t, token_of_proj: Base.projector => string): t => {
   let is_indented = is_indented_map(seg);
 
   // recursive across seg's bidelimited containers
@@ -353,8 +353,7 @@ let of_segment = (seg: Segment.t, info_map: Statics.Map.t): t => {
             let map = map |> add_g(g, {origin, last});
             (contained_indent, last, map);
           | Projector(p) =>
-            let token =
-              Projector.placeholder(p, Id.Map.find_opt(p.id, info_map));
+            let token = token_of_proj(p);
             let last = last_of_token(token, origin);
             let map = extra_rows(token, origin, map);
             let map = add_pr(p, {origin, last}, map);
@@ -403,3 +402,10 @@ let length = (seg: Segment.t, map: t): int =>
     let last = find_p(ListUtil.last(tl), map);
     last.last.col - first.origin.col;
   };
+
+/* Width in characters of row at measurement.origin */
+let start_row_width = (measurement: measurement, measured: t): int =>
+  switch (IntMap.find_opt(measurement.origin.row, measured.rows)) {
+  | None => 0
+  | Some(row) => row.max_col
+  };
diff --git a/src/haz3lcore/dynamics/EvalCtx.re b/src/haz3lcore/dynamics/EvalCtx.re
index 1f60bfa70a..bfafc131e0 100644
--- a/src/haz3lcore/dynamics/EvalCtx.re
+++ b/src/haz3lcore/dynamics/EvalCtx.re
@@ -23,6 +23,7 @@ type term =
   | BinOp2(Operators.op_bin, DHExp.t, t)
   | Tuple(t, (list(DHExp.t), list(DHExp.t)))
   | Test(t)
+  | Parens(t, Probe.tag)
   | ListLit(t, (list(DHExp.t), list(DHExp.t)))
   | MultiHole(t, (list(Any.t), list(Any.t)))
   | Cons1(t, DHExp.t)
@@ -88,6 +89,9 @@ let rec compose = (ctx: t, d: DHExp.t): DHExp.t => {
     | Test(ctx) =>
       let d1 = compose(ctx, d);
       Test(d1) |> wrap;
+    | Parens(ctx, tag) =>
+      let d1 = compose(ctx, d);
+      Parens(d1, tag) |> wrap;
     | UnOp(op, ctx) =>
       let d1 = compose(ctx, d);
       UnOp(op, d1) |> wrap;
diff --git a/src/haz3lcore/dynamics/Evaluator.re b/src/haz3lcore/dynamics/Evaluator.re
index fc4027f4d6..b91f76107b 100644
--- a/src/haz3lcore/dynamics/Evaluator.re
+++ b/src/haz3lcore/dynamics/Evaluator.re
@@ -41,6 +41,9 @@ module EvaluatorEVMode: {
   let update_test = (state, id, v) =>
     state := EvaluatorState.add_test(state^, id, v);
 
+  let update_probe = (state, id, v) =>
+    state := EvaluatorState.add_closure(state^, id, v);
+
   let req_value = (f, _, x) =>
     switch (f(x)) {
     | (BoxedValue, x) => (BoxedReady, x)
diff --git a/src/haz3lcore/dynamics/EvaluatorState.re b/src/haz3lcore/dynamics/EvaluatorState.re
index bb85612d05..f3dd98daaa 100644
--- a/src/haz3lcore/dynamics/EvaluatorState.re
+++ b/src/haz3lcore/dynamics/EvaluatorState.re
@@ -2,9 +2,14 @@
 type t = {
   stats: EvaluatorStats.t,
   tests: TestMap.t,
+  probes: Dynamics.Probe.Map.t,
 };
 
-let init = {stats: EvaluatorStats.initial, tests: TestMap.empty};
+let init = {
+  stats: EvaluatorStats.initial,
+  tests: TestMap.empty,
+  probes: Dynamics.Probe.Map.empty,
+};
 
 let take_step = ({stats, _} as es) => {
   ...es,
@@ -22,4 +27,9 @@ let add_test = ({tests, _} as es, id, report) => {
 
 let get_tests = ({tests, _}) => tests;
 
-let put_tests = (tests, es) => {...es, tests};
+let add_closure = ({probes, _} as es, id: Id.t, v: Dynamics.Probe.Closure.t) => {
+  ...es,
+  probes: Dynamics.Probe.Map.extend(id, v, probes),
+};
+
+let get_probes = ({probes, _}) => probes;
diff --git a/src/haz3lcore/dynamics/EvaluatorState.rei b/src/haz3lcore/dynamics/EvaluatorState.rei
index 916ac0586b..a20810396d 100644
--- a/src/haz3lcore/dynamics/EvaluatorState.rei
+++ b/src/haz3lcore/dynamics/EvaluatorState.rei
@@ -32,4 +32,6 @@ let add_test: (t, Id.t, TestMap.instance_report) => t;
 
 let get_tests: t => TestMap.t;
 
-let put_tests: (TestMap.t, t) => t;
+let add_closure: (t, Id.t, Dynamics.Probe.Closure.t) => t;
+
+let get_probes: t => Dynamics.Probe.Map.t;
diff --git a/src/haz3lcore/dynamics/EvaluatorStep.re b/src/haz3lcore/dynamics/EvaluatorStep.re
index 3416a46742..c473af4476 100644
--- a/src/haz3lcore/dynamics/EvaluatorStep.re
+++ b/src/haz3lcore/dynamics/EvaluatorStep.re
@@ -140,6 +140,9 @@ let rec matches =
       | Test(ctx) =>
         let+ ctx = matches(env, flt, ctx, exp, act, idx);
         Test(ctx) |> rewrap;
+      | Parens(ctx, tag) =>
+        let+ ctx = matches(env, flt, ctx, exp, act, idx);
+        Parens(ctx, tag) |> rewrap;
       | ListLit(ctx, ds) =>
         let+ ctx = matches(env, flt, ctx, exp, act, idx);
         ListLit(ctx, ds) |> rewrap;
@@ -332,6 +335,8 @@ module Decompose = {
     let otherwise = (env, o) => (o, Result.BoxedValue, env, ());
     let update_test = (state, id, v) =>
       state := EvaluatorState.add_test(state^, id, v);
+    let update_probe = (state, id, info) =>
+      state := EvaluatorState.add_closure(state^, id, info);
   };
 
   module Decomp = Transition(DecomposeEVMode);
@@ -377,6 +382,9 @@ module TakeStep = {
 
     let update_test = (state, id, v) =>
       state := EvaluatorState.add_test(state^, id, v);
+
+    let update_probe = (state, id, info) =>
+      state := EvaluatorState.add_closure(state^, id, info);
   };
 
   module TakeStepEV = Transition(TakeStepEVMode);
diff --git a/src/haz3lcore/dynamics/FilterMatcher.re b/src/haz3lcore/dynamics/FilterMatcher.re
index 61fd72f1bd..aeac72d1a8 100644
--- a/src/haz3lcore/dynamics/FilterMatcher.re
+++ b/src/haz3lcore/dynamics/FilterMatcher.re
@@ -1,11 +1,4 @@
-let evaluate_extend_env =
-    (new_bindings: Environment.t, to_extend: ClosureEnvironment.t)
-    : ClosureEnvironment.t => {
-  to_extend
-  |> ClosureEnvironment.map_of
-  |> Environment.union(new_bindings)
-  |> ClosureEnvironment.of_environment;
-};
+let evaluate_extend_env = ClosureEnvironment.extend_eval;
 
 let evaluate_extend_env_with_pat =
     (
@@ -104,8 +97,8 @@ let rec matches_exp =
     true;
   } else {
     switch (d |> DHExp.term_of, f |> DHExp.term_of) {
-    | (Parens(d), _) => matches_exp(d, f)
-    | (_, Parens(f)) => matches_exp(d, f)
+    | (Parens(d, _), _) => matches_exp(d, f)
+    | (_, Parens(f, _)) => matches_exp(d, f)
 
     | (Constructor("$e", _), _) => failwith("$e in matched expression")
     | (Constructor("$v", _), _) => failwith("$v in matched expression")
diff --git a/src/haz3lcore/dynamics/Probe.re b/src/haz3lcore/dynamics/Probe.re
new file mode 100644
index 0000000000..5530c941da
--- /dev/null
+++ b/src/haz3lcore/dynamics/Probe.re
@@ -0,0 +1,38 @@
+open Util;
+
+/* A syntax probe is inserted into syntax to capture
+ * information during evaluation. The tag type below,
+ * for the probe case, is used to collect binding ids
+ * which are used to faciltate capturing the values
+ * of certain variables in the environment. This captured
+ * information is, for a given closure, encoded in
+ * the `frame` type. */
+
+[@deriving (show({with_path: false}), sexp, yojson)]
+type t = {
+  refs: Binding.s,
+  stem: Binding.stem,
+};
+
+[@deriving (show({with_path: false}), sexp, yojson)]
+type tag =
+  | Paren
+  | Probe(t);
+
+/* Information about the evaluation of an ap */
+[@deriving (show({with_path: false}), sexp, yojson)]
+type frame = {
+  ap_id: Id.t, /* Syntax ID of the ap */
+  env_id: Id.t /* ID of ClosureEnv created by ap  */
+};
+
+/* List of applications prior to some evaluation */
+[@deriving (show({with_path: false}), sexp, yojson)]
+type stack = list(frame);
+
+let empty: t = {refs: [], stem: []};
+
+let env_stack: list(frame) => list(Id.t) =
+  List.map((en: frame) => en.env_id);
+
+let mk_frame = (~env_id: Id.t, ~ap_id: Id.t): frame => {env_id, ap_id};
diff --git a/src/haz3lcore/dynamics/Substitution.re b/src/haz3lcore/dynamics/Substitution.re
index 5d918e520b..53d3faaab5 100644
--- a/src/haz3lcore/dynamics/Substitution.re
+++ b/src/haz3lcore/dynamics/Substitution.re
@@ -115,9 +115,9 @@ let rec subst_var = (m, d1: DHExp.t, x: Var.t, d2: DHExp.t): DHExp.t => {
   | TyAlias(tp, ut, d4) =>
     let d4' = subst_var(m, d1, x, d4);
     TyAlias(tp, ut, d4') |> rewrap;
-  | Parens(d4) =>
+  | Parens(d4, tag) =>
     let d4' = subst_var(m, d1, x, d4);
-    Parens(d4') |> rewrap;
+    Parens(d4', tag) |> rewrap;
   | Deferral(_) => d2
   | DeferredAp(d3, d4s) =>
     let d3 = subst_var(m, d1, x, d3);
@@ -132,33 +132,28 @@ let rec subst_var = (m, d1: DHExp.t, x: Var.t, d2: DHExp.t): DHExp.t => {
 and subst_var_env =
     (m, d1: DHExp.t, x: Var.t, env: ClosureEnvironment.t)
     : ClosureEnvironment.t => {
-  let id = env |> ClosureEnvironment.id_of;
-  let map =
-    env
-    |> ClosureEnvironment.map_of
-    |> Environment.foldo(
-         ((x', d': DHExp.t), map) => {
-           let d' =
-             switch (DHExp.term_of(d')) {
-             /* Substitute each previously substituted binding into the
-              * fixpoint. */
-             | FixF(_) =>
-               map
-               |> Environment.foldo(
-                    ((x'', d''), d) => subst_var(m, d'', x'', d),
-                    d',
-                  )
-             | _ => d'
-             };
+  Environment.foldo(
+    ((x', d': DHExp.t), map) => {
+      let d' =
+        switch (DHExp.term_of(d')) {
+        /* Substitute each previously substituted binding into the
+         * fixpoint. */
+        | FixF(_) =>
+          map
+          |> Environment.foldo(
+               ((x'', d''), d) => subst_var(m, d'', x'', d),
+               d',
+             )
+        | _ => d'
+        };
 
-           /* Substitute. */
-           let d' = subst_var(m, d1, x, d');
-           Environment.extend(map, (x', d'));
-         },
-         Environment.empty,
-       );
-
-  ClosureEnvironment.wrap(id, map);
+      /* Substitute. */
+      let d' = subst_var(m, d1, x, d');
+      Environment.extend(map, (x', d'));
+    },
+    Environment.empty,
+  )
+  |> ClosureEnvironment.update_env(_, env);
 }
 
 and subst_var_filter =
diff --git a/src/haz3lcore/dynamics/Transition.re b/src/haz3lcore/dynamics/Transition.re
index c178a49dfa..ab733e2821 100644
--- a/src/haz3lcore/dynamics/Transition.re
+++ b/src/haz3lcore/dynamics/Transition.re
@@ -74,14 +74,7 @@ type step_kind =
   | Cast
   | RemoveTypeAlias
   | RemoveParens;
-let evaluate_extend_env =
-    (new_bindings: Environment.t, to_extend: ClosureEnvironment.t)
-    : ClosureEnvironment.t => {
-  to_extend
-  |> ClosureEnvironment.map_of
-  |> Environment.union(new_bindings)
-  |> ClosureEnvironment.of_environment;
-};
+let evaluate_extend_env = ClosureEnvironment.extend_eval;
 
 type rule =
   | Step({
@@ -138,6 +131,8 @@ module type EV_MODE = {
   let otherwise: (ClosureEnvironment.t, 'a) => requirements(unit, 'a);
 
   let update_test: (state, Id.t, TestMap.instance_report) => unit;
+
+  let update_probe: (state, Id.t, Dynamics.Probe.Closure.t) => unit;
 };
 
 module Transition = (EV: EV_MODE) => {
@@ -346,13 +341,23 @@ module Transition = (EV: EV_MODE) => {
       switch (DHExp.term_of(d1')) {
       | Constructor(_) => Constructor
       | Fun(dp, d3, Some(env'), _) =>
-        let.match env'' = (env', matches(dp, d2'));
-        Step({
-          expr: Closure(env'', d3) |> fresh,
-          state_update,
-          kind: FunAp,
-          is_value: false,
-        });
+        switch (matches(dp, d2')) {
+        | IndetMatch
+        | DoesNotMatch => Indet
+        | Matches(env'') =>
+          let env'' =
+            evaluate_extend_env(
+              ~frame=Some(Term.Exp.rep_id(d)),
+              env'',
+              env',
+            );
+          Step({
+            expr: Closure(env'', d3) |> fresh,
+            state_update,
+            kind: FunAp,
+            is_value: false,
+          });
+        }
       | Cast(
           d3',
           {term: Arrow(ty1, ty2), _},
@@ -770,7 +775,26 @@ module Transition = (EV: EV_MODE) => {
     | Undefined =>
       let. _ = otherwise(env, d);
       Indet;
-    | Parens(d) =>
+    | Parens(d'', Probe(pr)) =>
+      /* When evaluated, a probe adds a dynamics info entry
+       * reflecting the evaluation of the contained expression */
+      let. _ = otherwise(env, ((d, _)) => Parens(d, Probe(pr)) |> rewrap)
+      and. (d', _) =
+        req_final_or_value(
+          req(state, env),
+          d => Parens(d, Probe(pr)) |> wrap_ctx,
+          d'',
+        );
+      Step({
+        expr: d',
+        state_update: () => {
+          let closure = Dynamics.Probe.Closure.mk(d', env, pr);
+          update_probe(state, DHExp.rep_id(d), closure);
+        },
+        kind: RemoveParens,
+        is_value: true,
+      });
+    | Parens(d, Paren) =>
       let. _ = otherwise(env, d);
       Step({expr: d, state_update, kind: RemoveParens, is_value: false});
     | TyAlias(_, _, d) =>
diff --git a/src/haz3lcore/dynamics/TypeAssignment.re b/src/haz3lcore/dynamics/TypeAssignment.re
index 59b58aa56f..d708913cf8 100644
--- a/src/haz3lcore/dynamics/TypeAssignment.re
+++ b/src/haz3lcore/dynamics/TypeAssignment.re
@@ -344,7 +344,7 @@ and typ_of_dhexp = (ctx: Ctx.t, m: Statics.Map.t, dh: DHExp.t): option(Typ.t) =>
       None;
     };
   | TyAlias(_, _, d) => typ_of_dhexp(ctx, m, d)
-  | Parens(d) => typ_of_dhexp(ctx, m, d)
+  | Parens(d, _) => typ_of_dhexp(ctx, m, d)
   };
 };
 
diff --git a/src/haz3lcore/dynamics/ValueChecker.re b/src/haz3lcore/dynamics/ValueChecker.re
index a6e5ab30f0..c5fa1d4693 100644
--- a/src/haz3lcore/dynamics/ValueChecker.re
+++ b/src/haz3lcore/dynamics/ValueChecker.re
@@ -78,6 +78,7 @@ module ValueCheckerEVMode: {
   };
 
   let update_test = (_, _, _) => ();
+  let update_probe = (_, _, _) => ();
 };
 
 module CV = Transition(ValueCheckerEVMode);
diff --git a/src/haz3lcore/pretty/Abbreviate.re b/src/haz3lcore/pretty/Abbreviate.re
new file mode 100644
index 0000000000..1b9d24b88f
--- /dev/null
+++ b/src/haz3lcore/pretty/Abbreviate.re
@@ -0,0 +1,173 @@
+/* Abbreviate a term for display, specifically for the live
+ * value probe projector. This is currently specialized for
+ * expressions which are (at least partially) values. This
+ * is a bit rough right now, and should be redone when we
+ * projectors (in particular, fold) within value displays */
+
+let comp_elipses = "⋱";
+let flat_ellipses = "…";
+let ellipses_term = () => IdTagged.fresh(Invalid(comp_elipses): Exp.term);
+let flat_ellipses_term = () =>
+  IdTagged.fresh(Invalid(flat_ellipses): Exp.term);
+let available = ref(0);
+
+let abbreviate_str = (min_len: int, s: string): string => {
+  let len = String.length(s);
+  let ellipsis = "…";
+  if (len <= min_len || min_len < 1) {
+    available := available^ - len;
+    s;
+  } else if (min_len < 1) {
+    let str = String.sub(s, 0, 1) ++ ellipsis;
+    available := available^ - String.length(str);
+    str;
+  } else {
+    let str = String.sub(s, 0, min_len - 1) ++ ellipsis;
+    available := available^ - String.length(str);
+    str;
+  };
+};
+
+let rec abbreviate_exp = (exp: Exp.t): Exp.t => {
+  let rewrap = (term: Exp.term): Exp.t => {
+    {...exp, term};
+  };
+
+  let wrap_or = (term, str): Exp.term =>
+    if (available^ > String.length(str)) {
+      available := available^ - String.length(str);
+      term;
+    } else {
+      Invalid(abbreviate_str(available^, str));
+    };
+
+  let indet_term: Exp.term = Invalid("<INDET>");
+  let term: Exp.term =
+    switch (exp |> Exp.term_of) {
+    | Fun(_p, _e, _, Some(s)) => Invalid("<" ++ s ++ ">")
+    | Fun(_p, _e, _, None) => Invalid("<FUN>")
+    | BuiltinFun(_f) => Invalid("<BUILTIN>")
+    | Tuple([_]) => failwith("Singleton Tuples are not allowed")
+    | DynamicErrorHole(_exp, err) =>
+      Invalid("<" ++ InvalidOperationError.show(err) ++ ">")
+
+    // Atomic string cases
+    | Invalid(x) => Invalid(abbreviate_str(available^, x))
+    | String(s) => String(abbreviate_str(available^, s))
+    | Var(v) => Var(abbreviate_str(available^, v))
+    | Constructor(c, t) => Constructor(abbreviate_str(available^, c), t)
+
+    // Other atomic cases
+    | EmptyHole => EmptyHole
+    | ListLit([]) => ListLit([])
+    | Tuple([]) => Tuple([])
+    | Undefined => wrap_or(Undefined, "undefined")
+    | Bool(b) => wrap_or(Bool(b), string_of_bool(b))
+    | Int(n) =>
+      //TODO: smarter number summarization?
+      wrap_or(Int(n), string_of_int(n))
+    | Float(f) =>
+      //TODO: smarter number summarization?
+      wrap_or(Float(f), string_of_float(f))
+
+    // composite literal cases
+    | ListLit(xs) =>
+      //TODO: improve this logic
+      if (available^ < 6) {
+        ListLit([flat_ellipses_term()]);
+      } else {
+        available := available^ - 2;
+        let rec go = xs =>
+          switch (xs) {
+          | [] => []
+          | [x] => [abbreviate_exp(x)]
+          | [x, ...xs] =>
+            let hd = abbreviate_exp(x);
+            let tl =
+              if (available^ > 0) {
+                go(xs);
+              } else {
+                [flat_ellipses_term()];
+              };
+            [hd, ...tl];
+          };
+        ListLit(go(xs));
+      }
+
+    | Tuple(xs) =>
+      available := available^ - 2;
+      let rec go = xs =>
+        switch (xs) {
+        | [] => []
+        | [x] =>
+          if (available^ > 1) {
+            [abbreviate_exp(x)];
+          } else {
+            [flat_ellipses_term()];
+          }
+        | [x, ...xs] =>
+          let hd = abbreviate_exp(x);
+          let tl =
+            if (available^ > 0) {
+              available := available^ - 2;
+              go(xs);
+            } else {
+              [flat_ellipses_term()];
+            };
+          [hd, ...tl];
+        };
+      Tuple(go(xs));
+    | Ap(Forward, {term: Constructor(_str, _), _} as konst, arg) =>
+      let konst = abbreviate_exp(konst);
+      available := available^ - 2;
+      let arg =
+        if (available^ > 0) {
+          abbreviate_exp(arg);
+        } else {
+          ellipses_term();
+        };
+      Ap(Forward, konst, arg);
+    | Parens(e, pt) =>
+      available := available^ - 2;
+      Parens(abbreviate_exp(e), pt);
+
+    //unhandled atm
+    | Closure(_) => indet_term
+    | MultiHole(_es) => indet_term
+    | TypFun(_tp, _e, _) => indet_term
+    | FailedCast(_e, _, _t) => indet_term
+    | Cast(_e, _, _t) => indet_term
+
+    //non-value
+    | Cons(_) => indet_term
+    | Filter(_) => indet_term
+    | Ap(Forward, _e1, _e2) => indet_term
+    | Ap(Reverse, _e1, _e2) => indet_term
+    | Deferral(_d) => indet_term
+    | BinOp(_op, _l, _r) => indet_term
+    | Let(_p, _e1, _e2) => indet_term
+    | FixF(_p, _e, _) => indet_term
+    | TyAlias(_tp, _t, _e) => indet_term
+    | TypAp(_e, _t) => indet_term
+    | DeferredAp(_e, _es) => indet_term
+    | If(_e1, _e2, _e3) => indet_term
+    | Seq(_e1, _e2) => indet_term
+    | Test(_e) => indet_term
+    | ListConcat(_e1, _e2) => indet_term
+    | UnOp(Bool(Not), _e) => indet_term
+    | UnOp(Int(Minus), _e) => indet_term
+    | UnOp(Meta(Unquote), _e) => indet_term
+    | Match(_e, _rs) => indet_term
+    };
+  rewrap(term);
+};
+
+let abbreviate_exp = (~available as a=12, exp: Exp.t): (Exp.t, bool) => {
+  available := a;
+  available^ <= 1
+    ? (ellipses_term(), false)
+    : {
+      let exp = abbreviate_exp(exp);
+      (exp, available^ < 0);
+    };
+};
diff --git a/src/haz3lcore/pretty/ExpToSegment.re b/src/haz3lcore/pretty/ExpToSegment.re
index c2f57d0229..f1e3791856 100644
--- a/src/haz3lcore/pretty/ExpToSegment.re
+++ b/src/haz3lcore/pretty/ExpToSegment.re
@@ -49,6 +49,9 @@ let should_add_space = (s1, s2) =>
         && !Form.is_keyword(s1)
         && String.starts_with(s2, ~prefix="(") =>
     false
+  | _ when String.ends_with(s1, ~suffix="…") =>
+    /* Hack case for probe projector abbreviations */
+    false
   | _ => true
   };
 
@@ -118,12 +121,7 @@ let (@) = (seg1: Segment.t, seg2: Segment.t): Segment.t =>
 
 let fold_if = (condition, pieces) =>
   if (condition) {
-    [
-      ProjectorPerform.Update.init(
-        Fold,
-        mk_form("parens_exp", Id.mk(), [pieces]),
-      ),
-    ];
+    [Projector.init(Fold, mk_form("parens_exp", Id.mk(), [pieces]))];
   } else {
     pieces;
   };
@@ -131,7 +129,7 @@ let fold_if = (condition, pieces) =>
 let fold_fun_if = (condition, f_name: string, pieces) =>
   if (condition) {
     [
-      ProjectorPerform.Update.init_from_str(
+      Projector.init_from_str(
         Fold,
         mk_form("parens_exp", Id.mk(), [pieces]),
         ({text: f_name}: FoldProj.t)
@@ -225,7 +223,7 @@ let rec exp_to_pretty = (~settings: Settings.t, exp: Exp.t): pretty => {
     let id = exp |> Exp.rep_id;
     let+ es = es |> List.map(any_to_pretty(~settings)) |> all;
     ListUtil.flat_intersperse(Grout({id, shape: Concave}), es);
-  | Parens({term: Fun(p, e, _, _), _} as inner_exp) =>
+  | Parens({term: Fun(p, e, _, _), _} as inner_exp, _) =>
     // TODO: Add optional newlines
     let id = inner_exp |> Exp.rep_id;
     let+ p = pat_to_pretty(~settings: Settings.t, p)
@@ -382,8 +380,9 @@ let rec exp_to_pretty = (~settings: Settings.t, exp: Exp.t): pretty => {
     let id = exp |> Exp.rep_id;
     let+ e = go(e);
     [mk_form("test", id, [e])];
-  | Parens(e) =>
+  | Parens(e, _) =>
     // TODO: Add optional newlines
+
     let id = exp |> Exp.rep_id;
     let+ e = go(e);
     [mk_form("parens_exp", id, [e])];
@@ -674,6 +673,7 @@ let rec external_precedence = (exp: Exp.t): Precedence.t => {
   | EmptyHole
   | Deferral(_)
   | BuiltinFun(_)
+  | Constructor(_)
   | Undefined => Precedence.max
 
   // Same goes for forms which are already surrounded
@@ -684,7 +684,7 @@ let rec external_precedence = (exp: Exp.t): Precedence.t => {
 
   // Other forms
   | UnOp(Meta(Unquote), _) => Precedence.unquote
-  | Constructor(_) // Constructor is here because we currently always add a type annotation to constructors
+
   | Cast(_)
   | FailedCast(_) => Precedence.cast
   | Ap(Forward, _, _)
@@ -770,11 +770,11 @@ let external_precedence_typ = (tp: Typ.t) =>
 
 let paren_at = (internal_precedence: Precedence.t, exp: Exp.t): Exp.t =>
   external_precedence(exp) >= internal_precedence
-    ? Exp.fresh(Parens(exp)) : exp;
+    ? Exp.fresh(Parens(exp, Paren)) : exp;
 
 let paren_assoc_at = (internal_precedence: Precedence.t, exp: Exp.t): Exp.t =>
   external_precedence(exp) > internal_precedence
-    ? Exp.fresh(Parens(exp)) : exp;
+    ? Exp.fresh(Parens(exp, Paren)) : exp;
 
 let paren_pat_at = (internal_precedence: Precedence.t, pat: Pat.t): Pat.t =>
   external_precedence_pat(pat) >= internal_precedence
@@ -921,8 +921,8 @@ let rec parenthesize = (exp: Exp.t): Exp.t => {
   //     parenthesize(e) |> paren_at(Precedence.min),
   //   )
   //   |> rewrap
-  | Parens(e) =>
-    Parens(parenthesize(e) |> paren_at(Precedence.min)) |> rewrap
+  | Parens(e, tag) =>
+    Parens(parenthesize(e) |> paren_at(Precedence.min), tag) |> rewrap
   | Cons(e1, e2) =>
     Cons(
       parenthesize(e1) |> paren_at(Precedence.cons),
diff --git a/src/haz3lcore/prog/Dynamics.re b/src/haz3lcore/prog/Dynamics.re
new file mode 100644
index 0000000000..1f5b56ec20
--- /dev/null
+++ b/src/haz3lcore/prog/Dynamics.re
@@ -0,0 +1,132 @@
+open Util;
+
+/* Semantic information gathered during evaluation. This aspirationally
+  * unifies all evaluator output, in the same sense as Statics does for
+ * static information gathering, but right now it specifically handles
+ * closure gathering for probe projectors */
+
+module Probe = {
+  module Env = {
+    /* To avoid unnecessary de/serialization from evaluation worker,
+     * we refrain from retaining certain large un-educational values,
+     * such as closures. Which values are made opaque can be modulated
+     * via the below `elide` function */
+    [@deriving (show({with_path: false}), sexp, yojson)]
+    type elided_value =
+      | Opaque
+      | Val(DHExp.t);
+
+    /* A probe environment entry is a variable binding
+     * along with its corresponding elided value */
+    [@deriving (show({with_path: false}), sexp, yojson)]
+    type entry = {
+      binding: Binding.t,
+      value: elided_value,
+    };
+
+    /* A probe environment is a summarized version of the
+     * dynamic environment of the probed expression */
+    [@deriving (show({with_path: false}), sexp, yojson)]
+    type t = list(entry);
+
+    /* Selectively elide dynamic information not currently
+     * being used in the live probe UI, for (putative, unbenchmarked)
+     * performance purposes for worker de/serialization */
+    let elide = (env: ClosureEnvironment.t, d: DHExp.t) =>
+      switch (d.term) {
+      | Fun(_)
+      | FixF(_) => Opaque
+      | _ =>
+        Val(
+          d
+          |> DHExp.strip_casts
+          |> Exp.substitute_closures(ClosureEnvironment.map_of(env)),
+        )
+      };
+
+    let mk_entry = (env: ClosureEnvironment.t, {name, id, _}: Binding.t) =>
+      switch (ClosureEnvironment.lookup(env, name)) {
+      | Some(d) => {
+          binding: {
+            name,
+            id,
+          },
+          value: elide(env, d),
+        }
+      | None => failwith("Probe: variable not found in environment")
+      };
+
+    let mk = (env: ClosureEnvironment.t, refs: Binding.s) =>
+      List.map(mk_entry(env), refs);
+  };
+
+  /* A probe closure records an elided value and environment,
+   * in the above senses, along with a `stack` which records
+   * partial information about the execution trace prior to
+   * the creation of the closure */
+  module Closure = {
+    [@deriving (show({with_path: false}), sexp, yojson)]
+    type t = {
+      closure_id: Id.t, /* Primary ID (Unique) */
+      value: DHExp.t,
+      env: Env.t,
+      stack: Probe.stack,
+    };
+
+    let mk = (value: DHExp.t, env: ClosureEnvironment.t, pr: Probe.t) => {
+      closure_id: Id.mk(),
+      value,
+      stack: ClosureEnvironment.stack_of(env),
+      env: Env.mk(env, pr.refs),
+    };
+  };
+
+  /* Closures recorded during evaluation, indexed by the
+   * syntax ids of their initial expressions */
+  module Map = {
+    [@deriving (show({with_path: false}), sexp, yojson)]
+    type t = Id.Map.t(list(Closure.t));
+
+    let empty = Id.Map.empty;
+    let lookup = Id.Map.find_opt;
+
+    let extend = (id, report, map: t) =>
+      Id.Map.update(
+        id,
+        opt =>
+          switch (opt) {
+          | Some(a) => Some(a @ [report])
+          | None => Some([report])
+          },
+        map,
+      );
+  };
+
+  /* Intercepts a probe form and adds in static semantic information
+   * to guide dynamic information gathering  */
+  let instrument =
+      (m: Statics.Map.t, id: Id.t, probe_tag: Probe.tag): Probe.tag =>
+    switch (probe_tag) {
+    | Paren => Paren
+    | Probe(_) =>
+      Probe({
+        refs: Statics.Map.refs_in(m, id),
+        stem: Statics.Map.enclosing_abstractions(m, id),
+      })
+    };
+};
+
+module Info = {
+  /* Collected closures for a given id */
+  [@deriving (show({with_path: false}), sexp, yojson)]
+  type t = list(Probe.Closure.t);
+};
+
+module Map = {
+  /* Just a wrapping around the Probe map (for now) */
+  [@deriving (show({with_path: false}), sexp, yojson)]
+  type t = Probe.Map.t;
+  let empty: t = Probe.Map.empty;
+  let mk: t => t = Fun.id;
+  let lookup = Probe.Map.lookup;
+};
diff --git a/src/haz3lcore/statics/Binding.re b/src/haz3lcore/statics/Binding.re
new file mode 100644
index 0000000000..0c4ad5fdb4
--- /dev/null
+++ b/src/haz3lcore/statics/Binding.re
@@ -0,0 +1,26 @@
+open Util;
+
+/* The name and UUID of a variable binding site or reference.
+ * In principle the name is redundant, but it is convienient
+ * to have it */
+[@deriving (show({with_path: false}), sexp, yojson)]
+type t = {
+  id: Id.t,
+  name: string,
+};
+
+/* A list of binding sites or references */
+[@deriving (show({with_path: false}), sexp, yojson)]
+type s = list(t);
+
+/* A binding site as specified by its id and a list of
+ * the variables bound there*/
+[@deriving (show({with_path: false}), sexp, yojson)]
+type site = {
+  id: Id.t,
+  bound: s,
+};
+
+/* An enclosing list of binding sites */
+[@deriving (show({with_path: false}), sexp, yojson)]
+type stem = list(site);
diff --git a/src/haz3lcore/statics/Ctx.re b/src/haz3lcore/statics/Ctx.re
index f213a18cb7..f8a8886047 100644
--- a/src/haz3lcore/statics/Ctx.re
+++ b/src/haz3lcore/statics/Ctx.re
@@ -177,3 +177,10 @@ let filter_duplicates = (ctx: t): t =>
 
 let shadows_typ = (ctx: t, name: string): bool =>
   Form.is_base_typ(name) || lookup_tvar(ctx, name) != None;
+
+/* The binding (binding site id and name) of `name` in `ctx` */
+let binding_of = (ctx: t, name: Var.t): Binding.t =>
+  switch (lookup_var(ctx, name)) {
+  | Some({id, _}) => {id, name}
+  | _ => {id: Id.invalid, name}
+  };
diff --git a/src/haz3lcore/statics/Elaborator.re b/src/haz3lcore/statics/Elaborator.re
index 979a2128c8..7ac4eb811c 100644
--- a/src/haz3lcore/statics/Elaborator.re
+++ b/src/haz3lcore/statics/Elaborator.re
@@ -231,10 +231,16 @@ let rec elaborate = (m: Statics.Map.t, uexp: UExp.t): (DHExp.t, Typ.t) => {
       |> rewrap
       |> cast_from(Typ.temp(Unknown(Internal)));
     | Cast(e, _, _) // We remove these casts because they should be re-inserted in the recursive call
-    | FailedCast(e, _, _)
-    | Parens(e) =>
+    | FailedCast(e, _, _) =>
+      let (e', ty) = elaborate(m, e);
+      Parens(e' |> cast_from(ty), Paren) |> rewrap;
+    | Parens(e, Paren) =>
       let (e', ty) = elaborate(m, e);
       e' |> cast_from(ty);
+    | Parens(e, probe) =>
+      let (e', ty) = elaborate(m, e);
+      let probe = Dynamics.Probe.instrument(m, Exp.rep_id(uexp), probe);
+      Parens(e' |> cast_from(ty), probe) |> rewrap;
     | Deferral(_) => uexp
     | Int(_) => uexp |> cast_from(Int |> Typ.temp)
     | Bool(_) => uexp |> cast_from(Bool |> Typ.temp)
diff --git a/src/haz3lcore/statics/MakeTerm.re b/src/haz3lcore/statics/MakeTerm.re
index 06f5786879..85e5b069c6 100644
--- a/src/haz3lcore/statics/MakeTerm.re
+++ b/src/haz3lcore/statics/MakeTerm.re
@@ -13,13 +13,23 @@
 open Util;
 open Any;
 
+/* Hack: Temporary construct internal to maketerm
+ * to handle probe parsing; see `tokens` below */
+let probe_wrap = ["PROBE_WRAP", "PROBE_WRAP"];
+let is_probe_wrap = (==)(probe_wrap);
+
 // TODO make less hacky
 let tokens =
   Piece.get(
     _ => [],
     _ => [" "],
     (t: Tile.t) => t.shards |> List.map(List.nth(t.label)),
-    _ => [],
+    _ =>
+      /* Hack: These act as temporary wrappers for projectors,
+       * which are retained through maketerm so as to be used in
+       * dynamics. These are inserted and removed entirely internal
+       * to maketerm. */
+      probe_wrap,
   );
 
 [@deriving (show({with_path: false}), sexp, yojson)]
@@ -113,16 +123,9 @@ let return = (wrap, ids, tm) => {
 let projectors: ref(Id.Map.t(Piece.projector)) = ref(Id.Map.empty);
 
 /* Strip a projector from a segment and log it in the map */
-let rm_and_log_projectors = (seg: Segment.t): Segment.t =>
-  List.map(
-    fun
-    | Piece.Projector(pr) => {
-        projectors := Id.Map.add(pr.id, pr, projectors^);
-        pr.syntax;
-      }
-    | x => x,
-    seg,
-  );
+let log_projector = (pr: Base.projector): unit => {
+  projectors := Id.Map.add(pr.id, pr, projectors^);
+};
 
 let parse_sum_term: UTyp.t => ConstructorMap.variant(UTyp.t) =
   fun
@@ -191,7 +194,10 @@ and exp_term: unsorted => (UExp.term, list(Id.t)) = {
       | ([t], []) when Form.is_var(t) => ret(Var(t))
       | ([t], []) when Form.is_ctr(t) =>
         ret(Constructor(t, Unknown(Internal) |> Typ.temp))
-      | (["(", ")"], [Exp(body)]) => ret(Parens(body))
+      | (["(", ")"], [Exp(body)]) => ret(Parens(body, Paren))
+      | (label, [Exp(body)]) when is_probe_wrap(label) =>
+        // Temporary wrapping form to persist projector probes
+        ret(Parens(body, Probe(Probe.empty)))
       | (["[", "]"], [Exp(body)]) =>
         switch (body) {
         | {ids, copied: false, term: Tuple(es)} => (ListLit(es), ids)
@@ -354,6 +360,7 @@ and pat_term: unsorted => (UPat.term, list(Id.t)) = {
         | ([t], []) when t != " " && !Form.is_explicit_hole(t) =>
           Invalid(t)
         | (["(", ")"], [Pat(body)]) => Parens(body)
+        | (label, [Pat(body)]) when is_probe_wrap(label) => body.term
         | (["[", "]"], [Pat(body)]) =>
           switch (body) {
           | {term: Tuple(ps), _} => ListLit(ps)
@@ -414,6 +421,7 @@ and typ_term: unsorted => (UTyp.term, list(Id.t)) = {
         | (["String"], []) => String
         | ([t], []) when Form.is_typ_var(t) => Var(t)
         | (["(", ")"], [Typ(body)]) => Parens(body)
+        | (label, [Typ(body)]) when is_probe_wrap(label) => body.term
         | (["[", "]"], [Typ(body)]) => List(body)
         | ([t], []) when t != " " && !Form.is_explicit_hole(t) =>
           Unknown(Hole(Invalid(t)))
@@ -523,12 +531,14 @@ and rul = (unsorted: unsorted): Rul.t => {
 and unsorted = (skel: Skel.t, seg: Segment.t): unsorted => {
   /* Remove projectors. We do this here as opposed to removing
    * them in an external call to save a whole-syntax pass. */
-  let seg = rm_and_log_projectors(seg);
   let tile_kids = (p: Piece.t): list(Term.Any.t) =>
     switch (p) {
     | Secondary(_)
     | Grout(_) => []
-    | Projector(_) => []
+    | Projector({syntax, id: _, _} as pr) =>
+      let _ = log_projector(pr);
+      let sort = Piece.sort(syntax) |> fst;
+      [go_s(sort, Segment.skel([syntax]), [syntax])];
     | Tile({mold, shards, children, _}) =>
       Aba.aba_triples(Aba.mk(shards, children))
       |> List.map(((l, kid, r)) => {
diff --git a/src/haz3lcore/statics/Statics.re b/src/haz3lcore/statics/Statics.re
index 4818a4aaf8..9d9abde74b 100644
--- a/src/haz3lcore/statics/Statics.re
+++ b/src/haz3lcore/statics/Statics.re
@@ -34,6 +34,9 @@ module Map = {
   [@deriving (show({with_path: false}), sexp, yojson)]
   type t = Id.Map.t(Info.t);
 
+  let empty = Id.Map.empty;
+  let lookup = Id.Map.find_opt;
+
   let error_ids = (info_map: t): list(Id.t) =>
     Id.Map.fold(
       (id, info, acc) =>
@@ -43,6 +46,39 @@ module Map = {
       info_map,
       [],
     );
+
+  /* If id is a closure-creating form, returns the id and the names
+   * and binding site ids for all variables bound by the closure */
+  let abstraction_at = (map: t, id: Id.t): option(Binding.site) =>
+    switch (lookup(id, map)) {
+    | Some(InfoExp({ctx, term: {term: Fun(pat, _, _, _), _}, _})) =>
+      Some({id, bound: Term.Pat.bound_var_ids(ctx, pat)})
+    | _ => None
+    };
+
+  /* Returns the ids and other binding site infor for all
+   * closure-creating forms enclosing the term with the provided id */
+  let enclosing_abstractions = (map: t, id: Id.t): list(Binding.site) =>
+    switch (lookup(id, map)) {
+    | Some(info) =>
+      Info.ancestors_of(info)
+      |> List.fold_left(
+           (abstractions, ancestor_id) =>
+             Option.to_list(abstraction_at(map, ancestor_id)) @ abstractions,
+           [],
+         )
+    | None => []
+    };
+
+  /* The ids of binding sites for for all references in term with `id` */
+  let refs_in = (m: t, id: Id.t): Binding.s =>
+    switch (lookup(id, m)) {
+    | Some(InfoExp({co_ctx, ctx, _})) =>
+      co_ctx
+      |> VarMap.to_list
+      |> List.map(((n, _)) => Ctx.binding_of(ctx, n))
+    | _ => []
+    };
 };
 
 let map_m = (f, xs, m: Map.t) =>
@@ -269,9 +305,14 @@ and uexp_to_info_map =
       m,
     )
   | DynamicErrorHole(e, _)
-  | Parens(e) =>
+  | Parens(e, Paren) =>
     let (e, m) = go(~mode, e, m);
     add(~self=Just(e.ty), ~co_ctx=e.co_ctx, m);
+  | Parens(e, Probe(_)) =>
+    /* Currently doing this as otherwise it clobbers the statics
+     * for the contained expression as i'm just reusing the same id
+     * in order to associate it through dynamics */
+    go(~mode, e, m)
   | UnOp(Meta(Unquote), e) when is_in_filter =>
     let e: UExp.t = {
       ids: e.ids,
@@ -1010,11 +1051,3 @@ let get_pat_error_at = (info_map: Map.t, id: Id.t) => {
        }
      );
 };
-
-let collect_errors = (map: Map.t): list((Id.t, Info.error)) =>
-  Id.Map.fold(
-    (id, info: Info.t, acc) =>
-      Option.to_list(Info.error_of(info) |> Option.map(x => (id, x))) @ acc,
-    map,
-    [],
-  );
diff --git a/src/haz3lcore/statics/Term.re b/src/haz3lcore/statics/Term.re
index 5677278b67..2298d31d02 100644
--- a/src/haz3lcore/statics/Term.re
+++ b/src/haz3lcore/statics/Term.re
@@ -291,6 +291,15 @@ module Pat = {
     | ListLit(dps) => List.flatten(List.map(bound_vars, dps))
     | Ap(_, dp1) => bound_vars(dp1)
     };
+
+  let bound_var_ids = (ctx, pat): list(Binding.t) =>
+    bound_vars(pat)
+    |> List.map(name =>
+         switch (Ctx.lookup_var(ctx, name)) {
+         | Some({id, _}) => Binding.{id, name}
+         | None => {id: Id.invalid, name}
+         }
+       );
 };
 
 module Exp = {
@@ -434,7 +443,7 @@ module Exp = {
   // determine when to allow for recursive definitions in a let binding.
   let rec is_fun = (e: t) => {
     switch (e.term) {
-    | Parens(e) => is_fun(e)
+    | Parens(e, _) => is_fun(e)
     | Cast(e, _, _) => is_fun(e)
     | TypFun(_)
     | Fun(_)
@@ -478,7 +487,7 @@ module Exp = {
     || (
       switch (e.term) {
       | Cast(e, _, _)
-      | Parens(e) => is_tuple_of_functions(e)
+      | Parens(e, _) => is_tuple_of_functions(e)
       | Tuple(es) => es |> List.for_all(is_fun)
       | Invalid(_)
       | EmptyHole
@@ -534,7 +543,7 @@ module Exp = {
       Some(1);
     } else {
       switch (e.term) {
-      | Parens(e) => get_num_of_functions(e)
+      | Parens(e, _) => get_num_of_functions(e)
       | Tuple(es) => is_tuple_of_functions(e) ? Some(List.length(es)) : None
       | Invalid(_)
       | EmptyHole
@@ -761,7 +770,7 @@ module Exp = {
     switch (e.term) {
     | Fun(_, _, _, n) => n
     | FixF(_, e, _) => get_fn_name(e)
-    | Parens(e) => get_fn_name(e)
+    | Parens(e, _) => get_fn_name(e)
     | TypFun(_, _, n) => n
     | _ => None
     };
diff --git a/src/haz3lcore/statics/TermBase.re b/src/haz3lcore/statics/TermBase.re
index e8c4b339f3..e3e34020ec 100644
--- a/src/haz3lcore/statics/TermBase.re
+++ b/src/haz3lcore/statics/TermBase.re
@@ -89,7 +89,7 @@ and exp_term =
   | Test(exp_t)
   | Filter(stepper_filter_kind_t, exp_t)
   | Closure([@show.opaque] closure_environment_t, exp_t)
-  | Parens(exp_t) // (
+  | Parens(exp_t, Probe.tag)
   | Cons(exp_t, exp_t)
   | ListConcat(exp_t, exp_t)
   | UnOp(Operators.op_un, exp_t)
@@ -147,7 +147,11 @@ and rul_term =
   | Rules(exp_t, list((pat_t, exp_t)))
 and rul_t = IdTagged.t(rul_term)
 and environment_t = VarBstMap.Ordered.t_(exp_t)
-and closure_environment_t = (Id.t, environment_t)
+and closure_environment_t = {
+  id: Id.t,
+  env: environment_t,
+  stack: Probe.stack,
+}
 and stepper_filter_kind_t =
   | Filter(filter)
   | Residue(int, FilterAction.t)
@@ -328,7 +332,7 @@ and Exp: {
         | Test(e) => Test(exp_map_term(e))
         | Filter(f, e) => Filter(flt_map_term(f), exp_map_term(e))
         | Closure(env, e) => Closure(env, exp_map_term(e))
-        | Parens(e) => Parens(exp_map_term(e))
+        | Parens(e, tag) => Parens(exp_map_term(e), tag)
         | Cons(e1, e2) => Cons(exp_map_term(e1), exp_map_term(e2))
         | ListConcat(e1, e2) =>
           ListConcat(exp_map_term(e1), exp_map_term(e2))
@@ -354,9 +358,13 @@ and Exp: {
   let rec fast_equal = (e1, e2) =>
     switch (e1 |> IdTagged.term_of, e2 |> IdTagged.term_of) {
     | (DynamicErrorHole(x, _), _)
-    | (Parens(x), _) => fast_equal(x, e2)
+    | (Parens(x, Paren), _) => fast_equal(x, e2)
     | (_, DynamicErrorHole(x, _))
-    | (_, Parens(x)) => fast_equal(e1, x)
+    | (_, Parens(x, Paren)) => fast_equal(e1, x)
+    /* Below is kind of a hack to make EvalResult.calculate go after adding a projector.
+     * We should clarify syntactic/semantic equality here */
+    | (Parens(x1, Probe(_)), Parens(x2, Probe(_))) => fast_equal(x1, x2)
+    | (Parens(_, Probe(_)), _) => false
     | (EmptyHole, EmptyHole) => true
     | (Undefined, Undefined) => true
     | (Invalid(s1), Invalid(s2)) => s1 == s2
@@ -910,56 +918,42 @@ and ClosureEnvironment: {
   [@deriving (show({with_path: false}), sexp, yojson)]
   type t = closure_environment_t;
 
-  let wrap: (Id.t, Environment.t) => t;
+  let empty: t;
+
+  let of_environment: Environment.t => t;
 
   let id_of: t => Id.t;
   let map_of: t => Environment.t;
-
-  let to_list: t => list((Var.t, Exp.t));
-
-  let of_environment: Environment.t => t;
+  let stack_of: t => list(Probe.frame);
 
   let id_equal: (closure_environment_t, closure_environment_t) => bool;
 
-  let empty: t;
-  let is_empty: t => bool;
-  let length: t => int;
-
   let lookup: (t, Var.t) => option(Exp.t);
-  let contains: (t, Var.t) => bool;
-  let update: (Environment.t => Environment.t, t) => t;
-  let update_keep_id: (Environment.t => Environment.t, t) => t;
-  let extend: (t, (Var.t, Exp.t)) => t;
-  let extend_keep_id: (t, (Var.t, Exp.t)) => t;
-  let union: (t, t) => t;
-  let union_keep_id: (t, t) => t;
-  let map: (((Var.t, Exp.t)) => Exp.t, t) => t;
-  let map_keep_id: (((Var.t, Exp.t)) => Exp.t, t) => t;
-  let filter: (((Var.t, Exp.t)) => bool, t) => t;
-  let filter_keep_id: (((Var.t, Exp.t)) => bool, t) => t;
-  let fold: (((Var.t, Exp.t), 'b) => 'b, 'b, t) => 'b;
+  let update_env: (Environment.t => Environment.t, t) => t;
+  let extend_eval: (~frame: option(Id.t)=?, Environment.t, t) => t;
 
+  let to_list: t => list((Var.t, Exp.t));
   let without_keys: (list(Var.t), t) => t;
-  let with_symbolic_keys: (list(Var.t), t) => t;
-
-  let placeholder: t;
 } = {
   module Inner: {
     [@deriving (show({with_path: false}), sexp, yojson)]
     type t = closure_environment_t;
 
-    let wrap: (Id.t, Environment.t) => t;
+    let wrap: (Id.t, Environment.t, Probe.stack) => t;
 
     let id_of: t => Id.t;
     let map_of: t => Environment.t;
+    let stack_of: t => list(Probe.frame);
   } = {
     [@deriving (show({with_path: false}), sexp, yojson)]
     type t = closure_environment_t;
 
-    let wrap = (ei, map): t => (ei, map);
+    let wrap = (id, env, stack): t => {id, env, stack};
+
+    let id_of = t => t.id;
+    let map_of = t => t.env;
+    let stack_of = t => t.stack;
 
-    let id_of = ((ei, _)) => ei;
-    let map_of = ((_, map)) => map;
     let (sexp_of_t, t_of_sexp) =
       StructureShareSexp.structure_share_here(id_of, sexp_of_t, t_of_sexp);
   };
@@ -967,10 +961,7 @@ and ClosureEnvironment: {
 
   let to_list = env => env |> map_of |> Environment.to_listo;
 
-  let of_environment = map => {
-    let ei = Id.mk();
-    wrap(ei, map);
-  };
+  let of_environment = env => wrap(Id.mk(), env, []);
 
   /* Equals only needs to check environment id's (faster than structural equality
    * checking.) */
@@ -978,52 +969,39 @@ and ClosureEnvironment: {
 
   let empty = Environment.empty |> of_environment;
 
-  let is_empty = env => env |> map_of |> Environment.is_empty;
-
-  let length = env => Environment.length(map_of(env));
-
   let lookup = (env, x) =>
     env |> map_of |> (map => Environment.lookup(map, x));
 
-  let contains = (env, x) =>
-    env |> map_of |> (map => Environment.contains(map, x));
-
-  let update = (f, env) => env |> map_of |> f |> of_environment;
-
-  let update_keep_id = (f, env) => env |> map_of |> f |> wrap(env |> id_of);
-
-  let extend = (env, xr) =>
-    env |> update(map => Environment.extend(map, xr));
-
-  let extend_keep_id = (env, xr) =>
-    env |> update_keep_id(map => Environment.extend(map, xr));
-
-  let union = (env1, env2) =>
-    env2 |> update(map2 => Environment.union(env1 |> map_of, map2));
-
-  let union_keep_id = (env1, env2) =>
-    env2 |> update_keep_id(map2 => Environment.union(env1 |> map_of, map2));
+  let update_env = (f, env) => env |> map_of |> f |> of_environment;
 
-  let map = (f, env) => env |> update(Environment.mapo(f));
+  let without_keys = keys => update_env(Environment.without_keys(keys));
 
-  let map_keep_id = (f, env) => env |> update_keep_id(Environment.mapo(f));
-
-  let filter = (f, env) => env |> update(Environment.filtero(f));
-
-  let filter_keep_id = (f, env) =>
-    env |> update_keep_id(Environment.filtero(f));
-
-  let fold = (f, init, env) => env |> map_of |> Environment.foldo(f, init);
-
-  let placeholder = wrap(Id.invalid, Environment.empty);
+  let update_stack = (ap_id: option(Id.t), env) => {
+    let stack =
+      switch (ap_id) {
+      | None => stack_of(env)
+      | Some(ap_id) => [
+          Probe.mk_frame(~env_id=id_of(env), ~ap_id),
+          ...stack_of(env),
+        ]
+      };
+    {...env, stack};
+  };
 
-  let without_keys = keys => update(Environment.without_keys(keys));
-  let with_symbolic_keys = (keys, env) =>
-    List.fold_right(
-      (key, env) => extend(env, (key, Var(key) |> IdTagged.fresh)),
-      keys,
-      env,
-    );
+  /* Extend the environment with new bindings. ~frame is an optional argument which
+   * will add an entry in a stack of environment ids, used to track closure
+   * indications for live value probes. Currently this is used to create new
+   * frames for each environment created by a function application, and the
+   * syntax ids of those applications are used as the Id for the frame */
+  let extend_eval =
+      (~frame: option(Id.t)=None, new_bindings: Environment.t, to_extend: t)
+      : t =>
+    {
+      id: Id.mk(),
+      env: Environment.union(new_bindings, map_of(to_extend)),
+      stack: stack_of(to_extend),
+    }
+    |> update_stack(frame);
 }
 and StepperFilterKind: {
   [@deriving (show({with_path: false}), sexp, yojson)]
diff --git a/src/haz3lcore/tiles/Base.re b/src/haz3lcore/tiles/Base.re
index 8c127d83ba..cfc79efa8f 100644
--- a/src/haz3lcore/tiles/Base.re
+++ b/src/haz3lcore/tiles/Base.re
@@ -7,6 +7,7 @@ open Util;
 type kind =
   | Fold
   | Info
+  | Probe
   | Checkbox
   | Slider
   | SliderF
diff --git a/src/haz3lcore/zipper/Editor.re b/src/haz3lcore/zipper/Editor.re
index 819ae28bf3..6ad2f796a7 100644
--- a/src/haz3lcore/zipper/Editor.re
+++ b/src/haz3lcore/zipper/Editor.re
@@ -33,7 +33,7 @@ module CachedSyntax = {
   let yojson_of_t = _ => failwith("Editor.Meta.yojson_of_t");
   let t_of_yojson = _ => failwith("Editor.Meta.t_of_yojson");
 
-  let init = (z, info_map): t => {
+  let init = (~token_of_proj, z): t => {
     let segment = Zipper.unselect_and_zip(z);
     let MakeTerm.{term, terms, projectors} = MakeTerm.go(segment);
     {
@@ -42,7 +42,7 @@ module CachedSyntax = {
       term_ranges: TermRanges.mk(segment),
       tiles: TileMap.mk(segment),
       holes: Segment.holes(segment),
-      measured: Measured.of_segment(segment, info_map),
+      measured: Measured.of_segment(segment, token_of_proj),
       selection_ids: Selection.selection_ids(z.selection),
       term,
       terms,
@@ -52,9 +52,9 @@ module CachedSyntax = {
 
   let mark_old: t => t = old => {...old, old: true};
 
-  let calculate = (z: Zipper.t, info_map, old: t) =>
+  let calculate = (z: Zipper.t, info_map, dyn_map, old: t) =>
     old.old
-      ? init(z, info_map)
+      ? init(z, ~token_of_proj=Projector.token_of_proj(info_map, dyn_map))
       : {...old, selection_ids: Selection.selection_ids(z.selection)};
 };
 
@@ -97,7 +97,7 @@ module Model = {
       col_target: None,
     },
     history: History.empty,
-    syntax: CachedSyntax.init(zipper, Id.Map.empty),
+    syntax: CachedSyntax.init(zipper, ~token_of_proj=_ => ""),
   };
 
   type persistent = PersistentZipper.t;
@@ -129,9 +129,6 @@ module Model = {
       };
     };
   };
-
-  let indicated_projector = (editor: t) =>
-    Projector.indicated(editor.state.zipper);
 };
 
 module Update = {
@@ -241,6 +238,7 @@ module Update = {
         ~settings: CoreSettings.t,
         ~is_edited,
         new_statics,
+        dyn_map,
         {syntax, state, history}: Model.t,
       ) => {
     // 1. Recalculate the autocomplete buffer if necessary
@@ -264,7 +262,8 @@ module Update = {
     // 2. Recalculate syntax cache
     let syntax = is_edited ? CachedSyntax.mark_old(syntax) : syntax;
 
-    let syntax = CachedSyntax.calculate(zipper, new_statics.info_map, syntax);
+    let syntax =
+      CachedSyntax.calculate(zipper, new_statics.info_map, dyn_map, syntax);
 
     // Recombine
     Model.{
diff --git a/src/haz3lcore/zipper/Printer.re b/src/haz3lcore/zipper/Printer.re
index 1ab6b176f5..107e5c6a4f 100644
--- a/src/haz3lcore/zipper/Printer.re
+++ b/src/haz3lcore/zipper/Printer.re
@@ -56,9 +56,9 @@ let to_rows =
 
 let measured = z =>
   z
-  |> ProjectorPerform.Update.remove_all
+  |> ZipperBase.remove_all_projectors
   |> Zipper.seg_without_buffer
-  |> Measured.of_segment(_, Id.Map.empty);
+  |> Measured.of_segment(_, _ => ""); // No projectors
 
 let pretty_print = (~holes: option(string)=Some(""), z: Zipper.t): string =>
   to_rows(
diff --git a/src/haz3lcore/zipper/Projector.re b/src/haz3lcore/zipper/Projector.re
index 82b036b821..c80a10acc5 100644
--- a/src/haz3lcore/zipper/Projector.re
+++ b/src/haz3lcore/zipper/Projector.re
@@ -8,42 +8,49 @@ let to_module = (kind: Base.kind): (module Cooked) =>
   switch (kind) {
   | Fold => (module Cook(FoldProj.M))
   | Info => (module Cook(InfoProj.M))
+  | Probe => (module Cook(ProbeProj.M))
   | Slider => (module Cook(SliderProj.M))
   | SliderF => (module Cook(SliderFProj.M))
   | Checkbox => (module Cook(CheckboxProj.M))
   | TextArea => (module Cook(TextAreaProj.M))
   };
 
+/* Currently projection is limited to convex pieces */
+let minimum_projection_condition = (syntax: syntax): bool =>
+  Piece.is_convex(syntax);
+
+let init = (kind: t, syntax: syntax): syntax => {
+  /* We set the projector id equal to the Piece id for convienence
+   * including cursor-info association. We maintain this invariant
+   * when we update a projector's contained syntax */
+  let (module P) = to_module(kind);
+  switch (P.can_project(syntax) && minimum_projection_condition(syntax)) {
+  | false => syntax
+  | true => Projector({id: Piece.id(syntax), kind, model: P.init, syntax})
+  };
+};
+
+let init_from_str = (kind: t, syntax: syntax, model_str: string): syntax => {
+  let (module P) = to_module(kind);
+  switch (P.can_project(syntax) && minimum_projection_condition(syntax)) {
+  | false => syntax
+  | true => Projector({id: Piece.id(syntax), kind, model: model_str, syntax})
+  };
+};
+
 let shape = (p: Base.projector, info: info): shape => {
   let (module P) = to_module(p.kind);
   P.placeholder(p.model, info);
 };
 
-/* A projector is replaced by a placeholder in the underlying
- * editor for view purposes. This projector is an all-whitespace
- * monotile. Currently there is no explicit notion of placeholders
- * in the zipper; a tile consisting of any number of whitespaces
- * is considered a placeholder. This could be made more principled.
- * Note that a placeholder retains the UUID of the underlying. */
-let placeholder = (p: Base.projector, ci: option(Info.t)): string =>
-  switch (shape(p, {id: p.id, syntax: p.syntax, ci})) {
+/* Returns a token consisting of whitespace (possibly including linebreaks)
+ * representing the space to leave for the projector in the underlying code view */
+let token_of_proj =
+    (statics: Statics.Map.t, dynamics: Dynamics.Map.t, p: Base.projector) => {
+  let statics = Statics.Map.lookup(p.id, statics);
+  let dynamics = Dynamics.Map.lookup(p.id, dynamics);
+  switch (shape(p, {id: p.id, syntax: p.syntax, statics, dynamics})) {
   | Inline(width) => String.make(width, ' ')
   | Block({row, col}) => String.make(row - 1, '\n') ++ String.make(col, ' ')
   };
-
-/* Currently projection is limited to convex pieces */
-let minimum_projection_condition = (syntax: syntax): bool =>
-  Piece.is_convex(syntax);
-
-/* Returns the projector at the caret, if any */
-let indicated = (z: ZipperBase.t) => {
-  open Util.OptUtil.Syntax;
-  let* id = Indicated.index(z);
-  let* (p, _, _) = Indicated.piece(z);
-  let+ projector =
-    switch (p) {
-    | Projector(pr) => Some(pr)
-    | _ => None
-    };
-  (id, projector);
 };
diff --git a/src/haz3lcore/zipper/ProjectorBase.re b/src/haz3lcore/zipper/ProjectorBase.re
index 5abe811d76..24b224222c 100644
--- a/src/haz3lcore/zipper/ProjectorBase.re
+++ b/src/haz3lcore/zipper/ProjectorBase.re
@@ -32,7 +32,29 @@ type external_action =
 type info = {
   id: Id.t,
   syntax,
-  ci: option(Info.t),
+  statics: option(Statics.Info.t),
+  dynamics: option(Dynamics.Info.t),
+};
+
+/* Utility functions/values for to projector views.
+ * These should be considered unstable/experimental
+ * features which have yet to be integrated into the
+ * projector API in a disciplined way */
+[@deriving (show({with_path: false}), sexp, yojson)]
+type utility = {
+  /* The current font metrics for the editor, usable
+   * to coordinate with the parent coordinate grid */
+  font_metrics: FontMetrics.t,
+  /* X position in pixels of the end of the row where
+   * where the projector starts; usable to position part
+   * of the projector UI at the end of the row */
+  offside_offset: float,
+  /* Non-interactive view for segments, included here
+   * because of cyclic dependency issues*/
+  view: (Sort.t, Base.segment) => Node.t,
+  /* Convert an expression to a segment, included here
+   * because of cyclic dependency issues*/
+  exp_to_seg: Exp.t => Base.segment,
 };
 
 /* To add a new projector:
@@ -83,7 +105,8 @@ module type Projector = {
       model,
       ~info: info,
       ~local: action => Ui_effect.t(unit),
-      ~parent: external_action => Ui_effect.t(unit)
+      ~parent: external_action => Ui_effect.t(unit),
+      ~utility: utility
     ) =>
     Node.t;
   /* How much space should be left in the code view for
@@ -123,12 +146,13 @@ module Cook = (C: Projector) : Cooked => {
   let init = C.init |> serialize_m;
   let can_project = C.can_project;
   let can_focus = C.can_focus;
-  let view = (m, ~info, ~local, ~parent) =>
+  let view = (m, ~info, ~local, ~parent, ~utility) =>
     C.view(
       deserialize_m(m),
       ~info,
       ~local=a => local(serialize_a(a)),
       ~parent,
+      ~utility,
     );
   let placeholder = m =>
     m |> Sexplib.Sexp.of_string |> C.model_of_sexp |> C.placeholder;
diff --git a/src/haz3lcore/zipper/ZipperBase.re b/src/haz3lcore/zipper/ZipperBase.re
index cb6311a4b8..f241e24700 100644
--- a/src/haz3lcore/zipper/ZipperBase.re
+++ b/src/haz3lcore/zipper/ZipperBase.re
@@ -160,3 +160,11 @@ module MapPiece = {
       go(f, z);
     };
 };
+
+let remove_all_projectors = (z: t): t =>
+  MapPiece.go(
+    fun
+    | Projector(pr) => pr.syntax
+    | x => x,
+    z,
+  );
diff --git a/src/haz3lcore/zipper/action/Indicated.re b/src/haz3lcore/zipper/action/Indicated.re
index 6cfbc5f997..47fd56d945 100644
--- a/src/haz3lcore/zipper/action/Indicated.re
+++ b/src/haz3lcore/zipper/action/Indicated.re
@@ -91,6 +91,18 @@ let index = (z: ZipperBase.t): option(Id.t) =>
   | Some((p, _, _)) => Some(Piece.id(p))
   };
 
+/* Returns the projector at the caret, if any */
+let projector = (z: ZipperBase.t) => {
+  let* id = index(z);
+  let* (p, _, _) = piece(z);
+  let+ projector =
+    switch (p) {
+    | Projector(pr) => Some(pr)
+    | _ => None
+    };
+  (id, projector);
+};
+
 let piece'' = piece'(~no_ws=true, ~ign=Piece.is_secondary);
 
 let ci_of =
diff --git a/src/haz3lcore/zipper/action/ProjectorPerform.re b/src/haz3lcore/zipper/action/ProjectorPerform.re
index 55a1d2e8f7..647802269a 100644
--- a/src/haz3lcore/zipper/action/ProjectorPerform.re
+++ b/src/haz3lcore/zipper/action/ProjectorPerform.re
@@ -10,30 +10,11 @@ module Update = {
     | x => x
     };
 
-  let init = (kind: t, syntax: syntax): syntax => {
-    /* We set the projector id equal to the Piece id for convienence
-     * including cursor-info association. We maintain this invariant
-     * when we update a projector's contained syntax */
-    let (module P) = to_module(kind);
-    switch (P.can_project(syntax) && minimum_projection_condition(syntax)) {
-    | false => syntax
-    | true => Projector({id: Piece.id(syntax), kind, model: P.init, syntax})
-    };
-  };
-
-  let init_from_str = (kind: t, syntax: syntax, model_str: string): syntax => {
-    let (module P) = to_module(kind);
-    switch (P.can_project(syntax) && minimum_projection_condition(syntax)) {
-    | false => syntax
-    | true =>
-      Projector({id: Piece.id(syntax), kind, model: model_str, syntax})
-    };
-  };
-
   let add_projector = (kind: Base.kind, id: Id.t, syntax: syntax) =>
     switch (syntax) {
-    | Projector(pr) when Piece.id(syntax) == id => init(kind, pr.syntax)
-    | syntax when Piece.id(syntax) == id => init(kind, syntax)
+    | Projector(pr) when Piece.id(syntax) == id =>
+      Projector.init(kind, pr.syntax)
+    | syntax when Piece.id(syntax) == id => Projector.init(kind, syntax)
     | x => x
     };
 
@@ -46,13 +27,7 @@ module Update = {
   let add_or_remove_projector = (kind: Base.kind, id: Id.t, syntax: syntax) =>
     switch (syntax) {
     | Projector(pr) when Piece.id(syntax) == id => pr.syntax
-    | syntax when Piece.id(syntax) == id => init(kind, syntax)
-    | x => x
-    };
-
-  let remove_any_projector = (syntax: syntax) =>
-    switch (syntax) {
-    | Projector(pr) => pr.syntax
+    | syntax when Piece.id(syntax) == id => Projector.init(kind, syntax)
     | x => x
     };
 
@@ -71,7 +46,7 @@ module Update = {
     ZipperBase.MapPiece.fast_local(remove_projector(id), id, z);
 
   let remove_all = (z: ZipperBase.t): ZipperBase.t =>
-    ZipperBase.MapPiece.go(remove_any_projector, z);
+    ZipperBase.remove_all_projectors(z);
 };
 
 /* If the caret is inside the indicated piece, move it out
@@ -126,7 +101,7 @@ let go =
         jump_to_id_indicated(z, id) |> Option.value(~default=z)
       | Some(_) => z
       };
-    switch (Projector.indicated(z)) {
+    switch (Indicated.projector(z)) {
     | Some((_, p)) =>
       let (module P) = to_module(p.kind);
       P.focus((id, d));
diff --git a/src/haz3lcore/zipper/projectors/CheckboxProj.re b/src/haz3lcore/zipper/projectors/CheckboxProj.re
index b1d734a8cf..73c2c60b12 100644
--- a/src/haz3lcore/zipper/projectors/CheckboxProj.re
+++ b/src/haz3lcore/zipper/projectors/CheckboxProj.re
@@ -25,7 +25,13 @@ let put = (bool: bool): Piece.t => bool |> string_of_bool |> mk_mono(Exp);
 let toggle = (piece: Piece.t) => put(!get(piece));
 
 let view =
-    (_, ~info, ~local as _, ~parent: external_action => Ui_effect.t(unit)) =>
+    (
+      _,
+      ~info,
+      ~local as _,
+      ~parent: external_action => Ui_effect.t(unit),
+      ~utility as _,
+    ) =>
   Node.input(
     ~attrs=
       [
diff --git a/src/haz3lcore/zipper/projectors/FoldProj.re b/src/haz3lcore/zipper/projectors/FoldProj.re
index 8f9665dea6..af47bb2558 100644
--- a/src/haz3lcore/zipper/projectors/FoldProj.re
+++ b/src/haz3lcore/zipper/projectors/FoldProj.re
@@ -20,7 +20,7 @@ module M: Projector = {
   let placeholder = (m, _) =>
     Inline(m.text == "⋱" ? 2 : m.text |> String.length);
   let update = (m, _) => m;
-  let view = (m: model, ~info as _, ~local as _, ~parent) =>
+  let view = (m: model, ~info as _, ~local as _, ~parent, ~utility as _) =>
     div(
       ~attrs=[Attr.on_double_click(_ => parent(Remove))],
       [text(m.text)],
diff --git a/src/haz3lcore/zipper/projectors/InfoProj.re b/src/haz3lcore/zipper/projectors/InfoProj.re
index 6b467e76b1..5f9fde0273 100644
--- a/src/haz3lcore/zipper/projectors/InfoProj.re
+++ b/src/haz3lcore/zipper/projectors/InfoProj.re
@@ -68,7 +68,7 @@ module M: Projector = {
     display_ty(model, info) |> totalize_ty |> Typ.pretty_print;
 
   let placeholder = (model, info) =>
-    Inline((display(model, info.ci) |> String.length) + 5);
+    Inline((display(model, info.statics) |> String.length) + 5);
 
   let update = (model, a: action) =>
     switch (a, model) {
@@ -76,17 +76,17 @@ module M: Projector = {
     | (ToggleDisplay, Self) => Expected
     };
 
-  let view = (model, ~info, ~local, ~parent as _) =>
+  let view = (model, ~info, ~local, ~parent as _, ~utility as _) =>
     div(
       ~attrs=[
         Attr.classes(["info", "code"]),
         Attr.on_mousedown(_ => local(ToggleDisplay)),
       ],
       [
-        text("⋱ " ++ display_mode(model, info.ci) ++ " "),
+        text("⋱ " ++ display_mode(model, info.statics) ++ " "),
         div(
           ~attrs=[Attr.classes(["type"])],
-          [text(display(model, info.ci))],
+          [text(display(model, info.statics))],
         ),
       ],
     );
diff --git a/src/haz3lcore/zipper/projectors/ProbeProj.re b/src/haz3lcore/zipper/projectors/ProbeProj.re
new file mode 100644
index 0000000000..292360aaca
--- /dev/null
+++ b/src/haz3lcore/zipper/projectors/ProbeProj.re
@@ -0,0 +1,293 @@
+open Util;
+open ProjectorBase;
+open Virtual_dom.Vdom;
+open Node;
+open Js_of_ocaml;
+
+[@deriving (show({with_path: false}), sexp, yojson)]
+type t = {
+  [@default "⋱"]
+  text: string,
+  len: int,
+  show_all_vals: bool,
+};
+
+[@deriving (show({with_path: false}), sexp, yojson)]
+type a =
+  | ChangeLength(int)
+  | ToggleShowAllVals;
+
+let stack = stack =>
+  stack
+  |> List.rev
+  |> List.map(({env_id, ap_id}: Probe.frame) =>
+       ""
+       ++ String.sub(Id.to_string(env_id), 0, 2)
+       ++ "\n"
+       ++ String.sub(Id.to_string(ap_id), 0, 2)
+     )
+  |> String.concat("\n");
+
+let env_cursor: ref(list(Id.t)) = ref([]);
+let last_target: ref(list('a)) = ref([]);
+let mousedown: ref(option(Js.t(Dom_html.element))) = ref(Option.None);
+
+let common_suffix_length = (s1, s2) =>
+  List.length(ListUtil.max_common_suffix(s1, s2));
+
+let one_is_suffix_of_other = (s1, s2) =>
+  common_suffix_length(s1, s2) == List.length(s1)
+  || common_suffix_length(s1, s2) == List.length(s2);
+
+let comparor = (a: Dynamics.Probe.Closure.t, b: Dynamics.Probe.Closure.t) => {
+  compare(
+    common_suffix_length(env_cursor^, Probe.env_stack(b.stack)),
+    common_suffix_length(env_cursor^, Probe.env_stack(a.stack)),
+  );
+};
+
+let show_indicator = stack => {
+  let local = Probe.env_stack(stack);
+  env_cursor^ == []
+  && local == []
+  || env_cursor^ != []
+  && one_is_suffix_of_other(env_cursor^, local);
+};
+
+let seg_view = (utility, available, seg) =>
+  seg
+  |> DHExp.strip_casts
+  |> Abbreviate.abbreviate_exp(~available)
+  |> fst
+  |> utility.exp_to_seg
+  |> utility.view(Exp);
+
+let get_goal = (utility: utility, e: Js.t(Dom_html.mouseEvent)) =>
+  FontMetrics.get_goal(
+    ~font_metrics=utility.font_metrics,
+    e##.currentTarget
+    |> Js.Opt.get(_, _ => failwith(""))
+    |> JsUtil.get_child_with_class(_, "code")
+    |> Option.get,
+    e |> Js.Unsafe.coerce,
+  );
+
+let resizable_val =
+    (
+      ~resizable=false,
+      model,
+      utility,
+      local,
+      closure: Dynamics.Probe.Closure.t,
+    ) => {
+  let val_pointerdown = (e: Js.t(Dom_html.pointerEvent)) => {
+    let target = e##.target |> Js.Opt.get(_, _ => failwith("no target"));
+    JsUtil.setPointerCapture(target, e##.pointerId) |> ignore;
+    mousedown := Some(target);
+    env_cursor := Probe.env_stack(closure.stack);
+    last_target := [target];
+    Effect.Ignore;
+  };
+
+  let val_pointerup = (e: Js.t(Dom_html.pointerEvent)) => {
+    switch (mousedown^) {
+    | Some(target) =>
+      JsUtil.releasePointerCapture(target, e##.pointerId) |> ignore
+    | None => ()
+    };
+    mousedown := None;
+    Effect.Ignore;
+  };
+
+  //TODO: refactor to pointermove when supported
+  let val_mousemove = (e: Js.t(Dom_html.mouseEvent)) =>
+    switch (mousedown^) {
+    | Some(_elem) when Js.to_bool(e##.shiftKey) && resizable =>
+      /* Ideally we could just use hasPointerCapture... */
+      let goal = get_goal(utility, e);
+      local(ChangeLength(goal.col));
+    | _ => Effect.Ignore
+    };
+
+  div(
+    ~attrs=[
+      Attr.title(stack(closure.stack)),
+      Attr.classes(
+        ["val-resize"] @ (show_indicator(closure.stack) ? ["cursor"] : []),
+      ),
+      Attr.on_double_click(_ => local(ToggleShowAllVals)),
+      Attr.on_pointerdown(val_pointerdown),
+      Attr.on_pointerup(val_pointerup),
+      Attr.on_mousemove(val_mousemove),
+    ],
+    [seg_view(utility, model.len, closure.value)],
+  );
+};
+
+let env_val = (en: Dynamics.Probe.Env.entry, utility: utility) => {
+  Node.div(
+    ~attrs=[Attr.classes(["live-env-entry"])],
+    [
+      Node.text(en.binding.name ++ "="),
+      switch (en.value) {
+      | Opaque => Node.text("Opaque")
+      | Val(d) => seg_view(utility, 12, d)
+      },
+    ],
+  );
+};
+
+/* Remove opaque values like function literals */
+let rm_opaques:
+  list(Dynamics.Probe.Env.entry) => list(Dynamics.Probe.Env.entry) =
+  List.filter_map((en: Dynamics.Probe.Env.entry) =>
+    switch (en.value) {
+    | Opaque => None
+    | Val(_) => Some(en)
+    }
+  );
+
+/* Is the underlying syntax a variable reference? */
+let is_var_ref = (info: info): bool =>
+  switch (MakeTerm.go([info.syntax]).term.term) {
+  | Var(_) => true
+  | _ => false
+  };
+
+let env_view = (closure: Dynamics.Probe.Closure.t, utility: utility): Node.t =>
+  Node.div(
+    ~attrs=[Attr.classes(["live-env"])],
+    closure.env |> rm_opaques |> List.map(en => env_val(en, utility)),
+  );
+
+let closure_view =
+    (
+      info,
+      utility: utility,
+      model: t,
+      local,
+      index,
+      closure: Dynamics.Probe.Closure.t,
+    ) =>
+  div(
+    ~attrs=[
+      Attr.classes(
+        ["closure"] @ (show_indicator(closure.stack) ? ["cursor"] : []),
+      ),
+    ],
+    [resizable_val(~resizable=index == 0, model, utility, local, closure)]
+    @ (is_var_ref(info) ? [] : [env_view(closure, utility)]),
+  );
+
+let select_vals = (model: t, vals) => {
+  switch (List.sort(comparor, vals)) {
+  | [] => []
+  | [hd, ..._] when !model.show_all_vals => [hd]
+  | _ => vals
+  };
+};
+
+let offside_pos = utility =>
+  Attr.create(
+    "style",
+    Printf.sprintf("position: absolute; left: %fpx;", utility.offside_offset),
+  );
+
+let offside_view = (info, ~model, ~local, ~utility: utility) => {
+  Node.div(
+    ~attrs=[Attr.classes(["live-offside"]), offside_pos(utility)],
+    switch (info.dynamics) {
+    | Some(di) =>
+      List.mapi(
+        closure_view(info, utility, model, local),
+        select_vals(model, di),
+      )
+    | _ => []
+    },
+  );
+};
+
+let num_closures = (info: info) =>
+  switch (info.dynamics) {
+  | Some(di) => List.length(di)
+  | _ => 0
+  };
+
+let num_closures_view = (info: info) => {
+  let num_closures = num_closures(info);
+  let description = num_closures < 1000 ? string_of_int(num_closures) : "1k+";
+  div(
+    ~attrs=[
+      Attr.title(string_of_int(num_closures)),
+      Attr.classes(["num-closures"]),
+    ],
+    [text(description)],
+  );
+};
+
+let syntax_str = (info: info) => {
+  let max_len = 30;
+  let str = Printer.of_segment(~holes=None, [info.syntax]);
+  let str = Re.Str.global_replace(Re.Str.regexp("\n"), " ", str);
+  String.length(str) > max_len ? String.sub(str, 0, max_len) ++ "..." : str;
+};
+
+let syntax_view = (info: info) => info |> syntax_str |> text;
+
+let placeholder = (_m, info) =>
+  Inline(3 + String.length(syntax_str(info)));
+
+let icon = div(~attrs=[Attr.classes(["icon"])], [text("🔍")]);
+// let icon =
+//   img(
+//     ~attrs=[
+//       Attr.classes(["icon"]),
+//       Attr.create("height", "18px"),
+//       Attr.create("width", "18px"),
+//       Attr.src("img/noun-search-5661270.svg"),
+//       Attr.alt("probe"),
+//     ],
+//     (),
+//   );
+
+let view = (model: t, ~info, ~local, ~parent as _, ~utility: utility) =>
+  div([
+    offside_view(info, ~model, ~local, ~utility),
+    div(
+      ~attrs=[
+        Attr.classes(["main"]),
+        Attr.on_click(_ => {
+          env_cursor := [];
+          Effect.Ignore;
+        }),
+      ],
+      [icon, syntax_view(info), num_closures_view(info)],
+    ),
+  ]);
+
+let update = (m: t, a: a) => {
+  print_endline("update: action:" ++ show_a(a));
+  switch (a) {
+  | ChangeLength(len) =>
+    if (len > (-1)) {
+      {...m, len};
+    } else {
+      m;
+    }
+  | ToggleShowAllVals => {...m, show_all_vals: !m.show_all_vals}
+  };
+};
+
+module M: Projector = {
+  [@deriving (show({with_path: false}), sexp, yojson)]
+  type model = t;
+  [@deriving (show({with_path: false}), sexp, yojson)]
+  type action = a;
+  let init = {text: "🔍", len: 12, show_all_vals: true};
+  let can_project = _ => true;
+  let can_focus = false;
+  let placeholder = placeholder;
+  let update = update;
+  let view = view;
+  let focus = _ => ();
+};
diff --git a/src/haz3lcore/zipper/projectors/SliderFProj.re b/src/haz3lcore/zipper/projectors/SliderFProj.re
index 4ad36621ad..713315d395 100644
--- a/src/haz3lcore/zipper/projectors/SliderFProj.re
+++ b/src/haz3lcore/zipper/projectors/SliderFProj.re
@@ -27,7 +27,13 @@ module M: Projector = {
   let placeholder = (_, _) => Inline(10);
   let update = (model, _) => model;
   let view =
-      (_, ~info, ~local as _, ~parent: external_action => Ui_effect.t(unit)) =>
+      (
+        _,
+        ~info,
+        ~local as _,
+        ~parent: external_action => Ui_effect.t(unit),
+        ~utility as _,
+      ) =>
     Util.Web.range(
       ~attrs=[Attr.on_input((_, v) => parent(SetSyntax(put(v))))],
       get(info.syntax) |> Printf.sprintf("%.2f"),
diff --git a/src/haz3lcore/zipper/projectors/SliderProj.re b/src/haz3lcore/zipper/projectors/SliderProj.re
index 2a73c6d012..5d7b3fe5a4 100644
--- a/src/haz3lcore/zipper/projectors/SliderProj.re
+++ b/src/haz3lcore/zipper/projectors/SliderProj.re
@@ -24,7 +24,13 @@ module M: Projector = {
   let placeholder = (_, _) => Inline(10);
   let update = (model, _) => model;
   let view =
-      (_, ~info, ~local as _, ~parent: external_action => Ui_effect.t(unit)) =>
+      (
+        _,
+        ~info,
+        ~local as _,
+        ~parent: external_action => Ui_effect.t(unit),
+        ~utility as _,
+      ) =>
     Util.Web.range(
       ~attrs=[Attr.on_input((_, v) => parent(SetSyntax(put(v))))],
       get(info.syntax),
diff --git a/src/haz3lcore/zipper/projectors/TextAreaProj.re b/src/haz3lcore/zipper/projectors/TextAreaProj.re
index d6488afd86..63748ea0f9 100644
--- a/src/haz3lcore/zipper/projectors/TextAreaProj.re
+++ b/src/haz3lcore/zipper/projectors/TextAreaProj.re
@@ -77,7 +77,7 @@ let textarea =
     [],
   );
 
-let view = (_, ~info, ~local as _, ~parent) => {
+let view = (_, ~info, ~local as _, ~parent, ~utility as _) => {
   let text = info.syntax |> get |> Form.strip_quotes;
   Node.div(
     ~attrs=[Attr.classes(["wrapper"])],
diff --git a/src/haz3lweb/Keyboard.re b/src/haz3lweb/Keyboard.re
index 2d39ac24a0..f219b69a1f 100644
--- a/src/haz3lweb/Keyboard.re
+++ b/src/haz3lweb/Keyboard.re
@@ -103,6 +103,11 @@ let handle_key_event = (k: Key.t): option(Action.t) => {
   | {key: D("ƒ"), sys: Mac, shift: Up, meta: Up, ctrl: Up, alt: Down} =>
     /* Curly ƒ is what holding option turns f into on Mac */
     Some(Project(ToggleIndicated(Fold)))
+  | {key: D("v"), sys: PC, shift: Up, meta: Up, ctrl: Up, alt: Down} =>
+    Some(Project(ToggleIndicated(Probe)))
+  | {key: D("√"), sys: Mac, shift: Up, meta: Up, ctrl: Up, alt: Down} =>
+    /* √ is what holding option turns f into on Mac */
+    Some(Project(ToggleIndicated(Probe)))
   | {key: D(key), sys: _, shift: Up, meta: Up, ctrl: Up, alt: Down} =>
     switch (key) {
     | "ArrowLeft" => now(MoveToBackpackTarget(Left(ByToken)))
diff --git a/src/haz3lweb/app/common/FontMetrics.re b/src/haz3lweb/app/common/FontMetrics.re
index 4ed525c176..a72aa95763 100644
--- a/src/haz3lweb/app/common/FontMetrics.re
+++ b/src/haz3lweb/app/common/FontMetrics.re
@@ -1,10 +1,2 @@
-open Util;
-
-[@warning "-33"]
 [@deriving (show({with_path: false}), sexp, yojson)]
-type t = {
-  row_height: float,
-  col_width: float,
-};
-
-let init = {row_height: 10., col_width: 10.};
+include Haz3lcore.FontMetrics;
diff --git a/src/haz3lweb/app/common/ProjectorView.re b/src/haz3lweb/app/common/ProjectorView.re
index 387ccc5cd7..5212457892 100644
--- a/src/haz3lweb/app/common/ProjectorView.re
+++ b/src/haz3lweb/app/common/ProjectorView.re
@@ -7,15 +7,14 @@ open Util;
 open Util.OptUtil.Syntax;
 open Util.Web;
 
-type kind = Base.kind;
-
 /* A friendly name for each projector. This is used
  * both for identifying a projector in the CSS and for
  * selecting projectors in the projector panel menu */
-let name = (p: kind): string =>
+let name = (p: Base.kind): string =>
   switch (p) {
   | Fold => "fold"
   | Info => "type"
+  | Probe => "probe"
   | Checkbox => "check"
   | Slider => "slider"
   | SliderF => "sliderf"
@@ -25,10 +24,11 @@ let name = (p: kind): string =>
 /* This must be updated and kept 1-to-1 with the above
  * name function in order to be able to select the
  * projector in the projector panel menu */
-let of_name = (p: string): kind =>
+let of_name = (p: string): Base.kind =>
   switch (p) {
   | "fold" => Fold
   | "type" => Info
+  | "probe" => Probe
   | "check" => Checkbox
   | "slider" => Slider
   | "sliderf" => SliderF
@@ -109,6 +109,58 @@ let handle = (id, action: external_action): Action.project =>
   | SetSyntax(f) => SetSyntax(id, f)
   };
 
+/* Position in pixels for the position offset characters to the
+ * right of the end of the row at measurement.origin. */
+let offside =
+    (
+      ~offset: int,
+      font_metrics: FontMetrics.t,
+      measurement: Measured.measurement,
+      measured: Measured.t,
+    )
+    : float =>
+  font_metrics.col_width
+  *. float_of_int(
+       Measured.start_row_width(measurement, measured)
+       + offset
+       - measurement.origin.col,
+     );
+
+/* Gather utility functions/values to be passed to the projector.
+ * See ProjectorBase.utility definition for more information */
+let collate_utility =
+    (
+      globals: Globals.t,
+      measurement: Measured.measurement,
+      cached_syntax: Editor.CachedSyntax.t,
+    )
+    : ProjectorBase.utility => {
+  {
+    font_metrics: globals.font_metrics,
+    offside_offset:
+      offside(
+        ~offset=4,
+        globals.font_metrics,
+        measurement,
+        cached_syntax.measured,
+      ),
+    view: (sort, seg) =>
+      CodeViewable.view_segment(~globals, ~sort, ~token_of_proj=_ => "", seg),
+    exp_to_seg: exp =>
+      exp
+      |> DHExp.strip_casts
+      |> ExpToSegment.exp_to_segment(
+           ~settings={
+             inline: false,
+             fold_case_clauses: false,
+             fold_fn_bodies: false,
+             hide_fixpoints: false,
+             fold_cast_types: false,
+           },
+         ),
+  };
+};
+
 /* Extracts projector-instance-specific metadata necessary to
  * render the view, instantiates appropriate action handlers,
  * renders the view, and then wraps it so as to position it
@@ -118,31 +170,35 @@ let setup_view =
       id: Id.t,
       ~cached_statics: CachedStatics.t,
       ~cached_syntax: Editor.CachedSyntax.t,
+      ~dynamics,
       ~inject: Action.t => Ui_effect.t(unit),
-      ~font_metrics,
+      ~globals: Globals.t,
       ~indication: option(Direction.t),
     )
     : option(Node.t) => {
   let* p = Id.Map.find_opt(id, cached_syntax.projectors);
   let* syntax = Some(p.syntax);
-  let ci = Id.Map.find_opt(id, cached_statics.info_map);
-  let info = {id, ci, syntax};
+  let statics = Statics.Map.lookup(id, cached_statics.info_map);
+  let dynamics = Dynamics.Map.lookup(id, dynamics);
+  let info = {id, statics, dynamics, syntax};
   let+ measurement = Measured.find_pr_opt(p, cached_syntax.measured);
+  let utility = collate_utility(globals, measurement, cached_syntax);
   let (module P) = to_module(p.kind);
   let parent = a => inject(Project(handle(id, a)));
   let local = a => inject(Project(SetModel(id, P.update(p.model, a))));
   view_wrapper(
     ~inject,
-    ~font_metrics,
+    ~font_metrics=globals.font_metrics,
     ~measurement,
     ~indication,
     ~info,
     ~selected=List.mem(id, cached_syntax.selection_ids),
     p,
-    P.view(p.model, ~info, ~local, ~parent),
+    P.view(p.model, ~info, ~local, ~parent, ~utility),
   );
 };
 
+/* Is the piece with id indicated? If so, where is it wrt the caret? */
 let indication = (z, id) =>
   switch (Indicated.piece(z)) {
   | Some((p, d, _)) when Piece.id(p) == id => Some(Direction.toggle(d))
@@ -154,15 +210,12 @@ let indication = (z, id) =>
 let all =
     (
       z,
+      ~globals: Globals.t,
       ~cached_statics: CachedStatics.t,
       ~cached_syntax: Editor.CachedSyntax.t,
+      ~dynamics: Dynamics.Map.t,
       ~inject,
-      ~font_metrics,
     ) => {
-  // print_endline(
-  //   "cardinal: "
-  //   ++ (meta.projected.projectors |> Id.Map.cardinal |> string_of_int),
-  // );
   div_c(
     "projectors",
     List.filter_map(
@@ -172,8 +225,9 @@ let all =
           id,
           ~cached_statics,
           ~cached_syntax,
+          ~dynamics,
           ~inject,
-          ~font_metrics,
+          ~globals,
           ~indication,
         );
       },
@@ -191,7 +245,7 @@ let all =
  * For example, without the modifiers check, this would break selection
  * around a projector. */
 let key_handoff = (editor: Editor.t, key: Key.t): option(Action.project) =>
-  switch (Editor.Model.indicated_projector(editor)) {
+  switch (Indicated.projector(editor.state.zipper)) {
   | None => None
   | Some((id, p)) =>
     let* (_, d, _) = Indicated.piece(editor.state.zipper);
diff --git a/src/haz3lweb/app/editors/cell/CellEditor.re b/src/haz3lweb/app/editors/cell/CellEditor.re
index d3b7ca5b97..7aaa7afba7 100644
--- a/src/haz3lweb/app/editors/cell/CellEditor.re
+++ b/src/haz3lweb/app/editors/cell/CellEditor.re
@@ -68,7 +68,13 @@ module Update = {
       )
       : Model.t => {
     let editor =
-      CodeEditable.Update.calculate(~settings, ~is_edited, ~stitch, editor);
+      CodeEditable.Update.calculate(
+        ~settings,
+        ~is_edited,
+        ~stitch,
+        ~dynamics=EvalResult.Model.dynamics(result),
+        editor,
+      );
     let result =
       EvalResult.Update.calculate(
         ~settings={...settings, assist: false},
@@ -187,6 +193,7 @@ module View = {
               : (action => inject(MainEditor(action))),
           ~selected=selected == Some(MainEditor),
           ~overlays=overlays(model.editor.editor),
+          ~dynamics=EvalResult.Model.dynamics(model.result),
           ~sort?,
           model.editor,
         ),
diff --git a/src/haz3lweb/app/editors/code/Code.re b/src/haz3lweb/app/editors/code/Code.re
index ee0cd2b564..00a8778199 100644
--- a/src/haz3lweb/app/editors/code/Code.re
+++ b/src/haz3lweb/app/editors/code/Code.re
@@ -71,23 +71,15 @@ let of_secondary =
     }
   );
 
-let of_projector = (p, expected_sort, indent, info_map) =>
-  of_delim'((
-    [Projector.placeholder(p, Id.Map.find_opt(p.id, info_map))],
-    false,
-    expected_sort,
-    true,
-    true,
-    indent,
-    0,
-  ));
+let of_projector = (expected_sort, indent, token) =>
+  of_delim'(([token], false, expected_sort, true, true, indent, 0));
 
 module Text =
        (
          M: {
            let map: Measured.t;
            let settings: Settings.Model.t;
-           let info_map: Statics.Map.t;
+           let token_of_proj: Base.projector => string;
          },
        ) => {
   let m = p => Measured.find_p(~msg="Text", p, M.map);
@@ -118,7 +110,11 @@ module Text =
     | Secondary({content, _}) =>
       of_secondary((content, M.settings.secondary_icons, m(p).last.col))
     | Projector(p) =>
-      of_projector(p, expected_sort, m(Projector(p)).origin.col, M.info_map)
+      of_projector(
+        expected_sort,
+        m(Projector(p)).origin.col,
+        M.token_of_proj(p),
+      )
     };
   }
   and of_tile = (buffer_ids, expected_sort: Sort.t, t: Tile.t): list(Node.t) => {
@@ -160,12 +156,13 @@ let rec holes =
      );
 
 let simple_view = (~font_metrics, ~segment, ~settings: Settings.t): Node.t => {
-  let map = Measured.of_segment(segment, Id.Map.empty);
+  let token_of_proj = _ => ""; /* Assume this doesn't contain projectors */
+  let map = Measured.of_segment(segment, token_of_proj);
   module Text =
     Text({
       let map = map;
       let settings = settings;
-      let info_map = Id.Map.empty; /* Assume this doesn't contain projectors */
+      let token_of_proj = token_of_proj;
     });
   let holes = holes(~map, ~font_metrics, segment);
   div(
diff --git a/src/haz3lweb/app/editors/code/CodeEditable.re b/src/haz3lweb/app/editors/code/CodeEditable.re
index e90635a3ee..800a869689 100644
--- a/src/haz3lweb/app/editors/code/CodeEditable.re
+++ b/src/haz3lweb/app/editors/code/CodeEditable.re
@@ -162,24 +162,6 @@ module View = {
   type event =
     | MakeActive;
 
-  let get_goal =
-      (
-        ~font_metrics: FontMetrics.t,
-        text_box: Js.t(Dom_html.element),
-        e: Js.t(Dom_html.mouseEvent),
-      ) => {
-    let rect = text_box##getBoundingClientRect;
-    let goal_x = float_of_int(e##.clientX);
-    let goal_y = float_of_int(e##.clientY);
-    Point.{
-      row: Float.to_int((goal_y -. rect##.top) /. font_metrics.row_height),
-      col:
-        Float.(
-          to_int(round((goal_x -. rect##.left) /. font_metrics.col_width))
-        ),
-    };
-  };
-
   let mousedown_overlay = (~globals: Globals.t, ~inject) =>
     Node.div(
       ~attrs=
@@ -187,6 +169,7 @@ module View = {
           id("mousedown-overlay"),
           on_mouseup(_ => globals.inject_global(SetMousedown(false))),
           on_mousemove(e => {
+            let _ = ignore(e##.button);
             let mouse_handler =
               e##.target |> Js.Opt.get(_, _ => failwith("no target"));
             let text_box =
@@ -198,7 +181,11 @@ module View = {
               )
               |> Option.get;
             let goal =
-              get_goal(~font_metrics=globals.font_metrics, text_box, e);
+              FontMetrics.get_goal(
+                ~font_metrics=globals.font_metrics,
+                text_box,
+                e,
+              );
             inject(Action.Select(Resize(Goal(Point(goal)))));
           }),
         ],
@@ -207,7 +194,7 @@ module View = {
 
   let mousedown_handler = (~globals: Globals.t, ~signal, ~inject, evt) => {
     let goal =
-      get_goal(
+      FontMetrics.get_goal(
         ~font_metrics=globals.font_metrics,
         evt##.currentTarget
         |> Js.Opt.get(_, _ => failwith(""))
@@ -244,6 +231,7 @@ module View = {
         ~selected: bool,
         ~overlays: list(Node.t)=[],
         ~sort=?,
+        ~dynamics: Dynamics.Map.t,
         model: Model.t,
       ) => {
     let edit_decos = {
@@ -252,20 +240,28 @@ module View = {
           let editor = model.editor;
           let globals = globals;
           let statics = model.statics;
+          let dynamics = dynamics;
         });
       Deco.editor(model.editor.state.zipper, selected);
     };
     let projectors =
       ProjectorView.all(
         model.editor.state.zipper,
+        ~globals,
         ~cached_statics=model.statics,
         ~cached_syntax=model.editor.syntax,
         ~inject=x => inject(Perform(x)),
-        ~font_metrics=globals.font_metrics,
+        ~dynamics,
       );
     let overlays = edit_decos @ overlays @ [projectors];
     let code_view =
-      CodeWithStatics.View.view(~globals, ~overlays, ~sort?, model);
+      CodeWithStatics.View.view(
+        ~globals,
+        ~overlays,
+        ~dynamics,
+        ~sort?,
+        model,
+      );
     let mousedown_overlay =
       selected && globals.mousedown
         ? [mousedown_overlay(~globals, ~inject=x => inject(Perform(x)))]
diff --git a/src/haz3lweb/app/editors/code/CodeViewable.re b/src/haz3lweb/app/editors/code/CodeViewable.re
index ab789bdce0..675d13e0a5 100644
--- a/src/haz3lweb/app/editors/code/CodeViewable.re
+++ b/src/haz3lweb/app/editors/code/CodeViewable.re
@@ -12,14 +12,14 @@ let view =
       ~buffer_ids,
       ~segment,
       ~holes,
-      ~info_map,
+      ~token_of_proj,
     )
     : Node.t => {
   module Text =
     Code.Text({
       let map = measured;
       let settings = globals.settings;
-      let info_map = info_map;
+      let token_of_proj = token_of_proj;
     });
   let code = Text.of_segment(buffer_ids, false, sort, segment);
   let holes = List.map(Code.of_hole(~measured, ~globals), holes);
@@ -51,21 +51,32 @@ let view =
 // };
 
 let view_segment =
-    (~globals: Globals.t, ~sort: Sort.t, ~info_map, segment: Segment.t) => {
-  let measured = Measured.of_segment(segment, info_map);
+    (~globals: Globals.t, ~sort: Sort.t, ~token_of_proj, segment: Segment.t) => {
+  let measured = Measured.of_segment(segment, token_of_proj);
   let buffer_ids = [];
   let holes = Segment.holes(segment);
-  view(~globals, ~sort, ~measured, ~buffer_ids, ~holes, ~segment, ~info_map);
+  view(
+    ~globals,
+    ~sort,
+    ~measured,
+    ~buffer_ids,
+    ~holes,
+    ~segment,
+    ~token_of_proj,
+  );
 };
 
-let view_exp = (~globals: Globals.t, ~settings, exp: Exp.t) => {
+let view_exp =
+    (~dynamics, ~globals: Globals.t, ~settings, ~info_map, exp: Exp.t) => {
+  let token_of_proj = Projector.token_of_proj(info_map, dynamics);
   exp
   |> ExpToSegment.exp_to_segment(~settings)
-  |> view_segment(~globals, ~sort=Exp);
+  |> view_segment(~token_of_proj, ~globals, ~sort=Exp);
 };
 
-let view_typ = (~globals: Globals.t, ~settings, typ: Typ.t) => {
+let view_typ = (~globals: Globals.t, ~settings, ~info_map, typ: Typ.t) => {
+  let token_of_proj = Projector.token_of_proj(info_map, Dynamics.Map.empty);
   typ
   |> ExpToSegment.typ_to_segment(~settings)
-  |> view_segment(~globals, ~sort=Typ);
+  |> view_segment(~token_of_proj, ~globals, ~sort=Typ);
 };
diff --git a/src/haz3lweb/app/editors/code/CodeWithStatics.re b/src/haz3lweb/app/editors/code/CodeWithStatics.re
index 6e017081f7..a6bb65a7ad 100644
--- a/src/haz3lweb/app/editors/code/CodeWithStatics.re
+++ b/src/haz3lweb/app/editors/code/CodeWithStatics.re
@@ -55,11 +55,23 @@ module Update = {
 
   /* Calculates the statics for the editor. */
   let calculate =
-      (~settings, ~is_edited, ~stitch, {editor, statics: _}: Model.t)
+      (
+        ~settings,
+        ~is_edited,
+        ~stitch,
+        ~dynamics: Dynamics.Map.t,
+        {editor, statics: _}: Model.t,
+      )
       : Model.t => {
     let statics = CachedStatics.init(~settings, ~stitch, editor.state.zipper);
     let editor =
-      Editor.Update.calculate(~settings, ~is_edited, statics, editor);
+      Editor.Update.calculate(
+        ~settings,
+        ~is_edited,
+        statics,
+        dynamics,
+        editor,
+      );
     {editor, statics};
   };
 };
@@ -69,7 +81,13 @@ module View = {
   type event;
 
   let view =
-      (~globals, ~overlays: list(Node.t)=[], ~sort=Sort.root, model: Model.t) => {
+      (
+        ~globals,
+        ~overlays: list(Node.t)=[],
+        ~sort=Sort.root,
+        ~dynamics: Dynamics.Map.t,
+        model: Model.t,
+      ) => {
     let {
       statics: {info_map, _},
       editor:
@@ -80,6 +98,7 @@ module View = {
         },
       _,
     }: Model.t = model;
+    let token_of_proj = Projector.token_of_proj(info_map, dynamics);
     let code_text_view =
       CodeViewable.view(
         ~globals,
@@ -88,7 +107,7 @@ module View = {
         ~buffer_ids=Selection.is_buffer(z.selection) ? selection_ids : [],
         ~segment,
         ~holes,
-        ~info_map,
+        ~token_of_proj,
       );
     let statics_decos = {
       module Deco =
@@ -96,6 +115,7 @@ module View = {
           let globals = globals;
           let editor = model.editor;
           let statics = model.statics;
+          let dynamics = dynamics;
         });
       Deco.statics();
     };
diff --git a/src/haz3lweb/app/editors/decoration/BackpackView.re b/src/haz3lweb/app/editors/decoration/BackpackView.re
index 1e8c93985e..5ab468e0bf 100644
--- a/src/haz3lweb/app/editors/decoration/BackpackView.re
+++ b/src/haz3lweb/app/editors/decoration/BackpackView.re
@@ -3,15 +3,16 @@ open Node;
 open Haz3lcore;
 open Util;
 
-/* Assume this doesn't contain projectors */
-let measured_of = seg => Measured.of_segment(seg, Id.Map.empty);
+let token_of_proj = _ => ""; /* Assume this doesn't contain projectors */
+
+let measured_of = seg => Measured.of_segment(seg, token_of_proj);
 
 let text_view = (seg: Segment.t): list(Node.t) => {
   module Text =
     Code.Text({
       let map = measured_of(seg);
       let settings = Settings.Model.init;
-      let info_map = Id.Map.empty; /* Assume this doesn't contain projectors */
+      let token_of_proj = token_of_proj;
     });
   Text.of_segment([], true, Any, seg);
 };
diff --git a/src/haz3lweb/app/editors/decoration/Deco.re b/src/haz3lweb/app/editors/decoration/Deco.re
index 7512696ed7..014d6d6f2f 100644
--- a/src/haz3lweb/app/editors/decoration/Deco.re
+++ b/src/haz3lweb/app/editors/decoration/Deco.re
@@ -65,6 +65,7 @@ module HighlightSegment =
          M: {
            let measured: Measured.t;
            let info_map: Statics.Map.t;
+           let dynamics: Dynamics.Map.t;
            let font_metrics: FontMetrics.t;
          },
        ) => {
@@ -121,8 +122,7 @@ module HighlightSegment =
     switch (Measured.find_pr_opt(p, M.measured)) {
     | None => failwith("Deco.of_projector: missing measurement")
     | Some(_m) =>
-      let ci = Id.Map.find_opt(p.id, M.info_map);
-      let token = Projector.placeholder(p, ci);
+      let token = Projector.token_of_proj(M.info_map, M.dynamics, p);
       /* Handling this internal to ProjectorsView at the moment because the
        * commented-out strategy doesn't work well, since the inserted str8-
        * edged lines vertical edge placement doesn't account for whether
@@ -182,6 +182,7 @@ module Deco =
            let globals: Globals.t;
            let editor: Editor.t;
            let statics: CachedStatics.t;
+           let dynamics: Dynamics.Map.t;
          },
        ) => {
   let font_metrics = M.globals.font_metrics;
@@ -218,6 +219,7 @@ module Deco =
     HighlightSegment({
       let measured = M.editor.syntax.measured;
       let info_map = M.statics.info_map;
+      let dynamics = M.dynamics;
       let font_metrics = font_metrics;
     });
 
diff --git a/src/haz3lweb/app/editors/result/EvalResult.re b/src/haz3lweb/app/editors/result/EvalResult.re
index 81f0a04fd2..840f2b0961 100644
--- a/src/haz3lweb/app/editors/result/EvalResult.re
+++ b/src/haz3lweb/app/editors/result/EvalResult.re
@@ -1,4 +1,5 @@
 open Util;
+open Haz3lcore;
 
 /* The result box at the bottom of a cell. This is either the TestResutls
    kind where only a summary of test results is shown, or the EvalResults kind
@@ -37,7 +38,8 @@ module Model = {
   type t = {
     kind,
     result,
-    previous_tests: option(Haz3lcore.TestResults.t) // Stops test results from being cleared on update
+    previous_tests: option(Haz3lcore.TestResults.t), // Stops test results from being cleared on update
+    previous_probes: option(Dynamics.Probe.Map.t),
   };
 
   let make_test_report = (model: t): option(Haz3lcore.TestResults.t) =>
@@ -60,7 +62,12 @@ module Model = {
     | NoElab => None
     };
 
-  let init = {kind: Evaluation, result: NoElab, previous_tests: None};
+  let init = {
+    kind: Evaluation,
+    result: NoElab,
+    previous_tests: None,
+    previous_probes: None,
+  };
 
   let test_results = (model: t): option(Haz3lcore.TestResults.t) =>
     switch (model.result) {
@@ -82,6 +89,27 @@ module Model = {
     | NoElab => model.previous_tests
     };
 
+  let probe_results = (model: t): option(Dynamics.Probe.Map.t) =>
+    switch (model.result) {
+    | Evaluation({result: OldValue(ResultOk((_, state))), _})
+    | Evaluation({result: NewValue(ResultOk((_, state))), _}) =>
+      Some(Haz3lcore.EvaluatorState.get_probes(state))
+    | Stepper(s) =>
+      Some(
+        s.history
+        |> StepperView.Model.get_state
+        |> Haz3lcore.EvaluatorState.get_probes,
+      )
+    | Evaluation(_)
+    | NoElab => model.previous_probes
+    };
+
+  let dynamics = (model: t): Dynamics.Map.t =>
+    switch (probe_results(model)) {
+    | Some(result) => Dynamics.Map.mk(result)
+    | None => Dynamics.Map.mk(Dynamics.Probe.Map.empty)
+    };
+
   let get_elaboration = (model: t): option(Haz3lcore.Exp.t) =>
     switch (model.result) {
     | Evaluation({elab, _}) => Some(elab)
@@ -161,7 +189,13 @@ module Update = {
             cached_settings,
           }),
       }
-      |> (x => {...x, previous_tests: Model.test_results(x)})
+      |> (
+        x => {
+          ...x,
+          previous_tests: Model.test_results(x),
+          previous_probes: Model.probe_results(x),
+        }
+      )
       |> Updated.return
     | (UpdateResult(_), _) => model |> Updated.return_quiet
     };
@@ -265,6 +299,7 @@ module Update = {
                ~settings,
                ~stitch=_ => exp,
                ~is_edited,
+               ~dynamics=Dynamics.Map.empty, // Dynamics unneeded here
                editor,
              )
              |> (x => (exp, x))
@@ -377,6 +412,7 @@ module View = {
         ~globals,
         ~selected,
         ~sort=Haz3lcore.Sort.root,
+        ~dynamics=Dynamics.Map.empty, //This is just the result display
         editor,
       );
     let exn_view =
@@ -536,6 +572,11 @@ module View = {
         text("Evaluation disabled, showing elaboration:"),
         switch (Model.get_elaboration(model)) {
         | Some(elab) =>
+          let token_of_proj =
+            Projector.token_of_proj(
+              Statics.Map.empty,
+              Model.dynamics(model),
+            );
           elab
           |> Haz3lcore.ExpToSegment.(
                exp_to_segment(
@@ -543,11 +584,7 @@ module View = {
                    Settings.of_core(~inline=false, globals.settings.core),
                )
              )
-          |> CodeViewable.view_segment(
-               ~globals,
-               ~sort=Exp,
-               ~info_map=Haz3lcore.Id.Map.empty,
-             )
+          |> CodeViewable.view_segment(~globals, ~sort=Exp, ~token_of_proj);
         | None => text("No elaboration found")
         },
       ];
diff --git a/src/haz3lweb/app/editors/result/StepperEditor.re b/src/haz3lweb/app/editors/result/StepperEditor.re
index 7e3ba6e5c1..578458d645 100644
--- a/src/haz3lweb/app/editors/result/StepperEditor.re
+++ b/src/haz3lweb/app/editors/result/StepperEditor.re
@@ -35,11 +35,18 @@ module Update = {
         ~settings,
         ~is_edited,
         ~stitch,
+        ~dynamics: Dynamics.Map.t,
         {editor, taken_steps, next_steps}: Model.t,
       )
       : Model.t => {
     let editor =
-      CodeSelectable.Update.calculate(~settings, ~is_edited, ~stitch, editor);
+      CodeSelectable.Update.calculate(
+        ~settings,
+        ~is_edited,
+        ~stitch,
+        ~dynamics,
+        editor,
+      );
     {editor, taken_steps, next_steps};
   };
 };
@@ -64,6 +71,7 @@ module View = {
         ~signal: event => 'a,
         ~overlays=[],
         ~selected,
+        ~dynamics: Dynamics.Map.t,
         model: Model.t,
       ) => {
     let overlays = {
@@ -72,6 +80,7 @@ module View = {
           let editor = model.editor.editor;
           let globals = globals;
           let statics = model.editor.statics;
+          let dynamics = dynamics;
         });
       overlays
       @ Deco.taken_steps(model.taken_steps)
@@ -84,6 +93,7 @@ module View = {
       ~selected,
       ~globals,
       ~overlays,
+      ~dynamics,
       model.editor,
     );
   };
diff --git a/src/haz3lweb/app/explainthis/ExplainThis.re b/src/haz3lweb/app/explainthis/ExplainThis.re
index 8a499ee881..dcf2ab0c21 100644
--- a/src/haz3lweb/app/explainthis/ExplainThis.re
+++ b/src/haz3lweb/app/explainthis/ExplainThis.re
@@ -236,6 +236,7 @@ let expander_deco =
       let editor = editor;
       let globals = globals;
       let statics = CachedStatics.empty;
+      let dynamics = Dynamics.Map.empty;
     });
   switch (doc.expandable_id, List.length(options)) {
   | (None, _)
@@ -277,7 +278,7 @@ let expander_deco =
                   CodeViewable.view_segment(
                     ~globals,
                     ~sort=Exp,
-                    ~info_map=Id.Map.empty,
+                    ~token_of_proj=_ => "", // Assume no projectors
                     segment,
                   );
                 let classes =
@@ -411,7 +412,7 @@ let rec bypass_parens_pat = (pat: Pat.t) => {
 
 let rec bypass_parens_exp = (exp: Exp.t) => {
   switch (exp.term) {
-  | Parens(e) => bypass_parens_exp(e)
+  | Parens(e, _) => bypass_parens_exp(e)
   | _ => exp
   };
 };
@@ -496,12 +497,14 @@ let get_doc =
           editor,
         );
       let statics = CachedStatics.empty;
+      let dynamics = Dynamics.Map.empty;
       let highlight_deco = {
         module Deco =
           Deco.Deco({
             let editor = editor;
             let globals = {...globals, color_highlights: highlights};
             let statics = statics;
+            let dynamics = dynamics;
           });
         [Deco.color_highlights()];
       };
@@ -509,6 +512,7 @@ let get_doc =
         CodeWithStatics.View.view(
           ~globals,
           ~overlays=highlight_deco @ [expander_deco],
+          ~dynamics,
           ~sort,
           {editor, statics},
         );
@@ -1761,7 +1765,7 @@ let get_doc =
             ),
           TestExp.tests,
         );
-      | Parens(term) => get_message_exp(term.term) // No Special message?
+      | Parens(term, _) => get_message_exp(term.term) // No Special message?
       | Cons(hd, tl) =>
         let hd_id = List.nth(hd.ids, 0);
         let tl_id = List.nth(tl.ids, 0);
diff --git a/src/haz3lweb/app/inspector/ProjectorPanel.re b/src/haz3lweb/app/inspector/ProjectorPanel.re
index 6a19da402c..271363b4fe 100644
--- a/src/haz3lweb/app/inspector/ProjectorPanel.re
+++ b/src/haz3lweb/app/inspector/ProjectorPanel.re
@@ -5,12 +5,7 @@ open Projector;
 open Util.OptUtil.Syntax;
 open Util.Web;
 
-/* The projector selection panel on the right of the bottom bar */
-let option_view = (name, n) =>
-  option(
-    ~attrs=n == name ? [Attr.create("selected", "selected")] : [],
-    [text(n)],
-  );
+// The projector selection panel on the right of the bottom bar
 
 /* Decide which projectors are applicable based on the cursor info.
  * This is slightly inside-out as elsewhere it depends on the underlying
@@ -35,8 +30,8 @@ let applicable_projectors: option(Info.t) => list(Base.kind) =
     @ [Base.Fold]
     @ (
       switch (ci) {
-      | InfoExp(_)
-      | InfoPat(_) => [(Info: Base.kind)]
+      | InfoExp(_) => [Info, Probe]
+      | InfoPat(_) => [Info]
       | _ => []
       }
     );
@@ -75,14 +70,14 @@ let toggle_view =
 
 let kind = (editor: option(Editor.t)) => {
   let* editor = editor;
-  let+ (_, p) = Editor.Model.indicated_projector(editor);
+  let+ (_, p) = Indicated.projector(editor.state.zipper);
   p.kind;
 };
 
 let id = (editor: option(Editor.t)) => {
   {
     let* editor = editor;
-    let+ (id, _) = Editor.Model.indicated_projector(editor);
+    let+ (id, _) = Indicated.projector(editor.state.zipper);
     id;
   }
   |> Option.value(~default=Id.invalid);
@@ -100,38 +95,56 @@ let might_project: Cursor.cursor(Editors.Update.t) => bool =
       }
     };
 
-let currently_selected = editor =>
-  option_view(
-    switch (kind(editor)) {
-    | None => "Fold"
-    | Some(k) => ProjectorView.name(k)
-    },
+let lift = (str, strs) => List.cons(str, List.filter((!=)(str), strs));
+
+/* The string names of all projectors applicable to the currently
+ * indicated syntax, with the currently applied projection (if any)
+ * lifted to the top of the list */
+let applicable_projector_strings = (cursor: Cursor.cursor(Editors.Update.t)) => {
+  let strs =
+    applicable_projectors(cursor.info) |> List.map(ProjectorView.name);
+  switch (kind(cursor.editor)) {
+  | None => strs
+  | Some(k) => lift(ProjectorView.name(k), strs)
+  };
+};
+
+/* A selection input for contetually applicable projectors */
+let select_view =
+    (
+      ~inject: Action.project => Ui_effect.t(unit),
+      cursor: Cursor.cursor(Editors.Update.t),
+    ) => {
+  let applicable_projector_strings =
+    might_project(cursor) ? applicable_projector_strings(cursor) : [];
+  let value =
+    switch (applicable_projector_strings) {
+    | [] => ""
+    | [hd, ..._] => hd
+    };
+  Node.select(
+    ~attrs=[
+      Attr.on_change((_, name) =>
+        inject(SetIndicated(ProjectorView.of_name(name)))
+      ),
+      Attr.string_property("value", value),
+    ],
+    applicable_projector_strings |> List.map(n => option([text(n)])),
+  );
+};
+
+let toggle_view = (~inject, cursor: Cursor.cursor(Editors.Update.t)) =>
+  toggle_view(
+    ~inject,
+    cursor.info,
+    id(cursor.editor),
+    kind(cursor.editor) != None,
+    might_project(cursor),
   );
 
 let view = (~inject, cursor: Cursor.cursor(Editors.Update.t)) => {
-  let applicable_projectors = applicable_projectors(cursor.info);
-  let should_show = might_project(cursor) && applicable_projectors != [];
-  let select_view =
-    Node.select(
-      ~attrs=[
-        Attr.on_change((_, name) =>
-          inject(Action.SetIndicated(ProjectorView.of_name(name)))
-        ),
-      ],
-      (might_project(cursor) ? applicable_projectors : [])
-      |> List.map(ProjectorView.name)
-      |> List.map(currently_selected(cursor.editor)),
-    );
-  let toggle_view =
-    toggle_view(
-      ~inject,
-      cursor.info,
-      id(cursor.editor),
-      kind(cursor.editor) != None,
-      might_project(cursor),
-    );
   div(
     ~attrs=[Attr.id("projectors")],
-    (should_show ? [select_view] : []) @ [toggle_view],
+    [select_view(~inject, cursor)] @ [toggle_view(~inject, cursor)],
   );
 };
diff --git a/src/haz3lweb/exercises/SyntaxTest.re b/src/haz3lweb/exercises/SyntaxTest.re
index 23dff72251..bd8622fb09 100644
--- a/src/haz3lweb/exercises/SyntaxTest.re
+++ b/src/haz3lweb/exercises/SyntaxTest.re
@@ -47,9 +47,9 @@ let rec find_in_let =
         (name: string, upat: UPat.t, def: UExp.t, l: list(UExp.t))
         : list(UExp.t) => {
   switch (upat.term, def.term) {
-  | (Parens(up), Parens(ue)) => find_in_let(name, up, ue, l)
+  | (Parens(up), Parens(ue, _)) => find_in_let(name, up, ue, l)
   | (Parens(up), _) => find_in_let(name, up, def, l)
-  | (_, Parens(ue)) => find_in_let(name, upat, ue, l)
+  | (_, Parens(ue, _)) => find_in_let(name, upat, ue, l)
   | (Cast(up, _, _), _) => find_in_let(name, up, def, l)
   | (Var(x), Fun(_)) => x == name ? [def, ...l] : l
   | (Tuple(pl), Tuple(ul)) =>
@@ -92,7 +92,7 @@ let rec find_fn =
   | FixF(_, body, _)
   | Fun(_, body, _, _) => l |> find_fn(name, body)
   | TypAp(u1, _)
-  | Parens(u1)
+  | Parens(u1, _)
   | Cast(u1, _, _)
   | UnOp(_, u1)
   | TyAlias(_, _, u1)
@@ -191,7 +191,7 @@ let rec var_mention = (name: string, uexp: Exp.t): bool => {
   | TypFun(_, u, _)
   | TypAp(u, _)
   | Test(u)
-  | Parens(u)
+  | Parens(u, _)
   | UnOp(_, u)
   | TyAlias(_, _, u)
   | Filter(_, u) => var_mention(name, u)
@@ -252,7 +252,7 @@ let rec var_applied = (name: string, uexp: Exp.t): bool => {
       ? false : var_applied(name, def) || var_applied(name, body)
   | TypFun(_, u, _)
   | Test(u)
-  | Parens(u)
+  | Parens(u, _)
   | UnOp(_, u)
   | TyAlias(_, _, u)
   | Filter(_, u) => var_applied(name, u)
@@ -350,7 +350,7 @@ let rec tail_check = (name: string, uexp: Exp.t): bool => {
   | Closure(_, u)
   | TypFun(_, u, _)
   | TypAp(u, _)
-  | Parens(u) => tail_check(name, u)
+  | Parens(u, _) => tail_check(name, u)
   | UnOp(_, u) => !var_mention(name, u)
   | Ap(_, u1, u2) => var_mention(name, u2) ? false : tail_check(name, u1)
   | DeferredAp(fn, args) =>
diff --git a/src/haz3lweb/view/ExerciseMode.re b/src/haz3lweb/view/ExerciseMode.re
index d8bc55fafa..7787cdd666 100644
--- a/src/haz3lweb/view/ExerciseMode.re
+++ b/src/haz3lweb/view/ExerciseMode.re
@@ -193,7 +193,9 @@ module Update = {
        one of the editors is shown in two cells, so we arbitrarily choose which
        statics to take */
     let editors: Exercise.p('a) = {
-      let calculate = Editor.Update.calculate(~settings, ~is_edited);
+      let calculate = (statics, dynamics, ed) =>
+        Editor.Update.calculate(~settings, statics, dynamics, ~is_edited, ed);
+
       {
         title: model.editors.title,
         version: model.editors.version,
@@ -201,29 +203,44 @@ module Update = {
         prompt: model.editors.prompt,
         point_distribution: model.editors.point_distribution,
         prelude:
-          calculate(cells.prelude.editor.statics, model.editors.prelude),
+          calculate(
+            cells.prelude.editor.statics,
+            EvalResult.Model.dynamics(cells.prelude.result),
+            model.editors.prelude,
+          ),
         correct_impl:
           calculate(
             cells.test_validation.editor.statics,
+            EvalResult.Model.dynamics(cells.test_validation.result),
             model.editors.correct_impl,
           ),
         your_tests: {
           tests:
             calculate(
               cells.user_tests.editor.statics,
+              EvalResult.Model.dynamics(cells.user_tests.result),
               model.editors.your_tests.tests,
             ),
           required: model.editors.your_tests.required,
           provided: model.editors.your_tests.provided,
         },
         your_impl:
-          calculate(cells.user_impl.editor.statics, model.editors.your_impl),
+          calculate(
+            cells.user_impl.editor.statics,
+            EvalResult.Model.dynamics(cells.user_impl.result),
+            model.editors.your_impl,
+          ),
         hidden_bugs:
           List.map2(
             (cell: CellEditor.Model.t, editor: Exercise.wrong_impl('a)):
               Exercise.wrong_impl('a) =>
               {
-                impl: calculate(cell.editor.statics, editor.impl),
+                impl:
+                  calculate(
+                    cell.editor.statics,
+                    EvalResult.Model.dynamics(cell.result),
+                    editor.impl,
+                  ),
                 hint: editor.hint,
               },
             cells.hidden_bugs,
@@ -233,6 +250,7 @@ module Update = {
           tests:
             calculate(
               cells.hidden_tests.editor.statics,
+              EvalResult.Model.dynamics(cells.hidden_tests.result),
               model.editors.hidden_tests.tests,
             ),
           hints: model.editors.hidden_tests.hints,
diff --git a/src/haz3lweb/view/StepperView.re b/src/haz3lweb/view/StepperView.re
index 58077dd55c..2706f3159b 100644
--- a/src/haz3lweb/view/StepperView.re
+++ b/src/haz3lweb/view/StepperView.re
@@ -266,6 +266,7 @@ module Update = {
                 CodeSelectable.Update.calculate(
                   ~settings=settings |> Calc.get_value,
                   ~is_edited=false,
+                  ~dynamics=Dynamics.Map.empty, // No projectors in stepper atm
                   ~stitch=x =>
                   x
                 ),
@@ -483,6 +484,7 @@ module View = {
                               (),
                             ),
                           ),
+                     ~dynamics=Dynamics.Map.empty,
                      ~inject=
                        (x: StepperEditor.Update.t) =>
                          inject(StepperEditor(i + 1, x)),
@@ -552,6 +554,7 @@ module View = {
                 ~inject=
                   (x: StepperEditor.Update.t) =>
                     inject(StepperEditor(current_n, x)),
+                ~dynamics=Dynamics.Map.empty,
                 ~signal=
                   fun
                   | TakeStep(x) =>
diff --git a/src/haz3lweb/www/style.css b/src/haz3lweb/www/style.css
index d70e70a422..e38e08bfab 100644
--- a/src/haz3lweb/www/style.css
+++ b/src/haz3lweb/www/style.css
@@ -3,11 +3,10 @@
 @import "style/animations.css";
 @import "style/loading.css";
 @import "style/editor.css";
-@import "style/projectors.css";
+@import "style/projectors/base.css";
 @import "style/nut-menu.css";
 @import "style/cursor-inspector.css";
 @import "style/type-display.css";
-@import "style/projectors-panel.css";
 @import "style/explainthis.css";
 @import "style/exercise-mode.css";
 @import "style/cell.css";
diff --git a/src/haz3lweb/www/style/editor.css b/src/haz3lweb/www/style/editor.css
index 13ac029688..767fa6196e 100644
--- a/src/haz3lweb/www/style/editor.css
+++ b/src/haz3lweb/www/style/editor.css
@@ -20,9 +20,12 @@
 
 /* This is a hack to compensating for default linebreak handling
 * preventing a trailing linebreak in code editors from leaving a
-* trailing blank line, as per https://stackoverflow.com/questions/43492826/ */
+* trailing blank line, as per https://stackoverflow.com/questions/43492826/.
+* The mysterious chracter below is a zero-width space, used here
+* to avoid inserting an extraneous whitespace context for inline
+* syntax views, e.g. type views in the cursor inspector */
 .code-text:after {
-  content: " ";
+  content: "​";
 }
 
 /* TOKEN COLORS */
diff --git a/src/haz3lweb/www/style/projectors.css b/src/haz3lweb/www/style/projectors/base.css
similarity index 98%
rename from src/haz3lweb/www/style/projectors.css
rename to src/haz3lweb/www/style/projectors/base.css
index 8d187f01a0..49735cd2b5 100644
--- a/src/haz3lweb/www/style/projectors.css
+++ b/src/haz3lweb/www/style/projectors/base.css
@@ -1,5 +1,8 @@
 /* PROJECTORS */
 
+@import "panel.css";
+@import "probe.css";
+
 /* Turn off caret when a block projector is focused */
 #caret:has(~ .projectors .projector.block *:focus) {
   display: none;
@@ -14,27 +17,34 @@
   align-items: center;
   color: var(--BR2);
 }
+
 .projector > *:not(svg) {
   z-index: var(--projector-z);
 }
+
 .projector > svg {
   z-index: var(--projector-backing-z);
   fill: var(--shard_projector);
 }
+
 .projector.block > svg {
   stroke-width: 0.5px;
   stroke: var(--BR2);
 }
+
 .projector.indicated > svg {
   fill: var(--shard-caret-exp);
 }
+
 .projector > svg > path {
   vector-effect: non-scaling-stroke;
 }
+
 .projector.block.selected > svg > path {
   vector-effect: non-scaling-stroke;
   stroke: var(--Y3);
 }
+
 .projector.selected > svg,
 .projector.selected.indicated > svg,
 .projector.block.selected.indicated > svg {
@@ -168,3 +178,4 @@
   color: var(--BLACK);
   background-color: var(--shard-selected);
 }
+
diff --git a/src/haz3lweb/www/style/projectors-panel.css b/src/haz3lweb/www/style/projectors/panel.css
similarity index 100%
rename from src/haz3lweb/www/style/projectors-panel.css
rename to src/haz3lweb/www/style/projectors/panel.css
diff --git a/src/haz3lweb/www/style/projectors/probe.css b/src/haz3lweb/www/style/projectors/probe.css
new file mode 100644
index 0000000000..60e747dc38
--- /dev/null
+++ b/src/haz3lweb/www/style/projectors/probe.css
@@ -0,0 +1,136 @@
+/* Probe Projector */
+
+.projector.probe {
+  font-family: var(--code-font);
+  font-size: var(--base-font-size);
+  color: var(--STONE);
+}
+
+.projector.probe > svg {
+  fill: #c7e6c6;
+  filter: drop-shadow(0.7px 0.7px 0px green);
+}
+
+.projector.probe .main {
+  display: flex;
+  flex-direction: row;
+  gap: 0.4em;
+  cursor: pointer;
+  align-items: center;
+}
+
+@keyframes rotate {
+  to {
+    transform: rotate(360deg);
+  }
+}
+.projector.probe .live-offside:empty + * .icon {
+  animation: rotate 5s linear infinite;
+}
+
+.projector.probe .num-closures {
+  position: absolute;
+  right: -0.5em;
+  top: -0.3em;
+  transform-origin: top right;
+  scale: 0.6;
+  color: oklch(1 0 0);
+  font-family: var(--ui-font);
+  display: flex;
+  justify-content: center;
+  background-color: var(--G0);
+  border-radius: 2em;
+  font-size: 0.7em;
+  padding: 0.3em;
+  min-width: 1em;
+  z-index: var(--code-emblems-z);
+}
+.projector.probe.selected .num-closures {
+  background-color: var(--Y1);
+}
+
+.projector.probe .live-offside {
+  display: flex;
+  flex-direction: row;
+  position: absolute;
+  left: 10em;
+  gap: 0.15em;
+}
+
+.projector.probe .live-offside:empty {
+  display: none;
+}
+
+.projector.probe .closure:hover .live-env:empty {
+  display: none;
+}
+
+.projector.probe .val-resize {
+  cursor: pointer;
+}
+
+.projector.probe .val-resize .code-text {
+  background-color: #c7e6c6; /* TODO(andrew) */
+  border-radius: 0.4em 0.1em 0.1em 0.1em;
+  filter: drop-shadow(0.7px 0.7px 0px green);
+}
+.projector.probe .closure:first-child .val-resize:hover .code-text {
+  cursor: col-resize;
+}
+.projector.probe .val-resize.cursor .code-text {
+  outline: 1.6px solid var(--G0);
+  outline-style: dotted;
+  filter: none;
+  opacity: 100%;
+}
+
+.projector.probe .val-resize .code-text {
+  opacity: 40%;
+}
+.projector.probe .val-resize:not(.cursor) .code-text .token {
+  filter: saturate(0);
+}
+
+.projector.probe .live-env {
+  background-color: var(--T3);
+  border-radius: 0 0.2em 0.2em 0.2em;
+  padding: 0.2em;
+  display: none;
+  position: absolute;
+  top: 1.5em;
+  z-index: var(--code-hovers-z);
+}
+
+.projector.probe .live-env .live-env-entry {
+  display: flex;
+  flex-direction: row;
+  gap: 0.3em;
+  align-items: baseline;
+  color: var(--GB0);
+}
+
+.projector.probe.indicated > svg {
+  fill: var(--G0);
+}
+
+.projector.probe.indicated .val-resize .code-text {
+  opacity: 60%;
+}
+
+.projector.probe.indicated .main {
+  color: white;
+}
+
+.projector.probe.indicated .val-resize.cursor .code-text {
+  opacity: 100%;
+  /* outline: 1px solid var(--GB1); */
+  outline: 2.8px solid oklch(0.7 0.15 150.31);
+}
+
+.projector.probe.indicated .closure:hover .live-env {
+  display: block;
+}
+
+.projector.probe.indicated .closure.cursor .live-env:empty {
+  display: none;
+}
diff --git a/src/haz3lweb/www/style/variables.css b/src/haz3lweb/www/style/variables.css
index 143829787d..8859a25eab 100644
--- a/src/haz3lweb/www/style/variables.css
+++ b/src/haz3lweb/www/style/variables.css
@@ -209,8 +209,10 @@
 
   /* ABOVE CODE LEVEL */
   --backpack-targets-z: 11;
+  --code-hovers-z: 11;
   --stepper-interactive-z: 15;
   --caret-z: 20;
+  --code-emblems-z: 21;
 
   /* TOP LEVEL UI */
   --context-inspector-z: 29; /* keep below bottom bar */
diff --git a/src/util/JsUtil.re b/src/util/JsUtil.re
index 36890d518d..e84c34b69e 100644
--- a/src/util/JsUtil.re
+++ b/src/util/JsUtil.re
@@ -190,3 +190,22 @@ module Fragment = {
     Url.Current.get() |> Option.map(fragment_of_url);
   };
 };
+
+let setPointerCapture = (e: Js.t(Dom_html.element), pointerId: int) =>
+  Js.Unsafe.meth_call(
+    e,
+    "setPointerCapture",
+    [|Js.Unsafe.inject(pointerId)|],
+  );
+
+let releasePointerCapture = (e: Js.t(Dom_html.element), pointerId: int) =>
+  Js.Unsafe.meth_call(
+    e,
+    "releasePointerCapture",
+    [|Js.Unsafe.inject(pointerId)|],
+  );
+
+// TODO: Figure out why this doesn't work
+// let on_pointermove =
+//     (handler: Js.t(Dom_html.pointerEvent) => Effect.t(unit)): Attr.t =>
+//   Virtual_dom.Vdom.Attr.property("onpointermove", Js.Unsafe.inject(handler));
diff --git a/src/util/ListUtil.re b/src/util/ListUtil.re
index 1e7e87a1af..300d280b3b 100644
--- a/src/util/ListUtil.re
+++ b/src/util/ListUtil.re
@@ -591,3 +591,16 @@ let minimum = (f: 'a => int, xs: list('a)): option('a) =>
       };
     loop(x, f(x), xs);
   };
+
+/* Given two lists, return their maximum common suffix */
+let max_common_suffix = (a: list('a), b: list('a)): list('a) => {
+  let rec loop = (a, b, acc) =>
+    switch (a, b) {
+    | ([], _)
+    | (_, []) => acc
+    | ([ha, ...ta], [hb, ...tb]) when ha == hb =>
+      loop(ta, tb, [ha, ...acc])
+    | _ => acc
+    };
+  loop(List.rev(a), List.rev(b), []);
+};
diff --git a/test/Test_Elaboration.re b/test/Test_Elaboration.re
index c515487535..c317ce3cb8 100644
--- a/test/Test_Elaboration.re
+++ b/test/Test_Elaboration.re
@@ -20,7 +20,7 @@ let empty_hole = () => alco_check("Empty hole", u2, dhexp_of_uexp(u2));
 
 let u3: Exp.t = {
   ids: [id_at(0)],
-  term: Parens({ids: [id_at(1)], term: Var("y"), copied: false}),
+  term: Parens({ids: [id_at(1)], term: Var("y"), copied: false}, Paren),
   copied: false,
 };
 
diff --git a/test/Test_MakeTerm.re b/test/Test_MakeTerm.re
index 46818664a9..84bd02ab6c 100644
--- a/test/Test_MakeTerm.re
+++ b/test/Test_MakeTerm.re
@@ -23,7 +23,7 @@ let tests = [
     exp_check(Var("x") |> Exp.fresh, "x")
   }),
   test_case("Parenthesized Expression", `Quick, () => {
-    exp_check(Parens(Int(0) |> Exp.fresh) |> Exp.fresh, "(0)")
+    exp_check(Parens(Int(0) |> Exp.fresh, Paren) |> Exp.fresh, "(0)")
   }),
   test_case("Let Expression", `Quick, () => {
     exp_check(