anchor.diff:          | Lookup (symbol, context, pos_opt, rq_info) -> run_lookup st symbol context pos_opt rq_info
           | Compute (term, rules) -> run_compute st term rules
           | Search term -> run_search st term
  -        | Exit | DescribeProtocol | DescribeRepl
  -        | GenericError _ | ProtocolViolation _ | Push _ -> failwith "impossible")
  +        | Push pquery when pquery.push_peek_only = true -> run_regular_push st pquery
  +        | Exit | DescribeProtocol | DescribeRepl | GenericError _
  +        | ProtocolViolation _ | Push _ -> failwith "impossible")
   
   let validate_query st (q: query) : query =
     match q.qq with
  
positive.code:     match r with
      | (status, Inr n) -> (status, Inr n)
      | (status, Inl full_st) -> (status, Inl (FullReplState full_st)) in
    // First handle queries that support both partial and full states…
    match q with
    | Exit -> run_exit st
    | DescribeProtocol -> run_describe_protocol st
    | DescribeRepl -> run_describe_repl st
    | GenericError message -> run_generic_error st message
    | ProtocolViolation query -> run_protocol_violation st query
    | Push push_query -> wrap <| run_push st push_query
    | _ -> // … then queries that only work on full states
      match st with
      | PartialReplState _ ->
  
negative.code:        TcEnv.set_tc_hooks tcenv tcenv_old_hooks),
        List.rev !events))
  
  let run_regular_push (st: full_repl_state) query =
    let { push_kind = kind; push_code = text; push_line = line;
          push_column = column; push_peek_only = peek_only } = query in
  
    let env = push_repl kind st in
  
    let env, finish_name_tracking = track_name_changes env in // begin name tracking…
  