diff options
-rw-r--r-- | ide/richpp.ml | 29 | ||||
-rw-r--r-- | ide/richpp.mli | 4 | ||||
-rw-r--r-- | ide/xmlprotocol.ml | 4 | ||||
-rw-r--r-- | lib/pp.ml | 14 | ||||
-rw-r--r-- | lib/pp.mli | 10 | ||||
-rw-r--r-- | lib/ppstyle.ml | 13 | ||||
-rw-r--r-- | lib/ppstyle.mli | 11 | ||||
-rw-r--r-- | parsing/cLexer.ml4 | 2 | ||||
-rw-r--r-- | tools/fake_ide.ml | 2 | ||||
-rw-r--r-- | toplevel/coqloop.ml | 2 | ||||
-rw-r--r-- | toplevel/coqtop.ml | 9 | ||||
-rw-r--r-- | toplevel/vernac.ml | 2 | ||||
-rw-r--r-- | vernac/topfmt.ml | 22 |
13 files changed, 37 insertions, 87 deletions
diff --git a/ide/richpp.ml b/ide/richpp.ml index 515090f71..ecf1f4021 100644 --- a/ide/richpp.ml +++ b/ide/richpp.ml @@ -24,10 +24,6 @@ type 'a context = { (** Pending opened nodes *) mutable offset : int; (** Quantity of characters printed so far *) - mutable annotations : 'a option Int.Map.t; - (** Map associating annotations to indexes *) - mutable index : int; - (** Current index of annotations *) } (** We use Format to introduce tags inside the pretty-printed document. @@ -38,23 +34,13 @@ type 'a context = { marking functions. As those functions are called when actually writing to the device, the resulting tree is correct. *) -let rich_pp width annotate ppcmds = +let rich_pp width ppcmds = let context = { stack = Leaf; offset = 0; - annotations = Int.Map.empty; - index = (-1); } in - let pp_tag obj = - let index = context.index + 1 in - let () = context.index <- index in - let obj = annotate obj in - let () = context.annotations <- Int.Map.add index obj context.annotations in - string_of_int index - in - let pp_buffer = Buffer.create 180 in let push_pcdata () = @@ -81,12 +67,8 @@ let rich_pp width annotate ppcmds = | Leaf -> assert false | Node (node, child, pos, ctx) -> let () = assert (String.equal tag node) in - let annotation = - try Int.Map.find (int_of_string node) context.annotations - with _ -> None - in let annotation = { - annotation = annotation; + annotation = Some tag; startpos = pos; endpos = context.offset; } in @@ -123,7 +105,7 @@ let rich_pp width annotate ppcmds = (** The whole output must be a valid document. To that end, we nest the document inside <pp> tags. *) pp_open_tag ft "pp"; - Pp.(pp_with ~pp_tag ft ppcmds); + Pp.(pp_with ft ppcmds); pp_close_tag ft (); (** Get the resulting XML tree. *) @@ -173,14 +155,13 @@ let xml_of_rich_pp tag_of_annotation attributes_of_annotation xml = type richpp = xml let richpp_of_pp width pp = - let annotate t = Some (Ppstyle.repr t) in let rec drop = function | PCData s -> [PCData s] | Element (_, annotation, cs) -> let cs = List.concat (List.map drop cs) in match annotation.annotation with | None -> cs - | Some s -> [Element (String.concat "." s, [], cs)] + | Some s -> [Element (s, [], cs)] in - let xml = rich_pp width annotate pp in + let xml = rich_pp width pp in Element ("_", [], drop xml) diff --git a/ide/richpp.mli b/ide/richpp.mli index 0ceeeefc2..0fe4315b7 100644 --- a/ide/richpp.mli +++ b/ide/richpp.mli @@ -24,9 +24,7 @@ type 'annotation located = { that represents (located) annotations of this string. The [get_annotations] function is used to convert tags into the desired annotation. [width] sets the printing witdh of the formatter. *) -val rich_pp : int -> - (Pp.pp_tag -> 'annotation option) -> Pp.std_ppcmds -> - 'annotation located Xml_datatype.gxml +val rich_pp : int -> Pp.std_ppcmds -> Pp.pp_tag located Xml_datatype.gxml (** [annotations_positions ssdoc] returns a list associating each annotations with its position in the string from which [ssdoc] is diff --git a/ide/xmlprotocol.ml b/ide/xmlprotocol.ml index 6ed62082d..1d50aed03 100644 --- a/ide/xmlprotocol.ml +++ b/ide/xmlprotocol.ml @@ -112,7 +112,7 @@ let rec of_pp (pp : Pp.std_ppcmds) = let open Pp in match pp with | 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_tag (t,s) -> constructor "ppdoc" "tag" [of_pair 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" [] @@ -126,7 +126,7 @@ let rec to_pp xpp = let open Pp in | "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 + | "tag" -> let (tg,s) = to_pair 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) @@ -17,7 +17,7 @@ \end{description} *) -type pp_tag = string list +type pp_tag = string type block_type = | Pp_hbox of int @@ -161,10 +161,8 @@ let rec pr_com ft s = Some s2 -> Format.pp_force_newline ft (); pr_com ft s2 | None -> () -type tag_handler = pp_tag -> Format.tag - (* pretty printing functions *) -let pp_with ?pp_tag ft = +let pp_with ft = let cpp_open_box = function | Pp_hbox n -> Format.pp_open_hbox ft () | Pp_vbox n -> Format.pp_open_vbox ft n @@ -182,9 +180,9 @@ let pp_with ?pp_tag 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 - | Ppcmd_tag(tag, s) -> Option.iter (fun f -> pp_open_tag ft (f tag)) pp_tag; + | Ppcmd_tag(tag, s) -> pp_open_tag ft tag; pp_cmd s; - Option.iter (fun _ -> pp_close_tag ft () ) pp_tag + pp_close_tag ft () in try pp_cmd with reraise -> @@ -197,8 +195,8 @@ let pp_with ?pp_tag ft = them to different windows. *) (** Output to a string formatter *) -let string_of_ppcmds ?pp_tag c = - Format.fprintf Format.str_formatter "@[%a@]" (pp_with ?pp_tag) c; +let string_of_ppcmds c = + Format.fprintf Format.str_formatter "@[%a@]" pp_with c; Format.flush_str_formatter () (* Copy paste from Util *) diff --git a/lib/pp.mli b/lib/pp.mli index 12747d3a1..ff4206534 100644 --- a/lib/pp.mli +++ b/lib/pp.mli @@ -33,7 +33,7 @@ (************************************************************************) (* XXX: Improve and add attributes *) -type pp_tag = string list +type pp_tag = string type block_type = | Pp_hbox of int @@ -165,9 +165,7 @@ val pr_loc : Loc.t -> std_ppcmds (** {6 Main renderers, to formatter and to string } *) -(** FIXME: These ignore the logging settings and call [Format] directly *) -type tag_handler = pp_tag -> Format.tag - (** [msg_with fmt pp] Print [pp] to [fmt] and don't flush [fmt] *) -val pp_with : ?pp_tag:tag_handler -> Format.formatter -> std_ppcmds -> unit -val string_of_ppcmds : ?pp_tag:tag_handler -> std_ppcmds -> string +val pp_with : Format.formatter -> std_ppcmds -> unit + +val string_of_ppcmds : std_ppcmds -> string diff --git a/lib/ppstyle.ml b/lib/ppstyle.ml index 298e3be6b..6969c3d5c 100644 --- a/lib/ppstyle.ml +++ b/lib/ppstyle.ml @@ -19,27 +19,20 @@ let make ?style tag = let name = to_format tag in let () = assert (not (String.Map.mem name !tags)) in let () = tags := String.Map.add name style !tags in - tag - -let repr t = t + name let get_style tag = - try String.Map.find (to_format tag) !tags - with Not_found -> assert false - -let get_style_format tag = try String.Map.find tag !tags with Not_found -> assert false let set_style tag st = - try tags := String.Map.update (to_format tag) st !tags + try tags := String.Map.update tag st !tags with Not_found -> assert false let clear_styles () = tags := String.Map.map (fun _ -> None) !tags -let dump () = - List.map (fun (s,b) -> (String.split '.' s, b)) (String.Map.bindings !tags) +let dump () = String.Map.bindings !tags let parse_config s = let styles = Terminal.parse s in diff --git a/lib/ppstyle.mli b/lib/ppstyle.mli index b9422f7cf..2690d3910 100644 --- a/lib/ppstyle.mli +++ b/lib/ppstyle.mli @@ -14,28 +14,17 @@ (** This API is provisional and will likely be refined. *) type t = Pp.pp_tag -val to_format : t -> Format.tag -val of_format : Format.tag -> t - (** Style tags *) val make : ?style:Terminal.style -> string list -> t (** Create a new tag with the given name. Each name must be unique. The optional style is taken as the default one. *) -val repr : t -> string list -(** Gives back the original name of the style tag where each string has been - concatenated and separated with a dot. *) - (** {5 Manipulating global styles} *) val get_style : t -> Terminal.style option -(** Get the style associated to a tag. *) - -val get_style_format : Format.tag -> Terminal.style option (** Get the style associated to a tag from a format tag. *) - val set_style : t -> Terminal.style option -> unit (** Set a style associated to a tag. *) diff --git a/parsing/cLexer.ml4 b/parsing/cLexer.ml4 index a637d2e43..3b84eaa81 100644 --- a/parsing/cLexer.ml4 +++ b/parsing/cLexer.ml4 @@ -105,7 +105,7 @@ module Error = struct Printf.sprintf "Unsupported Unicode character (0x%x)" x) (* Require to fix the Camlp4 signature *) - let print ppf x = Pp.pp_with ~pp_tag:Ppstyle.to_format ppf (Pp.str (to_string x)) + let print ppf x = Pp.pp_with ppf (Pp.str (to_string x)) end open Error diff --git a/tools/fake_ide.ml b/tools/fake_ide.ml index b538ba1d0..5dd2a9220 100644 --- a/tools/fake_ide.ml +++ b/tools/fake_ide.ml @@ -18,7 +18,7 @@ type coqtop = { } let print_error msg = - Format.eprintf "fake_id: error: @[%a@]\n%!" (Pp.pp_with ?pp_tag:None) msg + Format.eprintf "fake_id: error: @[%a@]\n%!" Pp.pp_with msg let base_eval_call ?(print=true) ?(fail=true) call coqtop = if print then prerr_endline (Xmlprotocol.pr_call call); diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml index e9506803d..43807c1ca 100644 --- a/toplevel/coqloop.ml +++ b/toplevel/coqloop.ml @@ -14,7 +14,7 @@ open Vernac open Pcoq let top_stderr x = - Format.fprintf !Topfmt.err_ft "@[%a@]%!" (pp_with ~pp_tag:Ppstyle.to_format) x + Format.fprintf !Topfmt.err_ft "@[%a@]%!" pp_with x (* A buffer for the character read from a channel. We store the command * entered to be able to report errors without pretty-printing. *) diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 823d05580..268d40c91 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -311,18 +311,13 @@ let print_style_tags () = let tags = Ppstyle.dump () in let iter (t, st) = let st = match st with Some st -> st | None -> Terminal.make () in - let opt = - Terminal.eval st ^ - String.concat "." (Ppstyle.repr t) ^ - Terminal.reset ^ "\n" - in + let opt = Terminal.eval st ^ t ^ Terminal.reset ^ "\n" in print_string opt in let make (t, st) = match st with | None -> None | Some st -> let tags = List.map string_of_int (Terminal.repr st) in - let t = String.concat "." (Ppstyle.repr t) in Some (t ^ "=" ^ String.concat ";" tags) in let repr = List.map_filter make tags in @@ -445,7 +440,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 ?pp_tag:None) msg; + Format.fprintf !Topfmt.err_ft "@[%a@]%!" pp_with msg; exit (if anomaly then 129 else 1) let parse_args arglist = diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index 4fc4540c1..06908abb6 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -181,7 +181,7 @@ let pp_cmd_header loc com = *) (* FIXME *) let print_cmd_header loc com = - Pp.pp_with ~pp_tag:Ppstyle.to_format !Topfmt.std_ft (pp_cmd_header loc com); + Pp.pp_with !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) = diff --git a/vernac/topfmt.ml b/vernac/topfmt.ml index 85981c386..e5063e27b 100644 --- a/vernac/topfmt.ml +++ b/vernac/topfmt.ml @@ -99,8 +99,8 @@ let set_margin v = type logger = ?loc:Loc.t -> level -> std_ppcmds -> unit -let msgnl_with ?pp_tag fmt strm = - pp_with ?pp_tag fmt (strm ++ fnl ()); +let msgnl_with fmt strm = + pp_with fmt (strm ++ fnl ()); Format.pp_print_flush fmt () (* XXX: This is really painful! *) @@ -133,25 +133,24 @@ let make_body quoter info ?loc s = 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) +let gen_logger dbg err ?loc level msg = match level with + | Debug -> msgnl_with !std_ft (make_body dbg dbg_str ?loc msg) + | Info -> msgnl_with !std_ft (make_body dbg info_str ?loc msg) (* XXX: What to do with loc here? *) - | Notice -> msgnl_with ?pp_tag !std_ft msg + | Notice -> msgnl_with !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) + msgnl_with !err_ft (make_body err warn_str ?loc msg)) () + | Error -> msgnl_with !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; + gen_logger (fun x -> x) (fun x -> x) ?loc level msg; !std_logger_cleanup () (** Color logging. Moved from pp_style, it may need some more refactoring *) @@ -176,7 +175,7 @@ let make_style_stack () = | st :: _ -> st in let push tag = - let style = match Ppstyle.get_style_format tag with + let style = match Ppstyle.get_style tag with | None -> empty | Some st -> st in @@ -199,7 +198,6 @@ let make_style_stack () = 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; |