anchor.diff:  module DsEnv = FStar.ToSyntax.Env
   module TcEnv = FStar.TypeChecker.Env
   module CTable = FStar.Interactive.CompletionTable
  +
  +exception ExitREPL of int
   
   // A custom version of the function that's in FStar.Universal.fs just for the
   // sake of the interactive mode
  
positive.code:           { qid = q.qid; qq = MissingCurrentModule }
          | _ -> q
  
  let rec go st : unit =
    let query = validate_query st (read_interactive_query st.repl_stdin) in
    let (status, response), state_opt = run_query st query.qq in
    write_response query.qid status response;
    match state_opt with
    | Inl st' -> go st'
    | Inr exitcode -> exit exitcode
  
  let interactive_error_handler = // No printing here — collect everything for future use
    let issues : ref<list<issue>> = Util.mk_ref [] in
  
negative.code: let read_interactive_query stream : query =
    try
      match Util.read_line stream with
      | None -> raise (ExitREPL 0)
      | Some line ->
        match Util.json_of_string line with
        | None -> { qid = "?"; qq = ProtocolViolation "Json parsing failed." }
  