anchor.diff:    s.buffer := !s.buffer @ [ read_chunk () ]
   
   let interactive_mode dsenv env =
  -    if Option.isSome !Options.codegen
  -    then (Util.print_warning "code-generation is not supported in interactive mode, ignoring the codegen flag");
  -
  -    let rec go (stack:stack) (curmod:option<modul>) dsenv env =
  -        begin match shift_chunk () with
  -            | Pop msg ->
  -              Parser.DesugarEnv.pop dsenv |> ignore;
  -              Tc.Env.pop env msg |> ignore;
  -              env.solver.refresh();
  -              Options.reset_options() |> ignore;
  -              let (curmod, dsenv, env), stack = match stack with
  -                | [] -> Util.print_error "too many pops"; exit 1
  -                | hd::tl -> hd, tl in
  -              go stack curmod dsenv env
  -
  -            | Push msg ->
  -              let stack = (curmod, dsenv, env)::stack in
  -              let dsenv = Parser.DesugarEnv.push dsenv in
  -              let env = Tc.Env.push env msg in
  -              go stack curmod dsenv env
  -
  -            | Code (text, (ok, fail)) ->
  -                let mark dsenv env =
  -                    let dsenv = Parser.DesugarEnv.mark dsenv in
  -                    let env = Tc.Env.mark env in
  -                    dsenv, env in
  -
  -                let reset_mark dsenv env =
  -                    let dsenv = Parser.DesugarEnv.reset_mark dsenv in
  -                    let env = Tc.Env.reset_mark env in
  -                    dsenv, env in
  -
  -                let commit_mark dsenv env =
  -                    let dsenv = Parser.DesugarEnv.commit_mark dsenv in
  -                    let env = Tc.Env.commit_mark env in
  -                    dsenv, env in
  -
  -                let fail curmod dsenv_mark env_mark =
  -                    Tc.Errors.report_all() |> ignore;
  -                    Tc.Errors.num_errs := 0;
  -                    Util.print1 "%s\n" fail;
  -                    let dsenv, env = reset_mark dsenv_mark env_mark in
  -                    go stack curmod dsenv env in
  -
  -              let dsenv_mark, env_mark = mark dsenv env in
  -              let res = tc_one_fragment curmod dsenv_mark env_mark text in
  -
  -              begin match res with
  -                | Some (curmod, dsenv, env) ->
  -                  if !Tc.Errors.num_errs=0
  -                  then begin
  -                     Util.print1 "\n%s\n" ok;
  -                     let dsenv, env = commit_mark dsenv env in
  -                     go stack curmod dsenv env
  +  if Option.isSome !Options.codegen then
  +    (Util.print_warning "code-generation is not supported in interactive mode, ignoring the codegen flag");
  +    let rec go (stack:stack) (curmod:option<modul>) dsenv env = begin
  +      match shift_chunk () with
  +      | Pop msg ->
  +          Parser.DesugarEnv.pop dsenv |> ignore;
  +          Tc.Env.pop env msg |> ignore;
  +          env.solver.refresh();
  +          Options.reset_options() |> ignore;
  +          let (curmod, dsenv, env), stack =
  +            match stack with
  +            | [] -> Util.print_error "too many pops"; exit 1
  +            | hd::tl -> hd, tl
  +          in
  +          go stack curmod dsenv env
  +      | Push msg ->
  +          let stack = (curmod, dsenv, env)::stack in
  +          let dsenv = Parser.DesugarEnv.push dsenv in
  +          let env = Tc.Env.push env msg in
  +          go stack curmod dsenv env
  +      | Code (text, (ok, fail)) ->
  +          let mark dsenv env =
  +            let dsenv = Parser.DesugarEnv.mark dsenv in
  +            let env = Tc.Env.mark env in
  +            dsenv, env in
  +          let reset_mark dsenv env =
  +            let dsenv = Parser.DesugarEnv.reset_mark dsenv in
  +            let env = Tc.Env.reset_mark env in
  +            dsenv, env in
  +          let commit_mark dsenv env =
  +            let dsenv = Parser.DesugarEnv.commit_mark dsenv in
  +            let env = Tc.Env.commit_mark env in
  +            dsenv, env in
  +          let fail curmod dsenv_mark env_mark =
  +            Tc.Errors.report_all() |> ignore;
  +            Tc.Errors.num_errs := 0;
  +            Util.print1 "%s\n" fail;
  +            let dsenv, env = reset_mark dsenv_mark env_mark in
  +            go stack curmod dsenv env in
  +          let dsenv_mark, env_mark = mark dsenv env in
  +          let res = tc_one_fragment curmod dsenv_mark env_mark text in begin
  +            match res with
  +            | Some (curmod, dsenv, env) ->
  +                if !Tc.Errors.num_errs = 0 then begin
  +                  Util.print1 "\n%s\n" ok;
  +                  let dsenv, env = commit_mark dsenv env in
  +                  go stack curmod dsenv env
                     end
  -                  else fail curmod dsenv_mark env_mark
  -
  -                | _ ->
  -                  fail curmod dsenv_mark env_mark
  -              end
  -        end in
  -
  +                else fail curmod dsenv_mark env_mark
  +            | _ -> fail curmod dsenv_mark env_mark
  +            end
  +    end in
       go [] None dsenv env
   
  -
  -let codegen fmods env=
  -    if !Options.codegen = Some "OCaml"
  -    || !Options.codegen = Some "FSharp"
  -    then begin
  -        let c, mllibs = Util.fold_map Extraction.ML.ExtractMod.extract (Extraction.ML.Env.mkContext env) fmods in
  -        let mllibs = List.flatten mllibs in
  -        let ext = if !Options.codegen = Some "FSharp" then ".fs" else ".ml" in
  -        let newDocs = List.collect Extraction.ML.Code.doc_of_mllib mllibs in
  -//                           else List.collect Extraction.OCaml.Code.doc_of_mllib mllibs, ".ml" in
  -        List.iter (fun (n,d) -> Util.write_file (Options.prependOutputDir (n^ext)) (FStar.Format.pretty 120 d)) newDocs
  +let codegen fmods env =
  +  if !Options.codegen = Some "OCaml" ||
  +     !Options.codegen = Some "FSharp"
  +  then begin
  +    let c, mllibs = Util.fold_map Extraction.ML.ExtractMod.extract (Extraction.ML.Env.mkContext env) fmods in
  +    let mllibs = List.flatten mllibs in
  +    let ext = if !Options.codegen = Some "FSharp" then ".fs" else ".ml" in
  +    let newDocs = List.collect Extraction.ML.Code.doc_of_mllib mllibs in
  +//else List.collect Extraction.OCaml.Code.doc_of_mllib mllibs, ".ml" in
  +    List.iter (fun (n,d) -> Util.write_file (Options.prependOutputDir (n^ext)) (FStar.Format.pretty 120 d)) newDocs
       end
   
   exception Found of string
  
