diff options
48 files changed, 625 insertions, 536 deletions
diff --git a/Makefile.build b/Makefile.build index 9d76638e1..c62420326 100644 --- a/Makefile.build +++ b/Makefile.build @@ -440,9 +440,10 @@ $(COQWORKMGR): $(call bestobj, lib/clib.cma stm/coqworkmgrApi.cmo tools/coqworkm # fake_ide : for debugging or test-suite purpose, a fake ide simulating # a connection to coqtop -ideslave -FAKEIDECMO:= lib/clib.cma lib/cErrors.cmo lib/spawn.cmo ide/document.cmo \ - ide/serialize.cmo ide/xml_lexer.cmo ide/xml_parser.cmo ide/xml_printer.cmo \ - ide/xmlprotocol.cmo tools/fake_ide.cmo +FAKEIDECMO:= lib/clib.cma lib/cErrors.cmo lib/spawn.cmo \ + ide/document.cmo ide/serialize.cmo ide/richpp.cmo ide/xml_lexer.cmo \ + ide/xml_parser.cmo ide/xml_printer.cmo ide/xmlprotocol.cmo \ + tools/fake_ide.cmo $(FAKEIDE): $(call bestobj, $(FAKEIDECMO)) | $(IDETOPLOOPCMA:.cma=$(BESTDYN)) $(SHOW)'OCAMLBEST -o $@' diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt index 12c3ec454..53e9a282f 100644 --- a/dev/doc/changes.txt +++ b/dev/doc/changes.txt @@ -70,6 +70,58 @@ work for EXTEND macros though. - The header parameter to `user_err` has been made optional. +** Pretty printing ** + +Some functions have been removed, see pretty printing below for more +details. + +* Pretty Printing and XML protocol * + +The type std_cmdpps has been reworked and made the canonical "Coq rich +document type". This allows for a more uniform handling of printing +(specially in IDEs). The main consequences are: + + - Richpp has been confined to IDE use. Most of previous uses of the + `richpp` type should be replaced now by `Pp.std_cmdpps`. Main API + has been updated. + + - The XML protocol will send a new message type of `pp`, which should + be rendered client-wise. + + - `Set Printing Width` is deprecated, now width is controlled + client-side. + + - `Pp_control` has removed. The new module `Topfmt` implements + console control for the toplevel. + + - The impure tag system in Pp has been removed. This also does away + with the printer signatures and functors. Now printers tag + unconditionally. + + - The following functions have been removed from `Pp`: + + val stras : int * string -> std_ppcmds + val tbrk : int * int -> std_ppcmds + val tab : unit -> std_ppcmds + val pifb : unit -> std_ppcmds + val comment : int -> std_ppcmds + val comments : ((int * int) * string) list ref + val eval_ppcmds : std_ppcmds -> std_ppcmds + val is_empty : std_ppcmds -> bool + val t : std_ppcmds -> std_ppcmds + val hb : int -> std_ppcmds + val vb : int -> std_ppcmds + val hvb : int -> std_ppcmds + val hovb : int -> std_ppcmds + val tb : unit -> std_ppcmds + val close : unit -> std_ppcmds + val tclose : unit -> std_ppcmds + val open_tag : Tag.t -> std_ppcmds + val close_tag : unit -> std_ppcmds + val msg_with : ... + + module Tag + ========================================= = CHANGES BETWEEN COQ V8.5 AND COQ V8.6 = ========================================= diff --git a/dev/top_printers.ml b/dev/top_printers.ml index dc354b130..cd464801b 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -29,7 +29,7 @@ let _ = set_bool_option_value ["Printing";"Matching"] false let _ = Detyping.set_detype_anonymous (fun _ _ -> raise Not_found) (* std_ppcmds *) -let pp x = Pp.pp_with !Pp_control.std_ft x +let pp x = Pp.pp_with !Topfmt.std_ft x (** Future printer *) diff --git a/ide/coq.ml b/ide/coq.ml index 9637b5b3f..e2036beee 100644 --- a/ide/coq.ml +++ b/ide/coq.ml @@ -205,7 +205,7 @@ type handle = { proc : CoqTop.process; xml_oc : Xml_printer.t; mutable alive : bool; - mutable waiting_for : ccb option; (* last call + callback + log *) + mutable waiting_for : ccb option; (* last call + callback *) } (** Coqtop process status : diff --git a/ide/coqOps.ml b/ide/coqOps.ml index 0f3629c8f..7982ffc8b 100644 --- a/ide/coqOps.ml +++ b/ide/coqOps.ml @@ -162,13 +162,16 @@ let flags_to_color f = else if List.mem `INCOMPLETE f then `NAME "gray" else `NAME Preferences.processed_color#get -let validate s = - let open Xml_datatype in - let rec validate = function - | PCData s -> Glib.Utf8.validate s - | Element (_, _, children) -> List.for_all validate children - in - validate (Richpp.repr s) +(* Move to utils? *) +let rec validate (s : Pp.std_ppcmds) = match s with + | Pp.Ppcmd_empty + | Pp.Ppcmd_print_break _ + | Pp.Ppcmd_force_newline -> true + | Pp.Ppcmd_glue l -> List.for_all validate l + | Pp.Ppcmd_string s -> Glib.Utf8.validate s + | Pp.Ppcmd_box (_,s) + | Pp.Ppcmd_tag (_,s) -> validate s + | Pp.Ppcmd_comment s -> List.for_all Glib.Utf8.validate s module Doc = Document @@ -418,9 +421,10 @@ object(self) | _ -> false method private enqueue_feedback msg = + (* Minilib.log ("Feedback received: " ^ Xml_printer.to_string_fmt (Xmlprotocol.of_feedback msg)); *) let id = msg.id in if self#is_dummy_id id then () else Queue.add msg feedbacks - + method private process_feedback () = let rec eat_feedback n = if n = 0 then true else @@ -466,7 +470,7 @@ object(self) (Printf.sprintf "%s %s %s" filepath ident ty) | Message(Error, loc, msg), Some (id,sentence) -> let loc = Option.default Loc.ghost loc in - let msg = Richpp.raw_print msg in + let msg = Pp.string_of_ppcmds msg in log "ErrorMsg" id; remove_flag sentence `PROCESSING; add_flag sentence (`ERROR (loc, msg)); @@ -476,14 +480,15 @@ object(self) self#position_error_tag_at_sentence sentence (Some (Loc.unloc loc)) | Message(Warning, loc, msg), Some (id,sentence) -> let loc = Option.default Loc.ghost loc in - let rmsg = Richpp.raw_print msg in - log "WarningMsg" id; + let rmsg = Pp.string_of_ppcmds msg in + log ("WarningMsg: " ^ Pp.string_of_ppcmds msg)id; add_flag sentence (`WARNING (loc, rmsg)); self#attach_tooltip sentence loc rmsg; self#position_warning_tag_at_sentence sentence loc; messages#push Warning msg | Message(lvl, loc, msg), Some (id,sentence) -> - messages#push lvl msg + log ("Msg: " ^ Pp.string_of_ppcmds msg) id; + messages#push lvl msg | InProgress n, _ -> if n < 0 then processed <- processed + abs n else to_process <- to_process + n @@ -629,10 +634,9 @@ object(self) if Queue.is_empty queue then conclude topstack else match Queue.pop queue, topstack with | `Skip(start,stop), [] -> - - logger Feedback.Error (Richpp.richpp_of_string "You must close the proof with Qed or Admitted"); + logger Feedback.Error (Pp.str "You must close the proof with Qed or Admitted"); self#discard_command_queue queue; - conclude [] + conclude [] | `Skip(start,stop), (_,s) :: topstack -> assert(start#equal (buffer#get_iter_at_mark s.start)); assert(stop#equal (buffer#get_iter_at_mark s.stop)); @@ -646,7 +650,7 @@ object(self) let handle_answer = function | Good (id, (Util.Inl (* NewTip *) (), msg)) -> Doc.assign_tip_id document id; - logger Feedback.Notice (Richpp.richpp_of_string msg); + logger Feedback.Notice (Pp.str msg); self#commit_queue_transaction sentence; loop id [] | Good (id, (Util.Inr (* Unfocus *) tip, msg)) -> @@ -654,7 +658,7 @@ object(self) let topstack, _ = Doc.context document in self#exit_focus; self#cleanup (Doc.cut_at document tip); - logger Feedback.Notice (Richpp.richpp_of_string msg); + logger Feedback.Notice (Pp.str msg); self#mark_as_needed sentence; if Queue.is_empty queue then loop tip [] else loop tip (List.rev topstack) @@ -673,7 +677,7 @@ object(self) let next = function | Good _ -> messages#clear; - messages#push Feedback.Info (Richpp.richpp_of_string "All proof terms checked by the kernel"); + messages#push Feedback.Info (Pp.str "All proof terms checked by the kernel"); Coq.return () | Fail x -> self#handle_failure x in Coq.bind (Coq.status true) next @@ -860,7 +864,7 @@ object(self) let next = function | Fail (_, l, str) -> (* FIXME: check *) display_error (l, str); - messages#add (Richpp.richpp_of_string ("Unsuccessfully tried: "^phrase)); + messages#add (Pp.str ("Unsuccessfully tried: "^phrase)); more | Good msg -> messages#add_string msg; @@ -906,7 +910,7 @@ object(self) let get_initial_state = let next = function | Fail (_, _, message) -> - let message = "Couldn't initialize coqtop\n\n" ^ (Richpp.raw_print message) in + let message = "Couldn't initialize coqtop\n\n" ^ (Pp.string_of_ppcmds message) in let popup = GWindow.message_dialog ~buttons:GWindow.Buttons.ok ~message_type:`ERROR ~message () in ignore (popup#run ()); exit 1 | Good id -> initial_state <- id; Coq.return () in diff --git a/ide/coqide.ml b/ide/coqide.ml index 3d56f9dd4..25858acce 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -318,7 +318,7 @@ let export kind sn = local_cd f ^ cmd_coqdoc#get ^ " --" ^ kind ^ " -o " ^ (Filename.quote output) ^ " " ^ (Filename.quote basef) ^ " 2>&1" in - sn.messages#set (Richpp.richpp_of_string ("Running: "^cmd)); + sn.messages#set (Pp.str ("Running: "^cmd)); let finally st = flash_info (cmd ^ pr_exit_status st) in run_command (fun msg -> sn.messages#add_string msg) finally cmd @@ -431,7 +431,7 @@ let compile sn = ^ " " ^ (Filename.quote f) ^ " 2>&1" in let buf = Buffer.create 1024 in - sn.messages#set (Richpp.richpp_of_string ("Running: "^cmd)); + sn.messages#set (Pp.str ("Running: "^cmd)); let display s = sn.messages#add_string s; Buffer.add_string buf s @@ -441,8 +441,8 @@ let compile sn = flash_info (f ^ " successfully compiled") else begin flash_info (f ^ " failed to compile"); - sn.messages#set (Richpp.richpp_of_string "Compilation output:\n"); - sn.messages#add (Richpp.richpp_of_string (Buffer.contents buf)); + sn.messages#set (Pp.str "Compilation output:\n"); + sn.messages#add (Pp.str (Buffer.contents buf)); end in run_command display finally cmd @@ -464,7 +464,7 @@ let make sn = |Some f -> File.saveall (); let cmd = local_cd f ^ cmd_make#get ^ " 2>&1" in - sn.messages#set (Richpp.richpp_of_string "Compilation output:\n"); + sn.messages#set (Pp.str "Compilation output:\n"); Buffer.reset last_make_buf; last_make := ""; last_make_index := 0; @@ -508,11 +508,11 @@ let next_error sn = let stopi = b#get_iter_at_byte ~line:(line-1) stop in b#apply_tag Tags.Script.error ~start:starti ~stop:stopi; b#place_cursor ~where:starti; - sn.messages#set (Richpp.richpp_of_string error_msg); + sn.messages#set (Pp.str error_msg); sn.script#misc#grab_focus () with Not_found -> last_make_index := 0; - sn.messages#set (Richpp.richpp_of_string "No more errors.\n") + sn.messages#set (Pp.str "No more errors.\n") let next_error = cb_on_current_term next_error @@ -789,7 +789,7 @@ let coqtop_arguments sn = let args = String.concat " " args in let msg = Printf.sprintf "Invalid arguments: %s" args in let () = sn.messages#clear in - sn.messages#push Feedback.Error (Richpp.richpp_of_string msg) + sn.messages#push Feedback.Error (Pp.str msg) else dialog#destroy () in let _ = entry#connect#activate ok_cb in diff --git a/ide/coqidetop.mllib b/ide/coqidetop.mllib index ed1fa465d..043ad6008 100644 --- a/ide/coqidetop.mllib +++ b/ide/coqidetop.mllib @@ -2,7 +2,7 @@ Xml_lexer Xml_parser Xml_printer Serialize -Richprinter +Richpp Xmlprotocol Texmacspp Document diff --git a/ide/ide.mllib b/ide/ide.mllib index 72a14134b..12170c462 100644 --- a/ide/ide.mllib +++ b/ide/ide.mllib @@ -9,11 +9,11 @@ Config_lexer Utf8_convert Preferences Project_file -Serialize -Richprinter Xml_lexer Xml_parser Xml_printer +Serialize +Richpp Xmlprotocol Ideutils Coq diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml index 0cb8d377f..88b61042e 100644 --- a/ide/ide_slave.ml +++ b/ide/ide_slave.ml @@ -32,9 +32,6 @@ let init_signal_handler () = let f _ = if !catch_break then raise Sys.Break else Control.interrupt := true in Sys.set_signal Sys.sigint (Sys.Signal_handle f) - -(** Redirection of standard output to a printable buffer *) - let pr_with_pid s = Printf.eprintf "[pid %d] %s\n%!" (Unix.getpid ()) s let pr_error s = pr_with_pid s @@ -174,13 +171,13 @@ let process_goal sigma g = let id = Goal.uid g in let ccl = let norm_constr = Reductionops.nf_evar sigma (Goal.V82.concl sigma g) in - Richpp.richpp_of_pp (pr_goal_concl_style_env env sigma norm_constr) + pr_goal_concl_style_env env sigma norm_constr in let process_hyp d (env,l) = let d = CompactedDecl.map_constr (Reductionops.nf_evar sigma) d in let d' = CompactedDecl.to_named_context d in (List.fold_right Environ.push_named d' env, - (Richpp.richpp_of_pp (pr_compacted_decl env sigma d)) :: l) in + (pr_compacted_decl env sigma d) :: l) in let (_env, hyps) = Context.Compacted.fold process_hyp (Termops.compact_named_context (Environ.named_context env)) ~init:(min_env,[]) in @@ -340,13 +337,10 @@ let handle_exn (e, info) = let loc_of e = match Loc.get_loc e with | Some loc when not (Loc.is_ghost loc) -> Some (Loc.unloc loc) | _ -> None in - let mk_msg () = - let msg = CErrors.print ~info e in - Richpp.richpp_of_pp msg - in + let mk_msg () = CErrors.print ~info e in match e with - | CErrors.Drop -> dummy, None, Richpp.richpp_of_string "Drop is not allowed by coqide!" - | CErrors.Quit -> dummy, None, Richpp.richpp_of_string "Quit is not allowed by coqide!" + | CErrors.Drop -> dummy, None, Pp.str "Drop is not allowed by coqide!" + | CErrors.Quit -> dummy, None, Pp.str "Quit is not allowed by coqide!" | e -> match Stateid.get info with | Some (valid, _) -> valid, loc_of info, mk_msg () @@ -446,7 +440,6 @@ let print_xml = try Xml_printer.print oc xml; Mutex.unlock m with e -> let e = CErrors.push e in Mutex.unlock m; iraise e - let slave_feeder xml_oc msg = let xml = Xmlprotocol.of_feedback msg in print_xml xml_oc xml @@ -467,7 +460,6 @@ let loop () = (* SEXP parser make *) let xml_ic = Xml_parser.make (Xml_parser.SLexbuf in_lb) in let () = Xml_parser.check_eof xml_ic false in - Feedback.set_logger Feedback.feedback_logger; Feedback.add_feeder (slave_feeder xml_oc); (* We'll handle goal fetching and display in our own way *) Vernacentries.enable_goal_printing := false; @@ -478,7 +470,7 @@ let loop () = (* pr_with_pid (Xml_printer.to_string_fmt xml_query); *) let Xmlprotocol.Unknown q = Xmlprotocol.to_call xml_query in let () = pr_debug_call q in - let r = eval_call q in + let r = eval_call q in let () = pr_debug_answer q r in (* pr_with_pid (Xml_printer.to_string_fmt (Xmlprotocol.of_answer q r)); *) print_xml xml_oc (Xmlprotocol.of_answer q r); diff --git a/ide/ideutils.ml b/ide/ideutils.ml index c3a280796..498a911ee 100644 --- a/ide/ideutils.ml +++ b/ide/ideutils.ml @@ -327,7 +327,7 @@ let textview_width (view : #GText.view_skel) = let char_width = GPango.to_pixels metrics#approx_char_width in pixel_width / char_width -type logger = Feedback.level -> Richpp.richpp -> unit +type logger = Feedback.level -> Pp.std_ppcmds -> unit let default_logger level message = let level = match level with @@ -337,7 +337,7 @@ let default_logger level message = | Feedback.Warning -> `WARNING | Feedback.Error -> `ERROR in - Minilib.log ~level (xml_to_string message) + Minilib.log ~level (Pp.string_of_ppcmds message) (** {6 File operations} *) diff --git a/ide/ideutils.mli b/ide/ideutils.mli index e32a4d9e3..1ae66e23e 100644 --- a/ide/ideutils.mli +++ b/ide/ideutils.mli @@ -69,7 +69,7 @@ val requote : string -> string val textview_width : #GText.view_skel -> int (** Returns an approximate value of the character width of a textview *) -type logger = Feedback.level -> Richpp.richpp -> unit +type logger = Feedback.level -> Pp.std_ppcmds -> unit val default_logger : logger (** Default logger. It logs messages that the casual user should not see. *) diff --git a/ide/interface.mli b/ide/interface.mli index 123cac6c2..43446f391 100644 --- a/ide/interface.mli +++ b/ide/interface.mli @@ -12,15 +12,14 @@ type raw = bool type verbose = bool -type richpp = Richpp.richpp (** The type of coqtop goals *) type goal = { goal_id : string; (** Unique goal identifier *) - goal_hyp : richpp list; + goal_hyp : Pp.std_ppcmds list; (** List of hypotheses *) - goal_ccl : richpp; + goal_ccl : Pp.std_ppcmds; (** Goal conclusion *) } @@ -119,7 +118,7 @@ type edit_id = Feedback.edit_id should probably retract to that point *) type 'a value = | Good of 'a - | Fail of (state_id * location * richpp) + | Fail of (state_id * location * Pp.std_ppcmds) type ('a, 'b) union = ('a, 'b) Util.union @@ -203,7 +202,7 @@ type about_sty = unit type about_rty = coq_info type handle_exn_sty = Exninfo.iexn -type handle_exn_rty = state_id * location * richpp +type handle_exn_rty = state_id * location * Pp.std_ppcmds (* Retrocompatibility stuff *) type interp_sty = (raw * verbose) * string diff --git a/lib/richpp.ml b/ide/richpp.ml index c0128dbc2..c0128dbc2 100644 --- a/lib/richpp.ml +++ b/ide/richpp.ml diff --git a/lib/richpp.mli b/ide/richpp.mli index 2e839e996..2e839e996 100644 --- a/lib/richpp.mli +++ b/ide/richpp.mli diff --git a/ide/wg_Command.ml b/ide/wg_Command.ml index d33c0add4..b83bd107e 100644 --- a/ide/wg_Command.ml +++ b/ide/wg_Command.ml @@ -103,7 +103,7 @@ object(self) let process = Coq.bind (Coq.query (phrase,Stateid.dummy)) (function | Interface.Fail (_,l,str) -> - Ideutils.insert_xml result#buffer str; + Ideutils.insert_xml result#buffer (Richpp.richpp_of_pp str); notebook#set_page ~tab_label:(new_tab_lbl "Error") frame#coerce; Coq.return () | Interface.Good res -> diff --git a/ide/wg_MessageView.ml b/ide/wg_MessageView.ml index 0330b8eff..1cf389c75 100644 --- a/ide/wg_MessageView.ml +++ b/ide/wg_MessageView.ml @@ -28,9 +28,9 @@ class type message_view = inherit GObj.widget method connect : message_view_signals method clear : unit - method add : Richpp.richpp -> unit + method add : Pp.std_ppcmds -> unit method add_string : string -> unit - method set : Richpp.richpp -> unit + method set : Pp.std_ppcmds -> unit method push : Ideutils.logger (** same as [add], but with an explicit level instead of [Notice] *) method buffer : GText.buffer @@ -79,21 +79,14 @@ let message_view () : message_view = | Feedback.Warning -> [Tags.Message.warning] | _ -> [] in - let rec non_empty = function - | Xml_datatype.PCData "" -> false - | Xml_datatype.PCData _ -> true - | Xml_datatype.Element (_, _, children) -> List.exists non_empty children - in - if non_empty (Richpp.repr msg) then begin - let mark = `MARK mark in - Ideutils.insert_xml ~mark buffer ~tags msg; - buffer#insert ~iter:(buffer#get_iter_at_mark mark) "\n"; - push#call (level, msg) - end + let mark = `MARK mark in + Ideutils.insert_xml ~mark buffer ~tags (Richpp.richpp_of_pp msg); + buffer#insert ~iter:(buffer#get_iter_at_mark mark) "\n"; + push#call (level, msg) method add msg = self#push Feedback.Notice msg - method add_string s = self#add (Richpp.richpp_of_string s) + method add_string s = self#add (Pp.str s) method set msg = self#clear; self#add msg diff --git a/ide/wg_MessageView.mli b/ide/wg_MessageView.mli index 2d34533de..a71d345a5 100644 --- a/ide/wg_MessageView.mli +++ b/ide/wg_MessageView.mli @@ -18,9 +18,9 @@ class type message_view = inherit GObj.widget method connect : message_view_signals method clear : unit - method add : Richpp.richpp -> unit + method add : Pp.std_ppcmds -> unit method add_string : string -> unit - method set : Richpp.richpp -> unit + method set : Pp.std_ppcmds -> unit method push : Ideutils.logger (** same as [add], but with an explicit level instead of [Notice] *) method buffer : GText.buffer diff --git a/ide/wg_ProofView.ml b/ide/wg_ProofView.ml index 47c86045a..72aa9051a 100644 --- a/ide/wg_ProofView.ml +++ b/ide/wg_ProofView.ml @@ -84,7 +84,7 @@ let mode_tactic sel_cb (proof : #GText.view_skel) goals hints = match goals with let () = hook_tag_cb tag hint sel_cb on_hover in [tag], hints in - let () = insert_xml ~tags proof#buffer hyp in + let () = insert_xml ~tags proof#buffer (Richpp.richpp_of_pp hyp) in proof#buffer#insert "\n"; insert_hyp rem_hints hs in @@ -98,13 +98,13 @@ let mode_tactic sel_cb (proof : #GText.view_skel) goals hints = match goals with else [] in proof#buffer#insert (goal_str 1 goals_cnt); - insert_xml proof#buffer cur_goal; + insert_xml proof#buffer (Richpp.richpp_of_pp cur_goal); proof#buffer#insert "\n" in (* Insert remaining goals (no hypotheses) *) let fold_goal i _ { Interface.goal_ccl = g } = proof#buffer#insert (goal_str i goals_cnt); - insert_xml proof#buffer g; + insert_xml proof#buffer (Richpp.richpp_of_pp g); proof#buffer#insert "\n" in let () = Util.List.fold_left_i fold_goal 2 () rem_goals in @@ -144,7 +144,7 @@ let display mode (view : #GText.view_skel) goals hints evars = (* The proof is finished, with the exception of given up goals. *) view#buffer#insert "No more subgoals, but there are some goals you gave up:\n\n"; let iter goal = - insert_xml view#buffer goal.Interface.goal_ccl; + insert_xml view#buffer (Richpp.richpp_of_pp goal.Interface.goal_ccl); view#buffer#insert "\n" in List.iter iter given_up_goals; @@ -153,7 +153,7 @@ let display mode (view : #GText.view_skel) goals hints evars = (* All the goals have been resolved but those on the shelf. *) view#buffer#insert "All the remaining goals are on the shelf:\n\n"; let iter goal = - insert_xml view#buffer goal.Interface.goal_ccl; + insert_xml view#buffer (Richpp.richpp_of_pp goal.Interface.goal_ccl); view#buffer#insert "\n" in List.iter iter shelved_goals @@ -166,7 +166,7 @@ let display mode (view : #GText.view_skel) goals hints evars = view#buffer#insert "This subproof is complete, but there are some unfocused goals:\n\n"; let iter i goal = let () = view#buffer#insert (goal_str (succ i)) in - insert_xml view#buffer goal.Interface.goal_ccl; + insert_xml view#buffer (Richpp.richpp_of_pp goal.Interface.goal_ccl); view#buffer#insert "\n" in List.iteri iter bg diff --git a/ide/xmlprotocol.ml b/ide/xmlprotocol.ml index 65f44fdd3..08f23d3d4 100644 --- a/ide/xmlprotocol.ml +++ b/ide/xmlprotocol.ml @@ -97,6 +97,49 @@ let to_richpp xml = match xml with | Element ("richpp", [], [x]) -> Richpp.richpp_of_xml x | x -> raise Serialize.(Marshal_error("richpp",x)) +let of_box (ppb : Pp.block_type) = let open Pp in match ppb with + | Pp_hbox i -> constructor "ppbox" "hbox" [of_int i] + | Pp_vbox i -> constructor "ppbox" "vbox" [of_int i] + | Pp_hvbox i -> constructor "ppbox" "hvbox" [of_int i] + | Pp_hovbox i -> constructor "ppbox" "hovbox" [of_int i] + +let to_box = let open Pp in + do_match "ppbox" (fun s args -> match s with + | "hbox" -> Pp_hbox (to_int (singleton args)) + | "vbox" -> Pp_vbox (to_int (singleton args)) + | "hvbox" -> Pp_hvbox (to_int (singleton args)) + | "hovbox" -> Pp_hovbox (to_int (singleton args)) + | x -> raise (Marshal_error("*ppbox",PCData x)) + ) + +let rec of_pp (pp : Pp.std_ppcmds) = let open Pp in match pp with + | Ppcmd_empty -> constructor "ppdoc" "emtpy" [] + | Ppcmd_string s -> constructor "ppdoc" "string" [of_string s] + | Ppcmd_glue sl -> constructor "ppdoc" "glue" [of_list of_pp sl] + | Ppcmd_box (bt,s) -> constructor "ppdoc" "box" [of_pair of_box of_pp (bt,s)] + | Ppcmd_tag (t,s) -> constructor "ppdoc" "tag" [of_pair (of_list of_string) of_pp (t,s)] + | Ppcmd_print_break (i,j) + -> constructor "ppdoc" "break" [of_pair of_int of_int (i,j)] + | Ppcmd_force_newline -> constructor "ppdoc" "newline" [] + | Ppcmd_comment cmd -> constructor "ppdoc" "comment" [of_list of_string cmd] + + +let rec to_pp xpp = let open Pp in + do_match "ppdoc" (fun s args -> match s with + | "empty" -> Ppcmd_empty + | "string" -> Ppcmd_string (to_string (singleton args)) + | "glue" -> Ppcmd_glue (to_list to_pp (singleton args)) + | "box" -> let (bt,s) = to_pair to_box to_pp (singleton args) in + Ppcmd_box(bt,s) + | "tag" -> let (tg,s) = to_pair (to_list to_string) to_pp (singleton args) in + Ppcmd_tag(tg,s) + | "break" -> let (i,j) = to_pair to_int to_int (singleton args) in + Ppcmd_print_break(i, j) + | "newline" -> Ppcmd_force_newline + | "comment" -> Ppcmd_comment (to_list to_string (singleton args)) + | x -> raise (Marshal_error("*ppdoc",PCData x)) + ) xpp + let of_value f = function | Good x -> Element ("value", ["val", "good"], [f x]) | Fail (id,loc, msg) -> @@ -104,7 +147,7 @@ let of_value f = function | None -> [] | Some (s, e) -> [("loc_s", string_of_int s); ("loc_e", string_of_int e)] in let id = of_stateid id in - Element ("value", ["val", "fail"] @ loc, [id; of_richpp msg]) + Element ("value", ["val", "fail"] @ loc, [id; of_pp msg]) let to_value f = function | Element ("value", attrs, l) -> @@ -120,7 +163,7 @@ let to_value f = function in let (id, msg) = match l with [id; msg] -> (id, msg) | _ -> raise (Marshal_error("val",PCData "no id attribute")) in let id = to_stateid id in - let msg = to_richpp msg in + let msg = to_pp msg in Fail (id, loc, msg) else raise (Marshal_error("good or fail",PCData ans)) | x -> raise (Marshal_error("value",x)) @@ -147,15 +190,15 @@ let to_evar = function | x -> raise (Marshal_error("evar",x)) let of_goal g = - let hyp = of_list of_richpp g.goal_hyp in - let ccl = of_richpp g.goal_ccl in + let hyp = of_list of_pp g.goal_hyp in + let ccl = of_pp g.goal_ccl in let id = of_string g.goal_id in Element ("goal", [], [id; hyp; ccl]) let to_goal = function | Element ("goal", [], [id; hyp; ccl]) -> - let hyp = to_list to_richpp hyp in - let ccl = to_richpp ccl in - let id = to_string id in + let hyp = to_list to_pp hyp in + let ccl = to_pp ccl in + let id = to_string id in { goal_hyp = hyp; goal_ccl = ccl; goal_id = id; } | x -> raise (Marshal_error("goal",x)) @@ -344,8 +387,8 @@ end = struct Printf.sprintf "Still focussed: [%a]." pr_focus g.bg_goals else let pr_goal { goal_hyp = hyps; goal_ccl = goal } = - "[" ^ String.concat "; " (List.map Richpp.raw_print hyps) ^ " |- " ^ - Richpp.raw_print goal ^ "]" in + "[" ^ String.concat "; " (List.map Pp.string_of_ppcmds hyps) ^ " |- " ^ + Pp.string_of_ppcmds goal ^ "]" in String.concat " " (List.map pr_goal g.fg_goals) let pr_evar (e : evar) = "[" ^ e.evar_info ^ "]" let pr_status (s : status) = @@ -701,10 +744,10 @@ let to_call : xml -> unknown_call = let pr_value_gen pr = function | Good v -> "GOOD " ^ pr v - | Fail (id,None,str) -> "FAIL "^Stateid.to_string id^" ["^Richpp.raw_print str^"]" + | Fail (id,None,str) -> "FAIL "^Stateid.to_string id^" ["^ Pp.string_of_ppcmds str ^ "]" | Fail (id,Some(i,j),str) -> "FAIL "^Stateid.to_string id^ - " ("^string_of_int i^","^string_of_int j^")["^Richpp.raw_print str^"]" + " ("^string_of_int i^","^string_of_int j^")["^Pp.string_of_ppcmds str^"]" let pr_value v = pr_value_gen (fun _ -> "FIXME") v let pr_full_value : type a. a call -> a value -> string = fun call value -> match call with | Add _ -> pr_value_gen (print add_rty_t ) value @@ -760,7 +803,7 @@ let document to_string_fmt = (to_string_fmt (of_value (fun _ -> PCData "b") (Good ()))); Printf.printf "or:\n\n%s\n\nwhere the attributes loc_s and loc_c are optional.\n" (to_string_fmt (of_value (fun _ -> PCData "b") - (Fail (Stateid.initial,Some (15,34),Richpp.richpp_of_string "error message")))); + (Fail (Stateid.initial,Some (15,34), Pp.str "error message")))); document_type_encoding to_string_fmt (* Moved from feedback.mli : This is IDE specific and we don't want to @@ -787,12 +830,12 @@ let to_message_level = let of_message lvl loc msg = let lvl = of_message_level lvl in let xloc = of_option of_loc loc in - let content = of_richpp msg in + let content = of_pp msg in Xml_datatype.Element ("message", [], [lvl; xloc; content]) let to_message xml = match xml with | Xml_datatype.Element ("message", [], [lvl; xloc; content]) -> - Message(to_message_level lvl, to_option to_loc xloc, to_richpp content) + Message(to_message_level lvl, to_option to_loc xloc, to_pp content) | x -> raise (Marshal_error("message",x)) let to_feedback_content = do_match "feedback_content" (fun s a -> match s,a with diff --git a/ide/xmlprotocol.mli b/ide/xmlprotocol.mli index ca911178f..f6fae24d7 100644 --- a/ide/xmlprotocol.mli +++ b/ide/xmlprotocol.mli @@ -66,5 +66,6 @@ val of_feedback : Feedback.feedback -> xml val to_feedback : xml -> Feedback.feedback val is_feedback : xml -> bool -val of_message : Feedback.level -> Loc.t option -> Richpp.richpp -> xml +val of_message : Feedback.level -> Loc.t option -> Pp.std_ppcmds -> xml +(* val to_message : xml -> Feedback.message *) diff --git a/lib/cErrors.ml b/lib/cErrors.ml index a05964039..99b763602 100644 --- a/lib/cErrors.ml +++ b/lib/cErrors.ml @@ -16,16 +16,6 @@ let push = Backtrace.add_backtrace exception Anomaly of string option * std_ppcmds (* System errors *) -(* XXX: To move to common tagging functions in Pp, blocked on tag - * system cleanup as we cannot define generic error tags now. - * - * Anyways, tagging should not happen here, but in the specific - * listener to the msg_* stuff. - *) -let tag_err_str s = tag Ppstyle.error_tag (str s) ++ spc () -let err_str = tag_err_str "Error:" -let ann_str = tag_err_str "Anomaly:" - let _ = let pr = function | Anomaly (s, pp) -> Some ("\"Anomaly: " ^ string_of_ppcmds pp ^ "\"") @@ -102,7 +92,7 @@ let print_backtrace e = match Backtrace.get_backtrace e with let print_anomaly askreport e = if askreport then - hov 0 (ann_str ++ raw_anomaly e ++ spc () ++ + hov 0 (raw_anomaly e ++ spc () ++ strbrk "Please report at " ++ str Coq_config.wwwbugtracker ++ str ".") else @@ -124,7 +114,7 @@ let iprint_no_report (e, info) = let _ = register_handler begin function | UserError(s, pps) -> - hov 0 (err_str ++ where s ++ pps) + hov 0 (where s ++ pps) | _ -> raise Unhandled end diff --git a/lib/clib.mllib b/lib/clib.mllib index 1e33173ee..5a5f6afd3 100644 --- a/lib/clib.mllib +++ b/lib/clib.mllib @@ -15,7 +15,6 @@ Store Exninfo Backtrace IStream -Pp_control Flags Control Loc @@ -28,9 +27,8 @@ CStack Util Stateid Pp -Ppstyle -Richpp Feedback +Ppstyle CUnix Envars Aux_file diff --git a/lib/feedback.ml b/lib/feedback.ml index 852eec2f2..31677ecfc 100644 --- a/lib/feedback.ml +++ b/lib/feedback.ml @@ -35,7 +35,7 @@ type feedback_content = (* Extra metadata *) | Custom of Loc.t * string * xml (* Generic messages *) - | Message of level * Loc.t option * Richpp.richpp + | Message of level * Loc.t option * Pp.std_ppcmds type feedback = { id : edit_or_state_id; @@ -45,140 +45,6 @@ type feedback = { let default_route = 0 -(** Feedback and logging *) -open Pp -open Pp_control - -type logger = ?loc:Loc.t -> level -> std_ppcmds -> unit - -let msgnl_with ?pp_tag fmt strm = - pp_with ?pp_tag fmt (strm ++ fnl ()); - Format.pp_print_flush fmt () - -(* XXX: This is really painful! *) -module Emacs = struct - - (* Special chars for emacs, to detect warnings inside goal output *) - let emacs_quote_start = String.make 1 (Char.chr 254) - let emacs_quote_end = String.make 1 (Char.chr 255) - - let emacs_quote_err g = - hov 0 (str emacs_quote_start ++ g ++ str emacs_quote_end) - - let emacs_quote_info_start = "<infomsg>" - let emacs_quote_info_end = "</infomsg>" - - let emacs_quote_info g = - hov 0 (str emacs_quote_info_start++ brk(0,0) ++ g ++ brk(0,0) ++ str emacs_quote_info_end) - -end - -open Emacs - -let dbg_str = tag Ppstyle.debug_tag (str "Debug:") ++ spc () -let info_str = mt () -let warn_str = tag Ppstyle.warning_tag (str "Warning:") ++ spc () -let err_str = tag Ppstyle.error_tag (str "Error:" ) ++ spc () - -let make_body quoter info ?loc s = - let loc = Option.cata Pp.pr_loc (Pp.mt ()) loc in - quoter (hov 0 (loc ++ info ++ s)) - -(* Generic logger *) -let gen_logger dbg err ?pp_tag ?loc level msg = match level with - | Debug -> msgnl_with ?pp_tag !std_ft (make_body dbg dbg_str ?loc msg) - | Info -> msgnl_with ?pp_tag !std_ft (make_body dbg info_str ?loc msg) - | Notice -> msgnl_with ?pp_tag !std_ft msg - | Warning -> Flags.if_warn (fun () -> - msgnl_with ?pp_tag !err_ft (make_body err warn_str ?loc msg)) () - | Error -> msgnl_with ?pp_tag !err_ft (make_body err err_str ?loc msg) - -(* We provide a generic clear_log_backend callback for backends - wanting to do clenaup after the print. -*) -let std_logger_tag = ref None -let std_logger_cleanup = ref (fun () -> ()) - -let std_logger ?loc level msg = - gen_logger (fun x -> x) (fun x -> x) ?pp_tag:!std_logger_tag ?loc level msg; - !std_logger_cleanup () - -(* Rules for emacs: - - Debug/info: emacs_quote_info - - Warning/Error: emacs_quote_err - - Notice: unquoted - - Note the inconsistency. - *) -let emacs_logger = gen_logger emacs_quote_info emacs_quote_err ?pp_tag:None - -(** Color logging. Moved from pp_style, it may need some more refactoring *) - -(** Not thread-safe. We should put a lock somewhere if we print from - different threads. Do we? *) -let make_style_stack () = - (** Default tag is to reset everything *) - let empty = Terminal.make () in - let default_tag = Terminal.({ - fg_color = Some `DEFAULT; - bg_color = Some `DEFAULT; - bold = Some false; - italic = Some false; - underline = Some false; - negative = Some false; - }) - in - let style_stack = ref [] in - let peek () = match !style_stack with - | [] -> default_tag (** Anomalous case, but for robustness *) - | st :: _ -> st - in - let push tag = - let style = match Ppstyle.get_style_format tag with - | None -> empty - | Some st -> st - in - (** Use the merging of the latest tag and the one being currently pushed. - This may be useful if for instance the latest tag changes the background and - the current one the foreground, so that the two effects are additioned. *) - let style = Terminal.merge (peek ()) style in - style_stack := style :: !style_stack; - Terminal.eval style - in - let pop _ = match !style_stack with - | [] -> (** Something went wrong, we fallback *) - Terminal.eval default_tag - | _ :: rem -> style_stack := rem; - Terminal.eval (peek ()) - in - let clear () = style_stack := [] in - push, pop, clear - -let init_color_output () = - let open Pp_control in - let push_tag, pop_tag, clear_tag = make_style_stack () in - std_logger_cleanup := clear_tag; - std_logger_tag := Some Ppstyle.to_format; - let tag_handler = { - Format.mark_open_tag = push_tag; - Format.mark_close_tag = pop_tag; - Format.print_open_tag = ignore; - Format.print_close_tag = ignore; - } in - Format.pp_set_mark_tags !std_ft true; - Format.pp_set_mark_tags !err_ft true; - Format.pp_set_formatter_tag_functions !std_ft tag_handler; - Format.pp_set_formatter_tag_functions !err_ft tag_handler - -let logger = ref std_logger -let set_logger l = logger := l - -let msg_info ?loc x = !logger ?loc Info x -let msg_notice ?loc x = !logger ?loc Notice x -let msg_warning ?loc x = !logger ?loc Warning x -let msg_error ?loc x = !logger ?loc Error x -let msg_debug ?loc x = !logger ?loc Debug x - (** Feeders *) let feeders : (int, feedback -> unit) Hashtbl.t = Hashtbl.create 7 @@ -190,11 +56,6 @@ let add_feeder = let del_feeder fid = Hashtbl.remove feeders fid -let debug_feeder = function - | { contents = Message (Debug, loc, pp) } -> - msg_debug ?loc (Pp.str (Richpp.raw_print pp)) - | _ -> () - let feedback_id = ref (Edit 0) let feedback_route = ref default_route @@ -209,32 +70,16 @@ let feedback ?id ?route what = } in Hashtbl.iter (fun _ f -> f m) feeders +(* Logging messages *) let feedback_logger ?loc lvl msg = - feedback ~route:!feedback_route ~id:!feedback_id - (Message (lvl, loc, Richpp.richpp_of_pp msg)) + feedback ~route:!feedback_route ~id:!feedback_id (Message (lvl, loc, msg)) -(* Output to file *) -let ft_logger old_logger ft ?loc level mesg = - let id x = x in - match level with - | Debug -> msgnl_with ft (make_body id dbg_str mesg) - | Info -> msgnl_with ft (make_body id info_str mesg) - | Notice -> msgnl_with ft mesg - | Warning -> old_logger ?loc level mesg - | Error -> old_logger ?loc level mesg - -let with_output_to_file fname func input = - let old_logger = !logger in - let channel = open_out (String.concat "." [fname; "out"]) in - logger := ft_logger old_logger (Format.formatter_of_out_channel channel); - try - let output = func input in - logger := old_logger; - close_out channel; - output - with reraise -> - let reraise = Backtrace.add_backtrace reraise in - logger := old_logger; - close_out channel; - Exninfo.iraise reraise +let msg_info ?loc x = feedback_logger ?loc Info x +let msg_notice ?loc x = feedback_logger ?loc Notice x +let msg_warning ?loc x = feedback_logger ?loc Warning x +let msg_error ?loc x = feedback_logger ?loc Error x +let msg_debug ?loc x = feedback_logger ?loc Debug x +let debug_feeder = function + | { contents = Message (Debug, loc, pp) } -> msg_debug ?loc pp + | _ -> () diff --git a/lib/feedback.mli b/lib/feedback.mli index 8eae31588..3fb7c0039 100644 --- a/lib/feedback.mli +++ b/lib/feedback.mli @@ -8,7 +8,7 @@ open Xml_datatype -(* Old plain messages (used to be in Pp) *) +(* Legacy-style logging messages (used to be in Pp) *) type level = | Debug | Info @@ -16,7 +16,6 @@ type level = | Warning | Error - (** Coq "semantic" infos obtained during parsing/execution *) type edit_id = int type state_id = Stateid.t @@ -44,7 +43,7 @@ type feedback_content = (* Extra metadata *) | Custom of Loc.t * string * xml (* Generic messages *) - | Message of level * Loc.t option * Richpp.richpp + | Message of level * Loc.t option * Pp.std_ppcmds type feedback = { id : edit_or_state_id; (* The document part concerned *) @@ -53,32 +52,12 @@ type feedback = { } (** {6 Feedback sent, even asynchronously, to the user interface} *) - -(** Moved here from pp.ml *) - (* Morally the parser gets a string and an edit_id, and gives back an AST. * Feedbacks during the parsing phase are attached to this edit_id. * The interpreter assignes an exec_id to the ast, and feedbacks happening * during interpretation are attached to the exec_id. * Only one among state_id and edit_id can be provided. *) -(** A [logger] takes a level plus a pretty printing doc and logs it *) -type logger = ?loc:Loc.t -> level -> Pp.std_ppcmds -> unit - -(** [set_logger l] makes the [msg_*] to use [l] for logging *) -val set_logger : logger -> unit - -(** [std_logger] standard logger to [stdout/stderr] *) -val std_logger : logger - -(** [init_color_output ()] Enable color in the std_logger *) -val init_color_output : unit -> unit - -(** [feedback_logger] will produce feedback messages instead IO events *) -val feedback_logger : logger -val emacs_logger : logger - - (** [add_feeder f] adds a feeder listiner [f], returning its id *) val add_feeder : (feedback -> unit) -> int @@ -97,10 +76,6 @@ val feedback : (** [set_id_for_feedback route id] Set the defaults for feedback *) val set_id_for_feedback : ?route:route_id -> edit_or_state_id -> unit -(** [with_output_to_file file f x] executes [f x] with logging - redirected to a file [file] *) -val with_output_to_file : string -> ('a -> 'b) -> 'a -> 'b - (** {6 output functions} [msg_notice] do not put any decoration on output by default. If @@ -128,7 +103,3 @@ val msg_error : ?loc:Loc.t -> Pp.std_ppcmds -> unit val msg_debug : ?loc:Loc.t -> Pp.std_ppcmds -> unit (** For debugging purposes *) - - - - @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Pp_control - (* The different kinds of blocks are: \begin{description} \item[hbox:] Horizontal block no line breaking; @@ -178,10 +176,9 @@ let pp_with ?pp_tag ft = | Ppcmd_glue sl -> List.iter pp_cmd sl | Ppcmd_string str -> let n = utf8_length str in pp_print_as ft n str - | Ppcmd_box(bty,ss) -> (* Prevent evaluation of the stream! *) - cpp_open_box bty ; - if not (Format.over_max_boxes ()) then pp_cmd ss; - Format.pp_close_box ft () + | Ppcmd_box(bty,ss) -> cpp_open_box bty ; + if not (over_max_boxes ()) then pp_cmd ss; + pp_close_box ft () | Ppcmd_print_break(m,n) -> pp_print_break ft m n | Ppcmd_force_newline -> pp_force_newline ft () | Ppcmd_comment coms -> List.iter (pr_com ft) coms diff --git a/lib/pp.mli b/lib/pp.mli index 5bf5391d3..12747d3a1 100644 --- a/lib/pp.mli +++ b/lib/pp.mli @@ -8,6 +8,30 @@ (** Coq document type. *) +(** Pretty printing guidelines ******************************************) +(* *) +(* std_ppcmds is the main pretty printing datatype in he Coq. Documents *) +(* are composed laying out boxes, and users can add arbitrary metadata *) +(* that backends are free to interpret. *) +(* *) +(* The datatype is public to allow serialization or advanced uses, *) +(* regular users are _strongly_ encouraged to use the top-level *) +(* functions to manipulate the type. *) +(* *) +(* Box order and number is indeed an important factor. Users should try *) +(* to create a proper amount of boxes. Also, the ++ operator provides *) +(* "efficient" concatenation, but directly using a list is preferred. *) +(* *) +(* That is to say, this: *) +(* *) +(* `hov [str "Term"; hov (pr_term t); str "is defined"]` *) +(* *) +(* is preferred to: *) +(* *) +(* `hov (str "Term" ++ hov (pr_term t) ++ str "is defined")` *) +(* *) +(************************************************************************) + (* XXX: Improve and add attributes *) type pp_tag = string list diff --git a/lib/pp_control.ml b/lib/pp_control.ml deleted file mode 100644 index ab8dc0798..000000000 --- a/lib/pp_control.ml +++ /dev/null @@ -1,93 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(* Parameters of pretty-printing *) - -type pp_global_params = { - margin : int; - max_indent : int; - max_depth : int; - ellipsis : string } - -(* Default parameters of pretty-printing *) - -let dflt_gp = { - margin = 78; - max_indent = 50; - max_depth = 50; - ellipsis = "..." } - -(* A deeper pretty-printer to print proof scripts *) - -let deep_gp = { - margin = 78; - max_indent = 50; - max_depth = 10000; - ellipsis = "..." } - -(* set_gp : Format.formatter -> pp_global_params -> unit - * set the parameters of a formatter *) - -let set_gp ft gp = - Format.pp_set_margin ft gp.margin ; - Format.pp_set_max_indent ft gp.max_indent ; - Format.pp_set_max_boxes ft gp.max_depth ; - Format.pp_set_ellipsis_text ft gp.ellipsis - -let set_dflt_gp ft = set_gp ft dflt_gp - -let get_gp ft = - { margin = Format.pp_get_margin ft (); - max_indent = Format.pp_get_max_indent ft (); - max_depth = Format.pp_get_max_boxes ft (); - ellipsis = Format.pp_get_ellipsis_text ft () } - -(* with_fp : 'a pp_formatter_params -> Format.formatter - * returns of formatter for given formatter functions *) - -let with_fp chan out_function flush_function = - let ft = Format.make_formatter out_function flush_function in - Format.pp_set_formatter_out_channel ft chan; - ft - -(* Output on a channel ch *) - -let with_output_to ch = - let ft = with_fp ch (output_substring ch) (fun () -> flush ch) in - set_gp ft deep_gp; - ft - -let std_ft = ref Format.std_formatter -let _ = set_dflt_gp !std_ft - -let err_ft = ref Format.err_formatter -let _ = set_gp !err_ft deep_gp - -let deep_ft = ref (with_output_to stdout) -let _ = set_gp !deep_ft deep_gp - -(* For parametrization through vernacular *) -let default = Format.pp_get_max_boxes !std_ft () -let default_margin = Format.pp_get_margin !std_ft () - -let get_depth_boxes () = Some (Format.pp_get_max_boxes !std_ft ()) -let set_depth_boxes v = - Format.pp_set_max_boxes !std_ft (match v with None -> default | Some v -> v) - -let get_margin () = Some (Format.pp_get_margin !std_ft ()) -let set_margin v = - let v = match v with None -> default_margin | Some v -> v in - Format.pp_set_margin Format.str_formatter v; - Format.pp_set_margin !std_ft v; - Format.pp_set_margin !deep_ft v; - (* Heuristic, based on usage: the column on the right of max_indent - column is 20% of width, capped to 30 characters *) - let m = max (64 * v / 100) (v-30) in - Format.pp_set_max_indent Format.str_formatter m; - Format.pp_set_max_indent !std_ft m; - Format.pp_set_max_indent !deep_ft m diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml index e019bb3c2..ee623c5ca 100644 --- a/plugins/extraction/extract_env.ml +++ b/plugins/extraction/extract_env.ml @@ -472,13 +472,14 @@ let formatter dry file = if dry then Format.make_formatter (fun _ _ _ -> ()) (fun _ -> ()) else match file with - | Some f -> Pp_control.with_output_to f + | Some f -> Topfmt.with_output_to f | None -> Format.formatter_of_buffer buf in + (* XXX: Fixme, this shouldn't depend on Topfmt *) (* We never want to see ellipsis ... in extracted code *) Format.pp_set_max_boxes ft max_int; (* We reuse the width information given via "Set Printing Width" *) - (match Pp_control.get_margin () with + (match Topfmt.get_margin () with | None -> () | Some i -> Format.pp_set_margin ft i; diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml index 8acc3c233..28548ecee 100644 --- a/stm/asyncTaskQueue.ml +++ b/stm/asyncTaskQueue.ml @@ -298,18 +298,11 @@ module Make(T : Task) = struct let slave_handshake () = Pool.worker_handshake (Option.get !slave_ic) (Option.get !slave_oc) - let pp_pid pp = - (* Breaking all abstraction barriers... very nice *) - let get_xml pp = match Richpp.repr pp with - | Xml_datatype.Element("_", [], xml) -> xml - | _ -> assert false in - Richpp.richpp_of_xml (Xml_datatype.Element("_", [], - get_xml (Richpp.richpp_of_pp Pp.(str (System.process_id ()^ " "))) @ - get_xml pp)) + let pp_pid pp = Pp.(str (System.process_id () ^ " ") ++ pp) let debug_with_pid = Feedback.(function | { contents = Message(Debug, loc, pp) } as fb -> - { fb with contents = Message(Debug,loc,pp_pid pp) } + { fb with contents = Message(Debug,loc, pp_pid pp) } | x -> x) let main_loop () = @@ -317,7 +310,6 @@ module Make(T : Task) = struct let slave_feeder oc fb = Marshal.to_channel oc (RespFeedback (debug_with_pid fb)) []; flush oc in Feedback.add_feeder (fun x -> slave_feeder (Option.get !slave_oc) x); - Feedback.set_logger Feedback.feedback_logger; (* We ask master to allocate universe identifiers *) Universes.set_remote_new_univ_level (bufferize (fun () -> marshal_response (Option.get !slave_oc) RespGetCounterNewUnivLevel; diff --git a/stm/stm.ml b/stm/stm.ml index e56db4090..75872d633 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -11,10 +11,6 @@ let pr_err s = Printf.eprintf "%s] %s\n" (System.process_id ()) s; flush stderr let prerr_endline s = if false then begin pr_err (s ()) end else () let prerr_debug s = if !Flags.debug then begin pr_err (s ()) end else () -(* Opening ppvernac below aliases Richpp, see PR#185 *) -let pp_to_richpp = Richpp.richpp_of_pp -let str_to_richpp = Richpp.richpp_of_string - open Vernacexpr open CErrors open Pp @@ -26,7 +22,7 @@ open Feedback let execution_error state_id loc msg = feedback ~id:(State state_id) - (Message (Error, Some loc, pp_to_richpp msg)) + (Message (Error, Some loc, msg)) module Hooks = struct @@ -48,7 +44,7 @@ let forward_feedback, forward_feedback_hook = let parse_error, parse_error_hook = Hook.make ~default:(fun id loc msg -> - feedback ~id (Message(Error, Some loc, pp_to_richpp msg))) () + feedback ~id (Message(Error, Some loc, msg))) () let unreachable_state, unreachable_state_hook = Hook.make ~default:(fun _ _ -> ()) () @@ -1945,7 +1941,7 @@ end = struct (* {{{ *) feedback ~id:(State r_for) Processed with e when CErrors.noncritical e -> let e = CErrors.push e in - let msg = pp_to_richpp (iprint e) in + let msg = iprint e in feedback ~id:(State r_for) (Message (Error, None, msg)) let name_of_task { t_what } = string_of_ppcmds (pr_ast t_what) diff --git a/test-suite/output/Arguments.out b/test-suite/output/Arguments.out index a2ee2d4c8..979396969 100644 --- a/test-suite/output/Arguments.out +++ b/test-suite/output/Arguments.out @@ -97,8 +97,8 @@ Expands to: Constant Top.f forall w : r, w 3 true = tt : Prop The command has indeed failed with message: -Error: Unknown interpretation for notation "$". +Unknown interpretation for notation "$". w 3 true = tt : Prop The command has indeed failed with message: -Error: Extra arguments: _, _. +Extra arguments: _, _. diff --git a/test-suite/output/Arguments_renaming.out b/test-suite/output/Arguments_renaming.out index b084ad498..4df21ae35 100644 --- a/test-suite/output/Arguments_renaming.out +++ b/test-suite/output/Arguments_renaming.out @@ -1,5 +1,5 @@ The command has indeed failed with message: -Error: To rename arguments the "rename" flag must be specified. +To rename arguments the "rename" flag must be specified. Argument A renamed to B. File "stdin", line 2, characters 0-25: Warning: This command is just asserting the names of arguments of identity. @@ -103,15 +103,15 @@ Expands to: Constant Top.myplus @myplus : forall Z : Type, Z -> nat -> nat -> nat The command has indeed failed with message: -Error: Argument lists should agree on the names they provide. +Argument lists should agree on the names they provide. The command has indeed failed with message: -Error: Sequences of implicit arguments must be of different lengths. +Sequences of implicit arguments must be of different lengths. The command has indeed failed with message: -Error: Some argument names are duplicated: F +Some argument names are duplicated: F The command has indeed failed with message: -Error: Argument z cannot be declared implicit. +Argument z cannot be declared implicit. The command has indeed failed with message: -Error: Extra arguments: y. +Extra arguments: y. The command has indeed failed with message: -Error: To rename arguments the "rename" flag must be specified. +To rename arguments the "rename" flag must be specified. Argument A renamed to R. diff --git a/test-suite/output/Errors.out b/test-suite/output/Errors.out index 06a6b2d15..38d055b28 100644 --- a/test-suite/output/Errors.out +++ b/test-suite/output/Errors.out @@ -7,4 +7,4 @@ In nested Ltac calls to "f" and "apply x", last call failed. Unable to unify "nat" with "True". The command has indeed failed with message: Ltac call to "instantiate ( (ident) := (lglob) )" failed. -Error: Instance is not well-typed in the environment of ?x. +Instance is not well-typed in the environment of ?x. diff --git a/test-suite/output/FunExt.out b/test-suite/output/FunExt.out index c6786c72f..8d2a125c1 100644 --- a/test-suite/output/FunExt.out +++ b/test-suite/output/FunExt.out @@ -16,4 +16,4 @@ Tactic failure: Already an intensional equality. The command has indeed failed with message: In nested Ltac calls to "extensionality in (var)" and "clearbody (ne_var_list)", last call failed. -Error: Hypothesis e depends on the body of H' +Hypothesis e depends on the body of H' diff --git a/test-suite/output/Notations.out b/test-suite/output/Notations.out index 26eaca827..9d106d2da 100644 --- a/test-suite/output/Notations.out +++ b/test-suite/output/Notations.out @@ -41,29 +41,29 @@ fun x : nat => ifn x is succ n then n else 0 -4 : Z The command has indeed failed with message: -Error: x should not be bound in a recursive pattern of the right-hand side. +x should not be bound in a recursive pattern of the right-hand side. The command has indeed failed with message: -Error: in the right-hand side, y and z should appear in +in the right-hand side, y and z should appear in term position as part of a recursive pattern. The command has indeed failed with message: The reference w was not found in the current environment. The command has indeed failed with message: -Error: in the right-hand side, y and z should appear in +in the right-hand side, y and z should appear in term position as part of a recursive pattern. The command has indeed failed with message: -Error: z is expected to occur in binding position in the right-hand side. +z is expected to occur in binding position in the right-hand side. The command has indeed failed with message: -Error: as y is a non-closed binder, no such "," is allowed to occur. +as y is a non-closed binder, no such "," is allowed to occur. The command has indeed failed with message: -Error: Cannot find where the recursive pattern starts. +Cannot find where the recursive pattern starts. The command has indeed failed with message: -Error: Cannot find where the recursive pattern starts. +Cannot find where the recursive pattern starts. The command has indeed failed with message: -Error: Cannot find where the recursive pattern starts. +Cannot find where the recursive pattern starts. The command has indeed failed with message: -Error: Cannot find where the recursive pattern starts. +Cannot find where the recursive pattern starts. The command has indeed failed with message: -Error: Both ends of the recursive pattern are the same. +Both ends of the recursive pattern are the same. SUM (nat * nat) nat : Set FST (0; 1) diff --git a/test-suite/output/ltac.out b/test-suite/output/ltac.out index 1ff09e3af..35c3057d8 100644 --- a/test-suite/output/ltac.out +++ b/test-suite/output/ltac.out @@ -1,5 +1,4 @@ The command has indeed failed with message: -Error: Ltac variable y depends on pattern variable name z which is not bound in current context. Ltac f x y z := symmetry in x, y; auto with z; auto; intros **; clearbody x; generalize @@ -22,11 +21,11 @@ The term "I" has type "True" while it is expected to have type "False". The command has indeed failed with message: In nested Ltac calls to "h" and "injection (destruction_arg)", last call failed. -Error: No primitive equality found. +No primitive equality found. The command has indeed failed with message: In nested Ltac calls to "h" and "injection (destruction_arg)", last call failed. -Error: No primitive equality found. +No primitive equality found. Hx nat nat diff --git a/test-suite/output/ltac_missing_args.out b/test-suite/output/ltac_missing_args.out index ae3fd7acc..172612405 100644 --- a/test-suite/output/ltac_missing_args.out +++ b/test-suite/output/ltac_missing_args.out @@ -1,21 +1,20 @@ The command has indeed failed with message: -Error: A fully applied tactic is expected: missing argument for variable x. +A fully applied tactic is expected: missing argument for variable x. The command has indeed failed with message: -Error: A fully applied tactic is expected: missing argument for variable x. +A fully applied tactic is expected: missing argument for variable x. The command has indeed failed with message: -Error: A fully applied tactic is expected: -missing arguments for variables y and _. +A fully applied tactic is expected: missing arguments for variables y and _. The command has indeed failed with message: -Error: A fully applied tactic is expected: missing argument for variable x. +A fully applied tactic is expected: missing argument for variable x. The command has indeed failed with message: -Error: A fully applied tactic is expected: missing argument for variable x. +A fully applied tactic is expected: missing argument for variable x. The command has indeed failed with message: -Error: A fully applied tactic is expected: missing argument for variable _. +A fully applied tactic is expected: missing argument for variable _. The command has indeed failed with message: -Error: A fully applied tactic is expected: missing argument for variable _. +A fully applied tactic is expected: missing argument for variable _. The command has indeed failed with message: -Error: A fully applied tactic is expected: missing argument for variable _. +A fully applied tactic is expected: missing argument for variable _. The command has indeed failed with message: -Error: A fully applied tactic is expected: missing argument for variable x. +A fully applied tactic is expected: missing argument for variable x. The command has indeed failed with message: -Error: A fully applied tactic is expected: missing argument for variable x. +A fully applied tactic is expected: missing argument for variable x. diff --git a/tools/fake_ide.ml b/tools/fake_ide.ml index 23c111b37..e89f19041 100644 --- a/tools/fake_ide.ml +++ b/tools/fake_ide.ml @@ -29,7 +29,7 @@ let error_xml s = exit 1 let logger level content = - Printf.eprintf "%a\n%! " print_xml (Richpp.repr content) + Printf.eprintf "%a\n%! " print_xml Richpp.(content |> richpp_of_pp |> repr) let base_eval_call ?(print=true) ?(fail=true) call coqtop = if print then prerr_endline (Xmlprotocol.pr_call call); @@ -44,8 +44,8 @@ let base_eval_call ?(print=true) ?(fail=true) call coqtop = let res = loop () in if print then prerr_endline (Xmlprotocol.pr_full_value call res); match res with - | Interface.Fail (_,_,s) when fail -> error_xml (Richpp.repr s) - | Interface.Fail (_,_,s) as x -> Printf.eprintf "%a\n%!" print_xml (Richpp.repr s); x + | Interface.Fail (_,_,s) when fail -> error_xml Richpp.(s |> richpp_of_pp |> repr) + | Interface.Fail (_,_,s) as x -> Printf.eprintf "%a\n%!" print_xml Richpp.(s |> richpp_of_pp |> repr); x | x -> x let eval_call c q = ignore(base_eval_call c q) @@ -194,7 +194,7 @@ let print_document () = module GUILogic = struct let after_add = function - | Interface.Fail (_,_,s) -> error_xml (Richpp.repr s) + | Interface.Fail (_,_,s) -> error_xml Richpp.(repr (richpp_of_pp s)) | Interface.Good (id, (Util.Inl (), _)) -> Document.assign_tip_id doc id | Interface.Good (id, (Util.Inr tip, _)) -> @@ -206,7 +206,7 @@ module GUILogic = struct let at id id' _ = Stateid.equal id' id let after_edit_at (id,need_unfocus) = function - | Interface.Fail (_,_,s) -> error_xml (Richpp.repr s) + | Interface.Fail (_,_,s) -> error_xml Richpp.(repr (richpp_of_pp s)) | Interface.Good (Util.Inl ()) -> if need_unfocus then Document.unfocus doc; ignore(Document.cut_at doc id); @@ -329,7 +329,7 @@ let main = let finish () = match base_eval_call (Xmlprotocol.status true) coq with | Interface.Good _ -> exit 0 - | Interface.Fail (_,_,s) -> error_xml (Richpp.repr s) in + | Interface.Fail (_,_,s) -> error_xml Richpp.(repr (richpp_of_pp s)) in (* The main loop *) init (); while true do diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml index 2cb608326..e9506803d 100644 --- a/toplevel/coqloop.ml +++ b/toplevel/coqloop.ml @@ -14,8 +14,7 @@ open Vernac open Pcoq let top_stderr x = - pp_with ~pp_tag:Ppstyle.to_format !Pp_control.err_ft x; - Format.pp_print_flush !Pp_control.err_ft () + Format.fprintf !Topfmt.err_ft "@[%a@]%!" (pp_with ~pp_tag:Ppstyle.to_format) x (* A buffer for the character read from a channel. We store the command * entered to be able to report errors without pretty-printing. *) @@ -253,7 +252,8 @@ let print_toplevel_error (e, info) = else mt () else print_location_in_file loc in - locmsg ++ CErrors.iprint (e, info) + let hdr msg = hov 0 (tag Ppstyle.error_tag (str "Error:") ++ spc () ++ msg) in + locmsg ++ hdr (CErrors.iprint (e, info)) (* Read the input stream until a dot is encountered *) let parse_to_dot = @@ -285,6 +285,33 @@ let read_sentence input = discard_to_dot (); iraise reraise +(** Coqloop Console feedback handler *) +let coqloop_feed (fb : Feedback.feedback) = let open Feedback in + match fb.contents with + | Processed -> () + | Incomplete -> () + | Complete -> () + | ProcessingIn _ -> () + | InProgress _ -> () + | WorkerStatus (_,_) -> () + | AddedAxiom -> () + | GlobRef (_,_,_,_,_) -> () + | GlobDef (_,_,_,_) -> () + | FileDependency (_,_) -> () + | FileLoaded (_,_) -> () + | Custom (_,_,_) -> () + | Message (Error,loc,msg) -> + (* We ignore errors here as we (still) have a different error + printer for the toplevel. It is hard to solve due the many + error paths presents, and the different compromise of feedback + error forwaring in the stm depending on the mode *) + () + | Message (lvl,loc,msg) -> + if !Flags.print_emacs then + Topfmt.emacs_logger ?loc lvl msg + else + Topfmt.std_logger ?loc lvl msg + (** [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. @@ -307,12 +334,13 @@ let do_vernac () = top_stderr (fnl ()); raise CErrors.Quit | CErrors.Drop -> (* Last chance *) if Mltop.is_ocaml_top() then raise CErrors.Drop - else Feedback.msg_error (str"There is no ML toplevel.") + else top_stderr (str "There is no ML toplevel.") | any -> + (** Main error printer, note that this didn't it the "emacs" + legacy path. *) let any = CErrors.push any in let msg = print_toplevel_error any ++ fnl () in - pp_with !Pp_control.std_ft msg; - Format.pp_print_flush !Pp_control.std_ft () + top_stderr msg (** Main coq loop : read vernacular expressions until Drop is entered. Ctrl-C is handled internally as Sys.Break instead of aborting Coq. @@ -320,22 +348,13 @@ let do_vernac () = exit the loop are Drop and Quit. Any other exception there indicates an issue with [print_toplevel_error] above. *) -(* -let feed_emacs = function - | { Interface.id = Interface.State id; - Interface.content = Interface.GlobRef (_,a,_,c,_) } -> - prerr_endline ("<info>" ^"<id>"^Stateid.to_string id ^"</id>" - ^a^" "^c^ "</info>") - | _ -> () -*) - (* Flush in a compatible order with 8.5 *) (* This mimics the semantics of the old Pp.flush_all *) let loop_flush_all () = Pervasives.flush stderr; Pervasives.flush stdout; - Format.pp_print_flush !Pp_control.std_ft (); - Format.pp_print_flush !Pp_control.err_ft () + Format.pp_print_flush !Topfmt.std_ft (); + Format.pp_print_flush !Topfmt.err_ft () let rec loop () = Sys.catch_break true; @@ -348,9 +367,9 @@ let rec loop () = | CErrors.Drop -> () | CErrors.Quit -> exit 0 | any -> - Feedback.msg_error (str"Anomaly: main loop exited with exception: " ++ - str (Printexc.to_string any) ++ - fnl() ++ - str"Please report" ++ - strbrk" at " ++ str Coq_config.wwwbugtracker ++ str "."); + 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 () diff --git a/toplevel/coqloop.mli b/toplevel/coqloop.mli index d248f2f70..eb61084e0 100644 --- a/toplevel/coqloop.mli +++ b/toplevel/coqloop.mli @@ -32,6 +32,8 @@ val set_prompt : (unit -> string) -> unit val print_toplevel_error : Exninfo.iexn -> std_ppcmds +val coqloop_feed : Feedback.feedback -> unit + (** Parse and execute one vernac command. *) val do_vernac : unit -> unit diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 541c1fd1b..823d05580 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -61,7 +61,7 @@ let init_color () = match colors with | None -> (** Default colors *) - Feedback.init_color_output () + Topfmt.init_color_output () | Some "" -> (** No color output *) () @@ -69,7 +69,7 @@ let init_color () = (** Overwrite all colors *) Ppstyle.clear_styles (); Ppstyle.parse_config s; - Feedback.init_color_output () + Topfmt.init_color_output () end let toploop_init = ref begin fun x -> @@ -78,15 +78,27 @@ let toploop_init = ref begin fun x -> x end -let toploop_run = ref (fun () -> +(* Feedback received in the init stage, this is different as the STM + will not be generally be initialized, thus stateid, etc... may be + bogus. For now we just print to the console too *) +let coqtop_init_feed = Coqloop.coqloop_feed + +(* Default toplevel loop *) +let console_toploop_run () = + (* We initialize the console only if we run the toploop_run *) + let tl_feed = Feedback.add_feeder Coqloop.coqloop_feed in if Dumpglob.dump () then begin if_verbose warning "Dumpglob cannot be used in interactive mode."; Dumpglob.noglob () end; Coqloop.loop(); + (* We remove the feeder but it could be ok not to do so *) + Feedback.del_feeder tl_feed; (* Initialise and launch the Ocaml toplevel *) Coqinit.init_ocaml_path(); - Mltop.ocaml_toploop()) + Mltop.ocaml_toploop() + +let toploop_run = ref console_toploop_run let output_context = ref false @@ -228,7 +240,6 @@ let compile_files () = if !compile_list == [] then () else let init_state = States.freeze ~marshallable:`No in - Feedback.(add_feeder debug_feeder); List.iter (fun vf -> States.unfreeze init_state; compile_file vf) @@ -240,7 +251,6 @@ let set_emacs () = if not (Option.is_empty !toploop) then error "Flag -emacs is incompatible with a custom toplevel loop"; Flags.print_emacs := true; - Feedback.(set_logger emacs_logger); Vernacentries.qed_display_script := false; color := `OFF @@ -435,7 +445,7 @@ let get_native_name s = with the appropriate error code *) let fatal_error info anomaly = let msg = info ++ fnl () in - Format.fprintf !Topfmt.err_ft "@[%a@]%!" pp_with msg; + Format.fprintf !Topfmt.err_ft "@[%a@]%!" (pp_with ?pp_tag:None) msg; exit (if anomaly then 129 else 1) let parse_args arglist = @@ -609,6 +619,7 @@ let parse_args arglist = let init_toplevel arglist = init_gc (); Sys.catch_break false; (* Ctrl-C is fatal during the initialisation *) + let init_feeder = Feedback.add_feeder coqtop_init_feed in Lib.init(); begin try @@ -663,7 +674,8 @@ let init_toplevel arglist = Feedback.msg_notice (with_option raw_print Prettyp.print_full_pure_context () ++ fnl ()); Profile.print_profile (); exit 0 - end + end; + Feedback.del_feeder init_feeder let start () = let () = init_toplevel (List.tl (Array.to_list Sys.argv)) in diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index 5d17054fc..4fc4540c1 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -143,8 +143,8 @@ let pr_new_syntax_in_context loc chan_beautify ocom = | None -> mt() in let after = comment (CLexer.extract_comments (snd loc)) in if !beautify_file then - (Pp.pp_with !Pp_control.std_ft (hov 0 (before ++ com ++ after)); - Format.pp_print_flush !Pp_control.std_ft ()) + (Pp.pp_with !Topfmt.std_ft (hov 0 (before ++ com ++ after)); + Format.pp_print_flush !Topfmt.std_ft ()) else Feedback.msg_info (hov 4 (str"New Syntax:" ++ fnl() ++ (hov 0 com))); States.unfreeze fs; @@ -179,9 +179,10 @@ let pp_cmd_header loc com = (* This is a special case where we assume we are in console batch mode and take control of the console. *) +(* FIXME *) let print_cmd_header loc com = - Pp.pp_with ~pp_tag:Ppstyle.to_format !Pp_control.std_ft (pp_cmd_header loc com); - Format.pp_print_flush !Pp_control.std_ft () + Pp.pp_with ~pp_tag:Ppstyle.to_format !Topfmt.std_ft (pp_cmd_header loc com); + Format.pp_print_flush !Topfmt.std_ft () let rec interp_vernac po chan_beautify checknav (loc,com) = let interp = function diff --git a/vernac/explainErr.ml b/vernac/explainErr.ml index 5b91af03c..f1e0c48f0 100644 --- a/vernac/explainErr.ml +++ b/vernac/explainErr.ml @@ -45,15 +45,9 @@ let _ = CErrors.register_handler explain_exn_default (** Pre-explain a vernac interpretation error *) -let wrap_vernac_error with_header (exn, info) strm = - if with_header then - let header = Pp.tag Ppstyle.error_tag (str "Error:") in - let e = EvaluatedError (hov 0 (header ++ spc () ++ strm), None) in - (e, info) - else - (EvaluatedError (strm, None), info) +let wrap_vernac_error (exn, info) strm = (EvaluatedError (strm, None), info) -let process_vernac_interp_error with_header exn = match fst exn with +let process_vernac_interp_error exn = match fst exn with | Univ.UniverseInconsistency i -> let msg = if !Constrextern.print_universes then @@ -61,40 +55,40 @@ let process_vernac_interp_error with_header exn = match fst exn with Univ.explain_universe_inconsistency Universes.pr_with_global_universes i else mt() in - wrap_vernac_error with_header exn (str "Universe inconsistency" ++ msg ++ str ".") + wrap_vernac_error exn (str "Universe inconsistency" ++ msg ++ str ".") | TypeError(ctx,te) -> - wrap_vernac_error with_header exn (Himsg.explain_type_error ctx Evd.empty te) + wrap_vernac_error exn (Himsg.explain_type_error ctx Evd.empty te) | PretypeError(ctx,sigma,te) -> - wrap_vernac_error with_header exn (Himsg.explain_pretype_error ctx sigma te) + wrap_vernac_error exn (Himsg.explain_pretype_error ctx sigma te) | Typeclasses_errors.TypeClassError(env, te) -> - wrap_vernac_error with_header exn (Himsg.explain_typeclass_error env te) + wrap_vernac_error exn (Himsg.explain_typeclass_error env te) | InductiveError e -> - wrap_vernac_error with_header exn (Himsg.explain_inductive_error e) + wrap_vernac_error exn (Himsg.explain_inductive_error e) | Modops.ModuleTypingError e -> - wrap_vernac_error with_header exn (Himsg.explain_module_error e) + wrap_vernac_error exn (Himsg.explain_module_error e) | Modintern.ModuleInternalizationError e -> - wrap_vernac_error with_header exn (Himsg.explain_module_internalization_error e) + wrap_vernac_error exn (Himsg.explain_module_internalization_error e) | RecursionSchemeError e -> - wrap_vernac_error with_header exn (Himsg.explain_recursion_scheme_error e) + wrap_vernac_error exn (Himsg.explain_recursion_scheme_error e) | Cases.PatternMatchingError (env,sigma,e) -> - wrap_vernac_error with_header exn (Himsg.explain_pattern_matching_error env sigma e) + wrap_vernac_error exn (Himsg.explain_pattern_matching_error env sigma e) | Tacred.ReductionTacticError e -> - wrap_vernac_error with_header exn (Himsg.explain_reduction_tactic_error e) + wrap_vernac_error exn (Himsg.explain_reduction_tactic_error e) | Logic.RefinerError e -> - wrap_vernac_error with_header exn (Himsg.explain_refiner_error e) + wrap_vernac_error exn (Himsg.explain_refiner_error e) | Nametab.GlobalizationError q -> - wrap_vernac_error with_header exn + wrap_vernac_error exn (str "The reference" ++ spc () ++ Libnames.pr_qualid q ++ spc () ++ str "was not found" ++ spc () ++ str "in the current" ++ spc () ++ str "environment.") | Refiner.FailError (i,s) -> let s = Lazy.force s in - wrap_vernac_error with_header exn + wrap_vernac_error exn (str "Tactic failure" ++ (if Pp.ismt s then s else str ": " ++ s) ++ if Int.equal i 0 then str "." else str " (level " ++ int i ++ str").") | AlreadyDeclared msg -> - wrap_vernac_error with_header exn (msg ++ str ".") + wrap_vernac_error exn (msg ++ str ".") | _ -> exn @@ -108,9 +102,9 @@ let additional_error_info = ref [] let register_additional_error_info f = additional_error_info := f :: !additional_error_info -let process_vernac_interp_error ?(allow_uncaught=true) ?(with_header=true) (exc, info) = +let process_vernac_interp_error ?(allow_uncaught=true) (exc, info) = let exc = strip_wrapping_exceptions exc in - let e = process_vernac_interp_error with_header (exc, info) in + let e = process_vernac_interp_error (exc, info) in let () = if not allow_uncaught && not (CErrors.handled (fst e)) then let (e, info) = e in diff --git a/vernac/explainErr.mli b/vernac/explainErr.mli index a67c887af..370ad7e3b 100644 --- a/vernac/explainErr.mli +++ b/vernac/explainErr.mli @@ -11,7 +11,7 @@ exception EvaluatedError of Pp.std_ppcmds * exn option (** Pre-explain a vernac interpretation error *) -val process_vernac_interp_error : ?allow_uncaught:bool -> ?with_header:bool -> Util.iexn -> Util.iexn +val process_vernac_interp_error : ?allow_uncaught:bool -> Util.iexn -> Util.iexn (** General explain function. Should not be used directly now, see instead function [Errors.print] and variants *) diff --git a/vernac/topfmt.ml b/vernac/topfmt.ml new file mode 100644 index 000000000..85981c386 --- /dev/null +++ b/vernac/topfmt.ml @@ -0,0 +1,245 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Feedback +open Pp + +(** Pp control also belongs here as the terminal is private to the toplevel *) + +type pp_global_params = { + margin : int; + max_indent : int; + max_depth : int; + ellipsis : string } + +(* Default parameters of pretty-printing *) + +let dflt_gp = { + margin = 78; + max_indent = 50; + max_depth = 50; + ellipsis = "..." } + +(* A deeper pretty-printer to print proof scripts *) + +let deep_gp = { + margin = 78; + max_indent = 50; + max_depth = 10000; + ellipsis = "..." } + +(* set_gp : Format.formatter -> pp_global_params -> unit + * set the parameters of a formatter *) + +let set_gp ft gp = + Format.pp_set_margin ft gp.margin ; + Format.pp_set_max_indent ft gp.max_indent ; + Format.pp_set_max_boxes ft gp.max_depth ; + Format.pp_set_ellipsis_text ft gp.ellipsis + +let set_dflt_gp ft = set_gp ft dflt_gp + +let get_gp ft = + { margin = Format.pp_get_margin ft (); + max_indent = Format.pp_get_max_indent ft (); + max_depth = Format.pp_get_max_boxes ft (); + ellipsis = Format.pp_get_ellipsis_text ft () } + +(* with_fp : 'a pp_formatter_params -> Format.formatter + * returns of formatter for given formatter functions *) + +let with_fp chan out_function flush_function = + let ft = Format.make_formatter out_function flush_function in + Format.pp_set_formatter_out_channel ft chan; + ft + +(* Output on a channel ch *) + +let with_output_to ch = + let ft = with_fp ch (output_substring ch) (fun () -> flush ch) in + set_gp ft deep_gp; + ft + +let std_ft = ref Format.std_formatter +let _ = set_dflt_gp !std_ft + +let err_ft = ref Format.err_formatter +let _ = set_gp !err_ft deep_gp + +let deep_ft = ref (with_output_to stdout) +let _ = set_gp !deep_ft deep_gp + +(* For parametrization through vernacular *) +let default = Format.pp_get_max_boxes !std_ft () +let default_margin = Format.pp_get_margin !std_ft () + +let get_depth_boxes () = Some (Format.pp_get_max_boxes !std_ft ()) +let set_depth_boxes v = + Format.pp_set_max_boxes !std_ft (match v with None -> default | Some v -> v) + +let get_margin () = Some (Format.pp_get_margin !std_ft ()) +let set_margin v = + let v = match v with None -> default_margin | Some v -> v in + Format.pp_set_margin Format.str_formatter v; + Format.pp_set_margin !std_ft v; + Format.pp_set_margin !deep_ft v; + (* Heuristic, based on usage: the column on the right of max_indent + column is 20% of width, capped to 30 characters *) + let m = max (64 * v / 100) (v-30) in + Format.pp_set_max_indent Format.str_formatter m; + Format.pp_set_max_indent !std_ft m; + Format.pp_set_max_indent !deep_ft m + +(** Console display of feedback *) + +type logger = ?loc:Loc.t -> level -> std_ppcmds -> unit + +let msgnl_with ?pp_tag fmt strm = + pp_with ?pp_tag fmt (strm ++ fnl ()); + Format.pp_print_flush fmt () + +(* XXX: This is really painful! *) +module Emacs = struct + + (* Special chars for emacs, to detect warnings inside goal output *) + let emacs_quote_start = String.make 1 (Char.chr 254) + let emacs_quote_end = String.make 1 (Char.chr 255) + + let emacs_quote_err g = + hov 0 (str emacs_quote_start ++ g ++ str emacs_quote_end) + + let emacs_quote_info_start = "<infomsg>" + let emacs_quote_info_end = "</infomsg>" + + let emacs_quote_info g = + hov 0 (str emacs_quote_info_start++ brk(0,0) ++ g ++ brk(0,0) ++ str emacs_quote_info_end) + +end + +open Emacs + +let dbg_str = tag Ppstyle.debug_tag (str "Debug:") ++ spc () +let info_str = mt () +let warn_str = tag Ppstyle.warning_tag (str "Warning:") ++ spc () +let err_str = tag Ppstyle.error_tag (str "Error:") ++ spc () + +let make_body quoter info ?loc s = + let loc = Option.cata Pp.pr_loc (Pp.mt ()) loc in + quoter (hov 0 (loc ++ info ++ s)) + +(* Generic logger *) +let gen_logger ?pp_tag dbg err ?loc level msg = match level with + | Debug -> msgnl_with ?pp_tag !std_ft (make_body dbg dbg_str ?loc msg) + | Info -> msgnl_with ?pp_tag !std_ft (make_body dbg info_str ?loc msg) + (* XXX: What to do with loc here? *) + | Notice -> msgnl_with ?pp_tag !std_ft msg + | Warning -> Flags.if_warn (fun () -> + msgnl_with ?pp_tag !err_ft (make_body err warn_str ?loc msg)) () + | Error -> msgnl_with ?pp_tag !err_ft (make_body err err_str ?loc msg) + +(** Standard loggers *) + +(* We provide a generic clear_log_backend callback for backends + wanting to do clenaup after the print. +*) +let std_logger_tag = ref None +let std_logger_cleanup = ref (fun () -> ()) + +let std_logger ?loc level msg = + gen_logger (fun x -> x) (fun x -> x) ?pp_tag:!std_logger_tag ?loc level msg; + !std_logger_cleanup () + +(** Color logging. Moved from pp_style, it may need some more refactoring *) + +(** Not thread-safe. We should put a lock somewhere if we print from + different threads. Do we? *) +let make_style_stack () = + (** Default tag is to reset everything *) + let empty = Terminal.make () in + let default_tag = Terminal.({ + fg_color = Some `DEFAULT; + bg_color = Some `DEFAULT; + bold = Some false; + italic = Some false; + underline = Some false; + negative = Some false; + }) + in + let style_stack = ref [] in + let peek () = match !style_stack with + | [] -> default_tag (** Anomalous case, but for robustness *) + | st :: _ -> st + in + let push tag = + let style = match Ppstyle.get_style_format tag with + | None -> empty + | Some st -> st + in + (** Use the merging of the latest tag and the one being currently pushed. + This may be useful if for instance the latest tag changes the background and + the current one the foreground, so that the two effects are additioned. *) + let style = Terminal.merge (peek ()) style in + style_stack := style :: !style_stack; + Terminal.eval style + in + let pop _ = match !style_stack with + | [] -> (** Something went wrong, we fallback *) + Terminal.eval default_tag + | _ :: rem -> style_stack := rem; + Terminal.eval (peek ()) + in + let clear () = style_stack := [] in + push, pop, clear + +let init_color_output () = + let push_tag, pop_tag, clear_tag = make_style_stack () in + std_logger_cleanup := clear_tag; + std_logger_tag := Some Ppstyle.to_format; + let tag_handler = { + Format.mark_open_tag = push_tag; + Format.mark_close_tag = pop_tag; + Format.print_open_tag = ignore; + Format.print_close_tag = ignore; + } in + Format.pp_set_mark_tags !std_ft true; + Format.pp_set_mark_tags !err_ft true; + Format.pp_set_formatter_tag_functions !std_ft tag_handler; + Format.pp_set_formatter_tag_functions !err_ft tag_handler + +(* Rules for emacs: + - Debug/info: emacs_quote_info + - Warning/Error: emacs_quote_err + - Notice: unquoted + *) +let emacs_logger = gen_logger emacs_quote_info emacs_quote_err + +(* Output to file, used only in extraction so a candidate for removal *) +let ft_logger old_logger ft ?loc level mesg = + let id x = x in + match level with + | Debug -> msgnl_with ft (make_body id dbg_str mesg) + | Info -> msgnl_with ft (make_body id info_str mesg) + | Notice -> msgnl_with ft mesg + | Warning -> old_logger ?loc level mesg + | Error -> old_logger ?loc level mesg + +let with_output_to_file fname func input = + (* XXX FIXME: redirect std_ft *) + (* let old_logger = !logger in *) + let channel = open_out (String.concat "." [fname; "out"]) in + (* logger := ft_logger old_logger (Format.formatter_of_out_channel channel); *) + try + let output = func input in + (* logger := old_logger; *) + close_out channel; + output + with reraise -> + let reraise = Backtrace.add_backtrace reraise in + (* logger := old_logger; *) + close_out channel; + Exninfo.iraise reraise diff --git a/lib/pp_control.mli b/vernac/topfmt.mli index d26f89eb3..38a400cfd 100644 --- a/lib/pp_control.mli +++ b/vernac/topfmt.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(** Parameters of pretty-printing. *) +(** Console printing options *) type pp_global_params = { margin : int; @@ -20,13 +20,12 @@ val set_gp : Format.formatter -> pp_global_params -> unit val set_dflt_gp : Format.formatter -> unit val get_gp : Format.formatter -> pp_global_params - (** {6 Output functions of pretty-printing. } *) val with_output_to : out_channel -> Format.formatter -val std_ft : Format.formatter ref -val err_ft : Format.formatter ref +val std_ft : Format.formatter ref +val err_ft : Format.formatter ref val deep_ft : Format.formatter ref (** {6 For parametrization through vernacular. } *) @@ -36,3 +35,15 @@ val get_depth_boxes : unit -> int option val set_margin : int option -> unit val get_margin : unit -> int option + +(** Console display of feedback *) +val std_logger : ?loc:Loc.t -> Feedback.level -> Pp.std_ppcmds -> unit + +val emacs_logger : ?loc:Loc.t -> Feedback.level -> Pp.std_ppcmds -> unit + +val init_color_output : unit -> unit + +(** [with_output_to_file file f x] executes [f x] with logging + redirected to a file [file] *) +val with_output_to_file : string -> ('a -> 'b) -> 'a -> 'b + diff --git a/vernac/vernac.mllib b/vernac/vernac.mllib index 94ef54f70..283c095eb 100644 --- a/vernac/vernac.mllib +++ b/vernac/vernac.mllib @@ -14,4 +14,5 @@ Record Assumptions Vernacinterp Mltop +Topfmt Vernacentries diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 3afe04b37..09c43f93e 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1448,8 +1448,8 @@ let _ = optdepr = false; optname = "the printing depth"; optkey = ["Printing";"Depth"]; - optread = Pp_control.get_depth_boxes; - optwrite = Pp_control.set_depth_boxes } + optread = Topfmt.get_depth_boxes; + optwrite = Topfmt.set_depth_boxes } let _ = declare_int_option @@ -1457,8 +1457,8 @@ let _ = optdepr = false; optname = "the printing width"; optkey = ["Printing";"Width"]; - optread = Pp_control.get_margin; - optwrite = Pp_control.set_margin } + optread = Topfmt.get_margin; + optwrite = Topfmt.set_margin } let _ = declare_bool_option @@ -2193,7 +2193,7 @@ let with_fail b f = | e -> let e = CErrors.push e in raise (HasFailed (CErrors.iprint - (ExplainErr.process_vernac_interp_error ~allow_uncaught:false ~with_header:false e)))) + (ExplainErr.process_vernac_interp_error ~allow_uncaught:false e)))) () with e when CErrors.noncritical e -> let (e, _) = CErrors.push e in @@ -2226,7 +2226,7 @@ let interp ?(verbosely=true) ?proof (loc,c) = current_timeout := Some n; aux ?locality ?polymorphism isprogcmd v | VernacRedirect (s, (_,v)) -> - Feedback.with_output_to_file s (aux false) v + Topfmt.with_output_to_file s (aux false) v | VernacTime (_,v) -> System.with_time !Flags.time (aux ?locality ?polymorphism isprogcmd) v; |