diff options
Diffstat (limited to 'toplevel/coqloop.ml')
| -rw-r--r-- | toplevel/coqloop.ml | 217 |
1 files changed, 120 insertions, 97 deletions
diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml index 3239d360..59a464a2 100644 --- a/toplevel/coqloop.ml +++ b/toplevel/coqloop.ml @@ -23,7 +23,7 @@ type input_buffer = { mutable str : Bytes.t; (* buffer of already read characters *) mutable len : int; (* number of chars in the buffer *) mutable bols : int list; (* offsets in str of beginning of lines *) - mutable tokens : Pcoq.Gram.coq_parsable; (* stream of tokens *) + mutable tokens : Pcoq.Parsable.t; (* stream of tokens *) mutable start : int } (* stream count of the first char of the buffer *) (* Double the size of the buffer. *) @@ -76,7 +76,7 @@ let reset_input_buffer doc ic ibuf = ibuf.str <- Bytes.empty; ibuf.len <- 0; ibuf.bols <- []; - ibuf.tokens <- Pcoq.Gram.parsable (Stream.from (prompt_char doc ic ibuf)); + ibuf.tokens <- Pcoq.Parsable.make (Stream.from (prompt_char doc ic ibuf)); ibuf.start <- 0 (* Functions to print underlined locations from an input buffer. *) @@ -150,29 +150,28 @@ let print_highlight_location ib loc = let valid_buffer_loc ib loc = let (b,e) = Loc.unloc loc in b-ib.start >= 0 && e-ib.start < ib.len && b<=e - (* Toplevel error explanation. *) -let error_info_for_buffer ?loc buf = - Option.map (fun loc -> +let error_info_for_buffer ?loc phase buf = + match loc with + | None -> Topfmt.pr_phase ?loc phase + | Some loc -> let fname = loc.Loc.fname in - let hl, loc = (* We are in the toplevel *) - match fname with - | Loc.ToplevelInput -> - let nloc = adjust_loc_buf buf loc in - if valid_buffer_loc buf loc then - (fnl () ++ print_highlight_location buf nloc, nloc) - (* in the toplevel, but not a valid buffer *) - else (mt (), nloc) - (* we are in batch mode, don't adjust location *) - | Loc.InFile _ -> - (mt (), loc) - in Topfmt.pr_loc loc ++ hl - ) loc + match fname with + | Loc.ToplevelInput -> + let nloc = adjust_loc_buf buf loc in + if valid_buffer_loc buf loc then + match Topfmt.pr_phase ~loc:nloc phase with + | None -> None + | Some hd -> Some (hd ++ fnl () ++ print_highlight_location buf nloc) + (* in the toplevel, but not a valid buffer *) + else Topfmt.pr_phase ~loc phase + (* we are in batch mode, don't adjust location *) + | Loc.InFile _ -> Topfmt.pr_phase ~loc phase (* Actual printing routine *) -let print_error_for_buffer ?loc lvl msg buf = - let pre_hdr = error_info_for_buffer ?loc buf in +let print_error_for_buffer ?loc phase lvl msg buf = + let pre_hdr = error_info_for_buffer ?loc phase buf in if !print_emacs then Topfmt.emacs_logger ?pre_hdr lvl msg else Topfmt.std_logger ?pre_hdr lvl msg @@ -229,7 +228,7 @@ let top_buffer = str = Bytes.empty; len = 0; bols = []; - tokens = Pcoq.Gram.parsable (Stream.of_list []); + tokens = Pcoq.Parsable.make (Stream.of_list []); start = 0 } let set_prompt prompt = @@ -254,15 +253,15 @@ let parse_to_dot = let rec discard_to_dot () = try - Pcoq.Gram.entry_parse parse_to_dot top_buffer.tokens + Pcoq.Entry.parse parse_to_dot top_buffer.tokens with | Token.Error _ | CLexer.Error.E _ -> discard_to_dot () | Stm.End_of_input -> raise Stm.End_of_input | e when CErrors.noncritical e -> () let read_sentence ~state input = - let open Vernac.State in - try Stm.parse_sentence ~doc:state.doc state.sid input + (* XXX: careful with ignoring the state Eugene!*) + try G_toplevel.parse_toplevel input with reraise -> let reraise = CErrors.push reraise in discard_to_dot (); @@ -282,7 +281,7 @@ let extract_default_loc loc doc_id sid : Loc.t option = with _ -> loc (** Coqloop Console feedback handler *) -let coqloop_feed (fb : Feedback.feedback) = let open Feedback in +let coqloop_feed phase (fb : Feedback.feedback) = let open Feedback in match fb.contents with | Processed -> () | Incomplete -> () @@ -301,43 +300,9 @@ let coqloop_feed (fb : Feedback.feedback) = let open Feedback in (* TopErr.print_error_for_buffer ?loc lvl msg top_buffer *) | Message (Warning,loc,msg) -> let loc = extract_default_loc loc fb.doc_id fb.span_id in - TopErr.print_error_for_buffer ?loc Warning msg top_buffer + TopErr.print_error_for_buffer ?loc phase Warning msg top_buffer | Message (lvl,loc,msg) -> - TopErr.print_error_for_buffer ?loc lvl msg top_buffer - -(** [do_vernac] reads and executes a toplevel phrase, and print error - messages when an exception is raised, except for the following: - - Drop: kill the Coq toplevel, going down to the Caml toplevel if it exists. - Otherwise, exit. - - End_of_input: Ctrl-D was typed in, we will quit. - - In particular, this is normally the only place where a Sys.Break - is caught and handled (i.e. not re-raised). -*) - -let do_vernac ~time ~state = - let open Vernac.State in - top_stderr (fnl()); - if !print_emacs then top_stderr (str (top_buffer.prompt state.doc)); - resynch_buffer top_buffer; - try - let input = (top_buffer.tokens, None) in - Vernac.process_expr ~time ~state (read_sentence ~state (fst input)) - with - | Stm.End_of_input | CErrors.Quit -> - top_stderr (fnl ()); raise CErrors.Quit - | CErrors.Drop -> (* Last chance *) - if Mltop.is_ocaml_top() then raise CErrors.Drop - else (Feedback.msg_warning (str "There is no ML toplevel."); state) - (* Exception printing should be done by the feedback listener, - however this is not yet ready so we rely on the exception for - now. *) - | any -> - let (e, info) = CErrors.push any in - let loc = Loc.get_loc info in - let msg = CErrors.iprint (e, info) in - TopErr.print_error_for_buffer ?loc Feedback.Error msg top_buffer; - state + TopErr.print_error_for_buffer ?loc phase lvl msg top_buffer (** Main coq loop : read vernacular expressions until Drop is entered. Ctrl-C is handled internally as Sys.Break instead of aborting Coq. @@ -353,12 +318,6 @@ let loop_flush_all () = Format.pp_print_flush !Topfmt.std_ft (); Format.pp_print_flush !Topfmt.err_ft () -let pr_open_cur_subgoals () = - try - let proof = Proof_global.give_me_the_proof () in - Printer.pr_open_subgoals ~proof - with Proof_global.NoCurrentProof -> Pp.str "" - (* Goal equality heuristic. *) let pequal cmp1 cmp2 (a1,a2) (b1,b2) = cmp1 a1 b1 && cmp2 a2 b2 let evleq e1 e2 = CList.equal Evar.equal e1 e2 @@ -369,53 +328,117 @@ let cproof p1 p2 = CList.equal Evar.equal a3 b3 && CList.equal Evar.equal a4 b4 +let drop_last_doc = ref None + +(* todo: could add other Set/Unset commands, such as "Printing Universes" *) +let print_anyway_opts = [ + [ "Diffs" ]; + ] + +let print_anyway c = + let open Vernacexpr in + match c with + | VernacExpr (_, VernacSetOption (_, opt, _)) + | VernacExpr (_, VernacUnsetOption (_, opt)) -> + List.mem opt print_anyway_opts + | _ -> false + (* We try to behave better when goal printing raises an exception [usually Ctrl-C] This is mostly a hack as we should protect printing in a more generic way, but that'll do for now *) -let top_goal_print oldp newp = +let top_goal_print ~doc c oldp newp = try let proof_changed = not (Option.equal cproof oldp newp) in - let print_goals = not !Flags.quiet && - proof_changed && Proof_global.there_are_pending_proofs () in - if print_goals then Feedback.msg_notice (pr_open_cur_subgoals ()) + let print_goals = proof_changed && Proof_global.there_are_pending_proofs () || + print_anyway c in + if not !Flags.quiet && print_goals then begin + let dproof = Stm.get_prev_proof ~doc (Stm.get_current_state ~doc) in + Printer.print_and_diff dproof newp + end with - | CErrors.Drop | CErrors.Quit as exn -> raise exn | exn -> let (e, info) = CErrors.push exn in let loc = Loc.get_loc info in let msg = CErrors.iprint (e, info) in - TopErr.print_error_for_buffer ?loc Feedback.Error msg top_buffer + TopErr.print_error_for_buffer ?loc Topfmt.InteractiveLoop Feedback.Error msg top_buffer -let drop_last_doc = ref None +(* Careful to keep this loop tail-rec *) +let rec vernac_loop ~state = + let open CAst in + let open Vernac.State in + let open G_toplevel in + loop_flush_all (); + top_stderr (fnl()); + if !print_emacs then top_stderr (str (top_buffer.prompt state.doc)); + resynch_buffer top_buffer; + (* execute one command *) + try + let input = top_buffer.tokens in + match read_sentence ~state input with + | {v=VernacBacktrack(bid,_,_)} -> + let bid = Stateid.of_int bid in + let doc, res = Stm.edit_at ~doc:state.doc bid in + assert (res = `NewTip); + let state = { state with doc; sid = bid } in + vernac_loop ~state + + | {v=VernacQuit} -> + exit 0 + | {v=VernacDrop} -> + if Mltop.is_ocaml_top() + then (drop_last_doc := Some state; state) + else (Feedback.msg_warning (str "There is no ML toplevel."); vernac_loop ~state) + | {v=VernacControl c; loc} -> + let nstate = Vernac.process_expr ~state (make ?loc c) in + top_goal_print ~doc:state.doc c state.proof nstate.proof; + vernac_loop ~state:nstate + with + | Stm.End_of_input -> + top_stderr (fnl ()); exit 0 + (* Exception printing should be done by the feedback listener, + however this is not yet ready so we rely on the exception for + now. *) + | any -> + let (e, info) = CErrors.push any in + let loc = Loc.get_loc info in + let msg = CErrors.iprint (e, info) in + TopErr.print_error_for_buffer ?loc Topfmt.InteractiveLoop Feedback.Error msg top_buffer; + vernac_loop ~state -let rec loop ~time ~state = +let rec loop ~state = let open Vernac.State in Sys.catch_break true; try reset_input_buffer state.doc stdin top_buffer; - (* Be careful to keep this loop tail-recursive *) - let rec vernac_loop ~state = - let nstate = do_vernac ~time ~state in - top_goal_print state.proof nstate.proof; - loop_flush_all (); - vernac_loop ~state:nstate - in vernac_loop ~state + vernac_loop ~state with - | CErrors.Drop -> - (* Due to using exceptions as a form of control, state here goes - out of sync as [do_vernac] will never return. We must thus do - this hack until we make `Drop` a toplevel-only command. See - bug #6872. *) - let state = { state with sid = Stm.get_current_state ~doc:state.doc } in - drop_last_doc := Some state; - state - | CErrors.Quit -> exit 0 | any -> - top_stderr (str "Anomaly: main loop exited with exception: " ++ - str (Printexc.to_string any) ++ - fnl() ++ - str"Please report" ++ - strbrk" at " ++ str Coq_config.wwwbugtracker ++ str "."); - loop ~time ~state + top_stderr + (hov 0 (str "Anomaly: main loop exited with exception:" ++ spc () ++ + str (Printexc.to_string any)) ++ spc () ++ + hov 0 (str "Please report at " ++ str Coq_config.wwwbugtracker ++ str ".")); + loop ~state + +(* Default toplevel loop *) +let warning s = Flags.(with_option warn Feedback.msg_warning (strbrk s)) + +let drop_args = ref None +let loop ~opts ~state = + drop_args := Some opts; + let open Coqargs in + print_emacs := opts.print_emacs; + (* We initialize the console only if we run the toploop_run *) + let tl_feed = Feedback.add_feeder (coqloop_feed Topfmt.InteractiveLoop) in + if Dumpglob.dump () then begin + Flags.if_verbose warning "Dumpglob cannot be used in interactive mode."; + Dumpglob.noglob () + end; + let _ = loop ~state in + (* Initialise and launch the Ocaml toplevel *) + Coqinit.init_ocaml_path(); + Mltop.ocaml_toploop(); + (* We delete the feeder after the OCaml toploop has ended so users + of Drop can see the feedback. *) + Feedback.del_feeder tl_feed |