(* The main file included in the OCaml toplevel. *)

#use "ml_toplevel/include_directories";;
#use "ml_toplevel/include_printers";;
#use "ml_toplevel/include_utilities";;

let go () =
  Flags.with_option
    Toploop.may_trace
    (fun () -> Coqloop.ml_toplevel_state := Some (Coqloop.loop ~state:(Option.get !Coqloop.ml_toplevel_state)))
    ();
  print_newline ()

let () =
  if not !Coqloop.ml_toplevel_include_ran then
    Toploop.add_directive
      "go"
      (Toploop.Directive_none go)
      Toploop.{section="Coq"; doc="Run Rocq toplevel loop"}

let _ =
  print_newline ();
  print_endline "OCaml toplevel with Rocq printers and utilities (to go back to Rocq, use `#quit;;`, or `#go;;` if `#trace` was used)"

let _ =
  Coqloop.ml_toplevel_include_ran := true