anchor.diff:      with InvalidSearch s -> (QueryNOK, JsonStr s) in
     (results, Inl st)
   
  -let run_query st : query' -> (query_status * json) * either<repl_state,int> = function
  +let run_query st (q: query') : (query_status * json) * either<repl_state, int> =
  +  let wrap r =
  +    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
  -  | Pop -> run_pop st
  -  | Push (kind, text, l, c, peek) -> run_push st kind text l c peek
  -  | AutoComplete (search_term, context) -> run_autocomplete st search_term context
  -  | 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
  -  | MissingCurrentModule -> run_missing_current_module st query
  +  | 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 _ ->
  +      run_generic_error st "Please send a code fragment before running this query"
  +    | FullReplState st ->
  +      wrap
  +       (match q with
  +        | Pop -> run_pop st
  +        | AutoComplete (search_term, context) -> run_autocomplete st search_term context
  +        | 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")
   
   let validate_query st (q: query) : query =
     match q.qq with
  -  | Push (SyntaxCheck, _, _, _, false) ->
  +  | Push { push_kind = SyntaxCheck; push_peek_only = false } ->
       { qid = q.qid; qq = ProtocolViolation "Cannot use 'kind': 'syntax' with 'query': 'push'" }
  -  | _ -> match st.repl_curmod with
  -        | None when query_needs_current_module q.qq ->
  -          { qid = q.qid; qq = MissingCurrentModule }
  +  | _ -> match st with
  +        | FullReplState { repl_curmod = None } when query_needs_current_module q.qq ->
  +          { qid = q.qid; qq = GenericError "Current module unset" }
           | _ -> q
  +
  +let stdin = function
  +  | PartialReplState st -> st.prepl_stdin
  +  | FullReplState st -> st.repl_stdin
   
   let rec go st : int =
     let rec loop st : int =
  -    let query = validate_query st (read_interactive_query st.repl_stdin) in
  +    let query = validate_query st (read_interactive_query (stdin st)) in
       let (status, response), state_opt = run_query st query.qq in
       write_response query.qid status response;
       match state_opt with
  
positive.code: 
  open FStar.Parser.ParseIt
  
  // FIXME: Store repl_names in the stack, too
  type repl_state = { repl_line: int; repl_column: int; repl_fname: string;
                      repl_deps: (deps_stack_t * m_timestamps);
                      repl_curmod: modul_t; repl_env: env_t;
                      repl_stdin: stream_reader; repl_names: CTable.table }
  
  let repl_stack: ref<list<repl_state>> = Util.mk_ref []
  
  let repl_stack_empty () =
    match !repl_stack with
  
negative.code: 
    let exit_code =
      if FStar.Options.record_hints() || FStar.Options.use_hints() then
        FStar.SMTEncoding.Solver.with_hints_db (List.hd (Options.file_list ())) (fun () -> go (FullReplState init_st))
      else
        go (FullReplState init_st) in
    exit exit_code
  
  let interactive_mode (filename:string): unit =
  