anchor.diff:          CTable.register_module_path table (loaded mod_key) mod_path ns_query)
       table (List.rev mods) // List.rev to process files in order or *increasing* precedence
   
  -let run_initial_push (st: partial_repl_state) query =
  -  assert (not query.push_peek_only);
  -
  -  let commit_names st name_events =
  -    { st with prepl_names = commit_name_tracking None st.prepl_names name_events } in
  -
  -  let on_successful_init (env, name_events) deps repl_deps  =
  -    TcEnv.toggle_id_info (snd env) true;
  -
  -    let st = commit_names st name_events in
  -    let full_st =
  -      { repl_line = 1; repl_column = 0; repl_fname = st.prepl_fname;
  -        repl_curmod = None; repl_env = env; repl_deps = repl_deps;
  -        repl_stdin = st.prepl_stdin;
  -        repl_names = add_module_completions st.prepl_fname deps st.prepl_names } in
  -
  -    wrap_repl_state FullReplState <| run_regular_push full_st query in
  -
  -  let on_failed_init (env, name_events) repl_deps =
  -    let st = { st with prepl_env = env; prepl_deps = repl_deps } in
  -    handle_deps_failure (PartialReplState (commit_names st name_events)) in
  -
  -  let env = st.prepl_env in
  -  let env, finish_name_tracking = track_name_changes env in // begin name tracking…
  -
  -  match load_deps env st.prepl_fname st.prepl_deps with
  -  | Inl (env, deps, repl_deps) ->
  -    on_successful_init (finish_name_tracking env) deps repl_deps
  -  | Inr (env, completed_tasks) ->
  -    on_failed_init (finish_name_tracking env) completed_tasks
  -
  -let run_push (st: repl_state) query =
  -  match st with
  -  | PartialReplState st -> run_initial_push st query
  -  | FullReplState st -> wrap_repl_state FullReplState <| run_regular_push st query
  -
  -let run_symbol_lookup (st: full_repl_state) symbol pos_opt requested_info =
  +let run_symbol_lookup st symbol pos_opt requested_info =
     let dsenv, tcenv = st.repl_env in
   
     let info_of_lid_str lid_str =
  
positive.code:   let js_errors = errors |> List.map json_of_issue in
    ((QueryNOK, JsonList js_errors), Inl st)
  
  let run_regular_push_without_deps (st: full_repl_state) env deps query =
    let { push_code = text; push_line = line; push_column = column;
          push_peek_only = peek_only } = query in
  
  
negative.code: 
  open FStar.Parser.ParseIt
  
  type repl_state = { repl_line: int; repl_column: int; repl_fname: string;
                           repl_deps: list<completed_dep_task>;
                           repl_curmod: option<Syntax.Syntax.modul>;
                           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
  