diff options
Diffstat (limited to 'toplevel')
-rw-r--r-- | toplevel/coqargs.ml | 8 | ||||
-rw-r--r-- | toplevel/coqloop.ml | 20 | ||||
-rw-r--r-- | toplevel/usage.ml | 1 | ||||
-rw-r--r-- | toplevel/vernac.ml | 33 |
4 files changed, 31 insertions, 31 deletions
diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml index 06b2ba41b..a1a07fce8 100644 --- a/toplevel/coqargs.ml +++ b/toplevel/coqargs.ml @@ -271,6 +271,11 @@ let get_cache opt = function | "force" -> Some Stm.AsyncOpts.Force | _ -> prerr_endline ("Error: force expected after "^opt); exit 1 +let get_identifier opt s = + try Names.Id.of_string s + with CErrors.UserError _ -> + prerr_endline ("Error: valid identifier expected after option "^opt); exit 1 + let is_not_dash_option = function | Some f when String.length f > 0 && f.[0] <> '-' -> true | _ -> false @@ -466,6 +471,9 @@ let parse_args arglist : coq_cmdopts * string list = |"-load-vernac-source-verbose"|"-lv" -> add_load_vernacular oval true (next ()) + |"-mangle-names" -> + Namegen.set_mangle_names_mode (get_identifier opt (next ())); oval + |"-print-mod-uid" -> let s = String.concat " " (List.map get_native_name rem) in print_endline s; exit 0 diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml index 1da46e8ce..a103cfe7f 100644 --- a/toplevel/coqloop.ml +++ b/toplevel/coqloop.ml @@ -341,6 +341,22 @@ 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 +let cproof p1 p2 = + let (a1,a2,a3,a4,_),(b1,b2,b3,b4,_) = Proof.proof p1, Proof.proof p2 in + evleq a1 b1 && + CList.equal (pequal evleq evleq) a2 b2 && + CList.equal Evar.equal a3 b3 && + CList.equal Evar.equal a4 b4 + let drop_last_doc = ref None let rec loop ~time ~state = @@ -351,6 +367,10 @@ let rec loop ~time ~state = (* Be careful to keep this loop tail-recursive *) let rec vernac_loop ~state = let nstate = do_vernac ~time ~state in + let proof_changed = not (Option.equal cproof nstate.proof state.proof) 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 ()); loop_flush_all (); vernac_loop ~state:nstate (* We recover the current stateid, threading from the caller is diff --git a/toplevel/usage.ml b/toplevel/usage.ml index 07553a2ab..504ffa521 100644 --- a/toplevel/usage.ml +++ b/toplevel/usage.ml @@ -79,6 +79,7 @@ let print_usage_channel co command = \n -impredicative-set set sort Set impredicative\ \n -indices-matter levels of indices (and nonuniform parameters) contribute to the level of inductives\ \n -type-in-type disable universe consistency checking\ +\n -mangle-names x mangle auto-generated names using prefix x\ \n -time display the time taken by each command\ \n -profile-ltac display the time taken by each (sub)tactic\ \n -m, --memory display total heap size at program exit\ diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index 7c889500a..56bdcc7e5 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -70,12 +70,6 @@ let print_cmd_header ?loc com = Pp.pp_with !Topfmt.std_ft (pp_cmd_header ?loc com); Format.pp_print_flush !Topfmt.std_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 "" - (* Reenable when we get back to feedback printing *) (* let is_end_of_input any = match any with *) (* Stm.End_of_input -> true *) @@ -94,23 +88,8 @@ end let interp_vernac ~time ~check ~interactive ~state (loc,com) = let open State in try - (* XXX: We need to run this before add as the classification is - highly dynamic and depends on the structure of the - document. Hopefully this is fixed when VtMeta can be removed - and Undo etc... are just interpreted regularly. *) - - (* XXX: The classifier can emit warnings so we need to guard - against that... *) - let wflags = CWarnings.get_flags () in - CWarnings.set_flags "none"; - let is_proof_step = match fst (Vernac_classifier.classify_vernac com) with - | VtProofStep _ | VtMeta | VtStartProof _ -> true - | _ -> false - in - CWarnings.set_flags wflags; - - (* The -time option is only supported from console-based - clients due to the way it prints. *) + (* The -time option is only supported from console-based clients + due to the way it prints. *) if time then print_cmd_header ?loc com; let com = if time then VernacTime(time,(CAst.make ?loc com)) else com in let doc, nsid, ntip = Stm.add ~doc:state.doc ~ontop:state.sid (not !Flags.quiet) (loc,com) in @@ -123,14 +102,6 @@ let interp_vernac ~time ~check ~interactive ~state (loc,com) = it otherwise reveals bugs *) (* Stm.observe nsid; *) let ndoc = if check then Stm.finish ~doc else doc in - - (* We could use a more refined criteria that depends on the - vernac. For now we imitate the old approach and rely on the - classification. *) - let print_goals = interactive && not !Flags.quiet && - is_proof_step && Proof_global.there_are_pending_proofs () in - - if print_goals then Feedback.msg_notice (pr_open_cur_subgoals ()); let new_proof = Proof_global.give_me_the_proof_opt () in { doc = ndoc; sid = nsid; proof = new_proof } with reraise -> |