positive.code: open FStar.Tc.Util
  open FStar.Ident
  
  let process_args () =
    let file_list = Util.mk_ref [] in
    let res = Getopt.parse_cmdline (Options.specs()) (fun i -> file_list := !file_list @ [i]) in
  
negative.code: }
  
  let rec read_chunk () =
    let s = the_interactive_state in
    let log =
      if !Options.debug <> [] then
        let transcript =
          match !s.log with
          | Some transcript -> transcript
          | None ->
              let transcript = Util.open_file_for_writing "transcript" in
              s.log := Some transcript;
              transcript
        in
        fun line ->
          Util.append_to_file transcript line;
          Util.flush_file transcript
      else
        fun _ -> ()
    in
    let stdin =
      match !s.stdin with
      | Some i -> i
      | None ->
          let i = Util.open_stdin () in
          s.stdin := Some i;
          i
    in
    let line =
      match Util.read_line stdin with
      | None -> exit 0
      | Some l -> l
    in
    log line;
  
    let l = Util.trim_string line in
    if Util.starts_with l "#end" then begin
      let responses =
        match Util.split l " " with
        | [_; ok; fail] -> (ok, fail)
        | _ -> ("ok", "fail") in
      let str = Util.string_of_string_builder s.chunk in
      Util.clear_string_builder s.chunk; Code (str, responses)
      end
    else if Util.starts_with l "#pop" then (Util.clear_string_builder s.chunk; Pop l)
    else if Util.starts_with l "#push" then (Util.clear_string_builder s.chunk; Push l)
    else if l = "#finish" then exit 0
    else
      (Util.string_builder_append s.chunk line;
      Util.string_builder_append s.chunk "\n";
      read_chunk())
  
  let shift_chunk () =
    let s = the_interactive_state in
    match !s.buffer with
    | [] -> read_chunk ()
    | chunk :: chunks ->
        s.buffer := chunks;
        chunk
  