anchor.diff:  module TcErr = FStar.TypeChecker.Err
   module TcEnv = FStar.TypeChecker.Env
   module CTable = FStar.Interactive.CompletionTable
  -
  -exception ExitREPL of int
   
   (** Checkpoint the current (typechecking and desugaring) environment **)
   let push env msg =
  
positive.code:           { qid = q.qid; qq = GenericError "Current module unset" }
          | _ -> q
  
  let rec go st : int =
    let rec loop st : int =
      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' -> loop st'
      | Inr exitcode -> raise (ExitREPL exitcode) in
  
    if Options.trace_error () then
      loop st
    else
      try loop st with ExitREPL n -> n
  
  let interactive_error_handler = // No printing here — collect everything for future use
    let issues : ref<list<issue>> = Util.mk_ref [] in
  
negative.code:     eh_report = report;
      eh_clear = clear }
  
  let interactive_printer printer =
    { printer_prinfo = (fun s -> forward_message printer "info" (JsonStr s));
      printer_prwarning = (fun s -> forward_message printer "warning" (JsonStr s));
      printer_prerror = (fun s -> forward_message printer "error" (JsonStr s));
      printer_prgeneric = (fun label get_string get_json ->
                           forward_message printer label (get_json ())) }
  
  let install_ide_mode_hooks () =
    FStar.Util.set_printer interactive_printer;
    FStar.Errors.set_handler interactive_error_handler
  
  let initial_range =
    Range.mk_range "<input>" (Range.mk_pos 1 0) (Range.mk_pos 1 0)
  
  let build_initial_repl_state (filename: string) =
    let env = init_env FStar.Parser.Dep.empty_deps in
    let env = FStar.TypeChecker.Env.set_range env initial_range in
  
    { repl_line = 1; repl_column = 0; repl_fname = filename;
      repl_curmod = None; repl_env = env; repl_deps_stack = [];
      repl_stdin = open_stdin ();
      repl_names = CompletionTable.empty }
  
  let interactive_mode' init_st =
    write_hello ();
  
    let exit_code =
      if FStar.Options.record_hints() || FStar.Options.use_hints() then
  