From 2280477a96e19ba5060de2d48dcc8fd7c8079d22 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 13 Nov 2015 11:31:34 +0100 Subject: Imported Upstream version 8.5~beta3+dfsg --- lib/aux_file.ml | 2 + lib/aux_file.mli | 4 ++ lib/cThread.ml | 14 +---- lib/clib.mllib | 1 + lib/dyn.ml | 9 ++-- lib/errors.ml | 27 ++++++++-- lib/errors.mli | 10 ++++ lib/flags.ml | 12 +++-- lib/flags.mli | 13 +++-- lib/future.ml | 20 ++++--- lib/future.mli | 7 ++- lib/pp.ml | 77 +++++++++++++++------------ lib/pp.mli | 5 +- lib/pp_control.ml | 11 ++-- lib/ppstyle.ml | 149 +++++++++++++++++++++++++++++++++++++++++++++++++++++ lib/ppstyle.mli | 70 +++++++++++++++++++++++++ lib/richpp.mli | 2 +- lib/spawn.ml | 44 ++++++++++------ lib/system.ml | 79 ++++++++++++++-------------- lib/system.mli | 10 ++-- lib/terminal.ml | 7 ++- lib/terminal.mli | 3 ++ lib/util.ml | 11 ++++ lib/util.mli | 3 ++ lib/xml_lexer.mll | 17 ++++-- lib/xml_parser.mli | 16 +++--- lib/xml_printer.ml | 2 + 27 files changed, 476 insertions(+), 149 deletions(-) create mode 100644 lib/ppstyle.ml create mode 100644 lib/ppstyle.mli (limited to 'lib') diff --git a/lib/aux_file.ml b/lib/aux_file.ml index c9018c9e..5dedb0d0 100644 --- a/lib/aux_file.ml +++ b/lib/aux_file.ml @@ -42,6 +42,8 @@ module M = Map.Make(String) type data = string M.t type aux_file = data H.t +let contents x = x + let empty_aux_file = H.empty let get aux loc key = M.find key (H.find (Loc.unloc loc) aux) diff --git a/lib/aux_file.mli b/lib/aux_file.mli index e340fc65..b672d3db 100644 --- a/lib/aux_file.mli +++ b/lib/aux_file.mli @@ -13,6 +13,10 @@ val get : aux_file -> Loc.t -> string -> string val empty_aux_file : aux_file val set : aux_file -> Loc.t -> string -> string -> aux_file +module H : Map.S with type key = int * int +module M : Map.S with type key = string +val contents : aux_file -> string M.t H.t + val start_aux_file_for : string -> unit val stop_aux_file : unit -> unit val recording : unit -> bool diff --git a/lib/cThread.ml b/lib/cThread.ml index 2d1f10bf..9cbdf5a9 100644 --- a/lib/cThread.ml +++ b/lib/cThread.ml @@ -8,22 +8,12 @@ type thread_ic = in_channel -let prepare_in_channel_for_thread_friendly_io ic = - Unix.set_nonblock (Unix.descr_of_in_channel ic); ic - -let safe_wait_timed_read fd time = - try Thread.wait_timed_read fd time - with Unix.Unix_error (Unix.EINTR, _, _) -> - (** On Unix, the above function may raise this exception when it is - interrupted by a signal. (It uses Unix.select internally.) *) - false +let prepare_in_channel_for_thread_friendly_io ic = ic let thread_friendly_read_fd fd s ~off ~len = let rec loop () = try Unix.read fd s off len - with Unix.Unix_error((Unix.EWOULDBLOCK|Unix.EAGAIN|Unix.EINTR),_,_) -> - while not (safe_wait_timed_read fd 0.05) do Thread.yield () done; - loop () + with Unix.Unix_error(Unix.EINTR,_,_) -> loop () in loop () diff --git a/lib/clib.mllib b/lib/clib.mllib index 2da81c95..7ff1d293 100644 --- a/lib/clib.mllib +++ b/lib/clib.mllib @@ -29,6 +29,7 @@ Util Stateid Feedback Pp +Ppstyle Xml_lexer Xml_parser Xml_printer diff --git a/lib/dyn.ml b/lib/dyn.ml index a5e8fb9c..056b6873 100644 --- a/lib/dyn.ml +++ b/lib/dyn.ml @@ -7,6 +7,7 @@ (************************************************************************) open Errors +open Pp (* Dynamics, programmed with DANGER !!! *) @@ -23,7 +24,7 @@ let create (s : string) = let () = if Int.Map.mem hash !dyntab then let old = Int.Map.find hash !dyntab in - let msg = Pp.str ("Dynamic tag collision: " ^ s ^ " vs. " ^ old) in + let msg = str "Dynamic tag collision: " ++ str s ++ str " vs. " ++ str old in anomaly ~label:"Dyn.create" msg in let () = dyntab := Int.Map.add hash s !dyntab in @@ -31,8 +32,7 @@ let create (s : string) = let outfun (nh, rv) = if Int.equal hash nh then Obj.magic rv else - let msg = (Pp.str ("dyn_out: expected " ^ s)) in - anomaly msg + anomaly (str "dyn_out: expected " ++ str s) in (infun, outfun) @@ -43,8 +43,7 @@ let has_tag (s, _) tag = let tag (s,_) = try Int.Map.find s !dyntab with Not_found -> - let msg = Pp.str ("Unknown dynamic tag " ^ (string_of_int s)) in - anomaly msg + anomaly (str "Unknown dynamic tag " ++ int s) let pointer_equal (t1,o1) (t2,o2) = t1 = t2 && o1 == o2 diff --git a/lib/errors.ml b/lib/errors.ml index a4ec357e..c1d224df 100644 --- a/lib/errors.ml +++ b/lib/errors.ml @@ -69,12 +69,12 @@ let rec print_gen bottom stk e = let where = function | None -> mt () | Some s -> - if !Flags.debug then str ("in "^s^":") ++ spc () else mt () + if !Flags.debug then str "in " ++ str s ++ str ":" ++ spc () else mt () let raw_anomaly e = match e with | Anomaly (s, pps) -> where s ++ pps ++ str "." - | Assert_failure _ | Match_failure _ -> str (Printexc.to_string e ^ ".") - | _ -> str ("Uncaught exception " ^ Printexc.to_string e ^ ".") + | Assert_failure _ | Match_failure _ -> str (Printexc.to_string e) ++ str "." + | _ -> str "Uncaught exception " ++ str (Printexc.to_string e) ++ str "." let print_backtrace e = match Backtrace.get_backtrace e with | None -> mt () @@ -99,6 +99,8 @@ let iprint (e, info) = print ~info e (** Same as [print], except that the "Please report" part of an anomaly isn't printed (used in Ltac debugging). *) let print_no_report e = print_gen (print_anomaly false) !handle_stack e +let iprint_no_report (e, info) = + print_gen (print_anomaly false) !handle_stack e ++ print_backtrace info (** Predefined handlers **) @@ -118,3 +120,22 @@ let noncritical = function | Timeout | Drop | Quit -> false | Invalid_argument "equal: functional value" -> false | _ -> true + +(** Check whether an exception is handled *) + +exception Bottom + +let handled e = + let bottom _ = raise Bottom in + try let _ = print_gen bottom !handle_stack e in true + with Bottom -> false + +(** Prints info which is either an error or + an anomaly and then exits with the appropriate + error code *) + +let fatal_error info anomaly = + let msg = info ++ fnl () in + pp_with ~pp_tag:Ppstyle.pp_tag !Pp_control.err_ft msg; + flush_all (); + exit (if anomaly then 129 else 1) diff --git a/lib/errors.mli b/lib/errors.mli index 03caa6a9..e5dad93f 100644 --- a/lib/errors.mli +++ b/lib/errors.mli @@ -80,6 +80,7 @@ val iprint : Exninfo.iexn -> Pp.std_ppcmds (** Same as [print], except that the "Please report" part of an anomaly isn't printed (used in Ltac debugging). *) val print_no_report : exn -> Pp.std_ppcmds +val iprint_no_report : Exninfo.iexn -> Pp.std_ppcmds (** Critical exceptions should not be caught and ignored by mistake by inner functions during a [vernacinterp]. They should be handled @@ -87,3 +88,12 @@ val print_no_report : exn -> Pp.std_ppcmds Typical example: [Sys.Break], [Assert_failure], [Anomaly] ... *) val noncritical : exn -> bool + +(** Check whether an exception is handled by some toplevel printer. The + [Anomaly] exception is never handled. *) +val handled : exn -> bool + +(** Prints info which is either an error or + an anomaly and then exits with the appropriate + error code *) +val fatal_error : Pp.std_ppcmds -> bool -> 'a diff --git a/lib/flags.ml b/lib/flags.ml index c8e7f7af..ab4ac03f 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -48,6 +48,8 @@ let batch_mode = ref false type compilation_mode = BuildVo | BuildVio | Vio2Vo let compilation_mode = ref BuildVo +let test_mode = ref false + type async_proofs = APoff | APonLazy | APon let async_proofs_mode = ref APoff type cache = Force @@ -160,7 +162,7 @@ let make_polymorphic_flag b = let program_mode = ref false let is_program_mode () = !program_mode -let warn = ref true +let warn = ref false let make_warn flag = warn := flag; () let if_warn f x = if !warn then f x @@ -206,10 +208,14 @@ let inline_level = ref default_inline_level let set_inline_level = (:=) inline_level let get_inline_level () = !inline_level -(* Disabling native code compilation for conversion and normalization *) -let no_native_compiler = ref Coq_config.no_native_compiler +(* Native code compilation for conversion and normalization *) +let native_compiler = ref false (* Print the mod uid associated to a vo file by the native compiler *) let print_mod_uid = ref false let tactic_context_compat = ref false + +let dump_bytecode = ref false +let set_dump_bytecode = (:=) dump_bytecode +let get_dump_bytecode () = !dump_bytecode diff --git a/lib/flags.mli b/lib/flags.mli index 756d3b85..8e371365 100644 --- a/lib/flags.mli +++ b/lib/flags.mli @@ -15,6 +15,8 @@ val batch_mode : bool ref type compilation_mode = BuildVo | BuildVio | Vio2Vo val compilation_mode : compilation_mode ref +val test_mode : bool ref + type async_proofs = APoff | APonLazy | APon val async_proofs_mode : async_proofs ref type cache = Force @@ -128,12 +130,17 @@ val set_inline_level : int -> unit val get_inline_level : unit -> int val default_inline_level : int -(* Disabling native code compilation for conversion and normalization *) -val no_native_compiler : bool ref +(** Native code compilation for conversion and normalization *) +val native_compiler : bool ref -(* Print the mod uid associated to a vo file by the native compiler *) +(** Print the mod uid associated to a vo file by the native compiler *) val print_mod_uid : bool ref val tactic_context_compat : bool ref (** Set to [true] to trigger the compatibility bugged context matching (old context vs. appcontext) is set. *) + +(** Dump the bytecode after compilation (for debugging purposes) *) +val dump_bytecode : bool ref +val set_dump_bytecode : bool -> unit +val get_dump_bytecode : unit -> bool diff --git a/lib/future.ml b/lib/future.ml index 02d3702d..78a15826 100644 --- a/lib/future.ml +++ b/lib/future.ml @@ -11,21 +11,27 @@ let freeze = ref (fun () -> assert false : unit -> Dyn.t) let unfreeze = ref (fun _ -> () : Dyn.t -> unit) let set_freeze f g = freeze := f; unfreeze := g -exception NotReady of string -exception NotHere of string -let _ = Errors.register_handler (function - | NotReady name -> +let not_ready_msg = ref (fun name -> Pp.strbrk("The value you are asking for ("^name^") is not ready yet. "^ "Please wait or pass "^ "the \"-async-proofs off\" option to CoqIDE to disable "^ "asynchronous script processing and don't pass \"-quick\" to "^ - "coqc.") - | NotHere name -> + "coqc.")) +let not_here_msg = ref (fun name -> Pp.strbrk("The value you are asking for ("^name^") is not available "^ "in this process. If you really need this, pass "^ "the \"-async-proofs off\" option to CoqIDE to disable "^ "asynchronous script processing and don't pass \"-quick\" to "^ - "coqc.") + "coqc.")) + +let customize_not_ready_msg f = not_ready_msg := f +let customize_not_here_msg f = not_here_msg := f + +exception NotReady of string +exception NotHere of string +let _ = Errors.register_handler (function + | NotReady name -> !not_ready_msg name + | NotHere name -> !not_here_msg name | _ -> raise Errors.Unhandled) type fix_exn = Exninfo.iexn -> Exninfo.iexn diff --git a/lib/future.mli b/lib/future.mli index 324d5f7d..adc15e49 100644 --- a/lib/future.mli +++ b/lib/future.mli @@ -91,13 +91,13 @@ val from_here : ?fix_exn:fix_exn -> 'a -> 'a computation * When a future enters the environment a corresponding hook is run to perform * some work. If this fails, then its failure has to be annotated with the * same state id that corresponds to the future computation end. I.e. Qed - * is split into two parts, the lazy one (the future) and the eagher one + * is split into two parts, the lazy one (the future) and the eager one * (the hook), both performing some computations for the same state id. *) val fix_exn_of : 'a computation -> fix_exn (* Run remotely, returns the function to assign. If not blocking (the default) it raises NotReady if forced before the - delage assigns it. *) + delegate assigns it. *) type 'a assignement = [ `Val of 'a | `Exn of Exninfo.iexn | `Comp of 'a computation] val create_delegate : ?blocking:bool -> name:string -> @@ -161,3 +161,6 @@ val print : ('a -> Pp.std_ppcmds) -> 'a computation -> Pp.std_ppcmds Thy are set for the outermos layer of the system, since they have to deal with the whole system state. *) val set_freeze : (unit -> Dyn.t) -> (Dyn.t -> unit) -> unit + +val customize_not_ready_msg : (string -> Pp.std_ppcmds) -> unit +val customize_not_here_msg : (string -> Pp.std_ppcmds) -> unit diff --git a/lib/pp.ml b/lib/pp.ml index 76046a7f..4ed4b177 100644 --- a/lib/pp.ml +++ b/lib/pp.ml @@ -8,13 +8,9 @@ module Glue : sig - (* A left associative glue implements efficient glue operator - when used as left associative. If glue is denoted ++ then + (** The [Glue] module implements a container data structure with + efficient concatenation. *) - a ++ b ++ c ++ d = ((a ++ b) ++ c) ++ d = [d] @ ([c] @ ([b] @ [a])) - - I.e. if the short list is the second argument - *) type 'a t val atom : 'a -> 'a t @@ -22,19 +18,28 @@ module Glue : sig val empty : 'a t val is_empty : 'a t -> bool val iter : ('a -> unit) -> 'a t -> unit - val map : ('a -> 'b) -> 'a t -> 'b t end = struct - type 'a t = 'a list + type 'a t = GEmpty | GLeaf of 'a | GNode of 'a t * 'a t + + let atom x = GLeaf x + + let glue x y = + match x, y with + | GEmpty, _ -> y + | _, GEmpty -> x + | _, _ -> GNode (x,y) + + let empty = GEmpty - let atom x = [x] - let glue x y = y @ x - let empty = [] - let is_empty x = x = [] + let is_empty x = x = GEmpty + + let rec iter f = function + | GEmpty -> () + | GLeaf x -> f x + | GNode (x,y) -> iter f x; iter f y - let iter f g = List.iter f (List.rev g) - let map = List.map end module Tag : @@ -145,21 +150,6 @@ let app = Glue.glue let is_empty g = Glue.is_empty g -let rewrite f p = - let strtoken = function - | Str_len (s, n) -> - let s' = f s in - Str_len (s', String.length s') - | Str_def s -> - Str_def (f s) - in - let rec ppcmd_token = function - | Ppcmd_print x -> Ppcmd_print (strtoken x) - | Ppcmd_box (bt, g) -> Ppcmd_box (bt, Glue.map ppcmd_token g) - | p -> p - in - Glue.map ppcmd_token p - (* Compute length of an UTF-8 encoded string Rem 1 : utf8_length <= String.length (equal if pure ascii) Rem 2 : if used for an iso8859_1 encoded string, the result is @@ -259,7 +249,7 @@ let escape_string s = else escape_at s (i-1) in escape_at s (String.length s - 1) -let qstring s = str ("\""^escape_string s^"\"") +let qstring s = str "\"" ++ str (escape_string s) ++ str "\"" let qs = qstring let quote s = h 0 (str "\"" ++ s ++ str "\"") @@ -372,11 +362,11 @@ let emacs_quote_info_start = "" let emacs_quote_info_end = "" let emacs_quote g = - if !print_emacs then str emacs_quote_start ++ hov 0 g ++ str emacs_quote_end + if !print_emacs then hov 0 (str emacs_quote_start ++ g ++ str emacs_quote_end) else hov 0 g let emacs_quote_info g = - if !print_emacs then str emacs_quote_info_start++fnl() ++ hov 0 g ++ str emacs_quote_info_end + if !print_emacs then hov 0 (str emacs_quote_info_start++ brk(0,0) ++ g ++ brk(0,0) ++ str emacs_quote_info_end) else hov 0 g @@ -434,7 +424,7 @@ type logger = message_level -> std_ppcmds -> unit let make_body info s = emacs_quote (hov 0 (info ++ spc () ++ s)) -let debugbody strm = hov 0 (str "Debug:" ++ spc () ++ strm) +let debugbody strm = emacs_quote_info (hov 0 (str "Debug:" ++ spc () ++ strm)) let warnbody strm = make_body (str "Warning:") strm let errorbody strm = make_body (str "Error:") strm let infobody strm = emacs_quote_info strm @@ -458,6 +448,27 @@ let logger = ref std_logger let make_pp_emacs() = print_emacs:=true; logger:=emacs_logger let make_pp_nonemacs() = print_emacs:=false; logger := std_logger +let ft_logger old_logger ft ~id level mesg = match level with + | Debug _ -> msgnl_with ft (debugbody mesg) + | Info -> msgnl_with ft (infobody mesg) + | Notice -> msgnl_with ft mesg + | Warning -> old_logger ~id:id level mesg + | Error -> old_logger ~id:id 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 feedback_id = ref (Feedback.Edit 0) let feedback_route = ref Feedback.default_route diff --git a/lib/pp.mli b/lib/pp.mli index 5dd2686d..3b1123a9 100644 --- a/lib/pp.mli +++ b/lib/pp.mli @@ -12,6 +12,8 @@ val make_pp_emacs:unit -> unit val make_pp_nonemacs:unit -> unit +val with_output_to_file : string -> ('a -> 'b) -> 'a -> 'b + (** Pretty-printers. *) type std_ppcmds @@ -46,9 +48,6 @@ val eval_ppcmds : std_ppcmds -> std_ppcmds val is_empty : std_ppcmds -> bool (** Test emptyness. *) -val rewrite : (string -> string) -> std_ppcmds -> std_ppcmds -(** [rewrite f pps] applies [f] to all strings that appear in [pps]. *) - (** {6 Derived commands} *) val spc : unit -> std_ppcmds diff --git a/lib/pp_control.ml b/lib/pp_control.ml index 0d224c03..969c1550 100644 --- a/lib/pp_control.ml +++ b/lib/pp_control.ml @@ -20,7 +20,7 @@ let dflt_gp = { margin = 78; max_indent = 50; max_depth = 50; - ellipsis = ".." } + ellipsis = "..." } (* A deeper pretty-printer to print proof scripts *) @@ -84,5 +84,10 @@ 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 - + 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/lib/ppstyle.ml b/lib/ppstyle.ml new file mode 100644 index 00000000..fb334c70 --- /dev/null +++ b/lib/ppstyle.ml @@ -0,0 +1,149 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* assert false + +let set_style tag st = + 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 () = String.Map.bindings !tags + +let parse_config s = + let styles = Terminal.parse s in + let set accu (name, st) = + try String.Map.update name (Some st) accu with Not_found -> accu + in + tags := List.fold_left set !tags styles + +let tag = Pp.Tag.create "ppstyle" + +(** Default tag is to reset everything *) +let default = Terminal.({ + fg_color = Some `DEFAULT; + bg_color = Some `DEFAULT; + bold = Some false; + italic = Some false; + underline = Some false; + negative = Some false; +}) + +let empty = Terminal.make () + +let make_style_stack style_tags = + (** Not thread-safe. We should put a lock somewhere if we print from + different threads. Do we? *) + let style_stack = ref [] in + let peek () = match !style_stack with + | [] -> default (** Anomalous case, but for robustness *) + | st :: _ -> st + in + let push tag = + let style = + try + begin match String.Map.find tag style_tags with + | None -> empty + | Some st -> st + end + with Not_found -> empty + 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 + let () = style_stack := style :: !style_stack in + Terminal.eval style + in + let pop _ = match !style_stack with + | [] -> + (** Something went wrong, we fallback *) + Terminal.eval default + | _ :: rem -> + let () = style_stack := rem in + Terminal.eval (peek ()) + in + let clear () = style_stack := [] in + push, pop, clear + +let error_tag = + let style = Terminal.make ~bold:true ~fg_color:`WHITE ~bg_color:`RED () in + make ~style ["message"; "error"] + +let warning_tag = + let style = Terminal.make ~bold:true ~fg_color:`WHITE ~bg_color:`YELLOW () in + make ~style ["message"; "warning"] + +let debug_tag = + let style = Terminal.make ~bold:true ~fg_color:`WHITE ~bg_color:`MAGENTA () in + make ~style ["message"; "debug"] + +let pp_tag t = match Pp.Tag.prj t tag with +| None -> "" +| Some key -> key + +let init_color_output () = + let push_tag, pop_tag, clear_tag = make_style_stack !tags in + 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 + let open Pp_control in + let () = Format.pp_set_mark_tags !std_ft true in + let () = Format.pp_set_mark_tags !err_ft true in + let () = Format.pp_set_formatter_tag_functions !std_ft tag_handler in + let () = Format.pp_set_formatter_tag_functions !err_ft tag_handler in + let pptag = tag in + let open Pp in + let msg ?header ft strm = + let strm = match header with + | None -> hov 0 strm + | Some (h, t) -> + let tag = Pp.Tag.inj t pptag in + let h = Pp.tag tag (str h ++ str ":") in + hov 0 (h ++ spc () ++ strm) + in + pp_with ~pp_tag ft strm; + Format.pp_print_newline ft (); + Format.pp_print_flush ft (); + (** In case something went wrong, we reset the stack *) + clear_tag (); + in + let logger level strm = match level with + | Debug _ -> msg ~header:("Debug", debug_tag) !std_ft strm + | Info -> msg !std_ft strm + | Notice -> msg !std_ft strm + | Warning -> + let header = ("Warning", warning_tag) in + Flags.if_warn (fun () -> msg ~header !err_ft strm) () + | Error -> msg ~header:("Error", error_tag) !err_ft strm + in + let () = set_logger logger in + () diff --git a/lib/ppstyle.mli b/lib/ppstyle.mli new file mode 100644 index 00000000..f5d6184c --- /dev/null +++ b/lib/ppstyle.mli @@ -0,0 +1,70 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* 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. *) + +val tag : t Pp.Tag.key +(** An annotation for styles *) + +(** {5 Manipulating global styles} *) + +val get_style : t -> Terminal.style option +(** Get the style associated to a tag. *) + +val set_style : t -> Terminal.style option -> unit +(** Set a style associated to a tag. *) + +val clear_styles : unit -> unit +(** Clear all styles. *) + +val parse_config : string -> unit +(** Add all styles from the given string as parsed by {!Terminal.parse}. + Unregistered tags are ignored. *) + +val dump : unit -> (t * Terminal.style option) list +(** Recover the list of known tags together with their current style. *) + +(** {5 Setting color output} *) + +val init_color_output : unit -> unit +(** Once called, all tags defined here will use their current style when + printed. To this end, this function redefines the loggers used when sending + messages to the user. The program will in particular use the formatters + {!Pp_control.std_ft} and {!Pp_control.err_ft} to display those messages, + with additional syle information provided by this module. Be careful this is + not compatible with the Emacs mode! *) + +val pp_tag : Pp.tag_handler +(** Returns the name of a style tag that is understandable by the formatters + that have been inititialized through {!init_color_output}. To be used with + {!Pp.pp_with}. *) + +(** {5 Tags} *) + +val error_tag : t +(** Tag used by the {!Pp.msg_error} function. *) + +val warning_tag : t +(** Tag used by the {!Pp.msg_warning} function. *) + +val debug_tag : t +(** Tag used by the {!Pp.msg_debug} function. *) diff --git a/lib/richpp.mli b/lib/richpp.mli index bf80c8dc..a0d3c374 100644 --- a/lib/richpp.mli +++ b/lib/richpp.mli @@ -20,7 +20,7 @@ type 'annotation located = { of [ppcmds] as a semi-structured document that represents (located) annotations of this string. The [get_annotations] function is used to convert tags into the desired - annotation. If this function returns [None], then no annotation is put. *) + annotation. *) val rich_pp : (Pp.Tag.t -> 'annotation option) -> Pp.std_ppcmds -> 'annotation located Xml_datatype.gxml diff --git a/lib/spawn.ml b/lib/spawn.ml index 9b63be70..851c6a22 100644 --- a/lib/spawn.ml +++ b/lib/spawn.ml @@ -45,26 +45,38 @@ end (* Common code *) let assert_ b s = if not b then Errors.anomaly (Pp.str s) +(* According to http://caml.inria.fr/mantis/view.php?id=5325 + * you can't use the same socket for both writing and reading (may change + * in 4.03 *) let mk_socket_channel () = let open Unix in - let s = socket PF_INET SOCK_STREAM 0 in - bind s (ADDR_INET (inet_addr_loopback,0)); - listen s 1; - match getsockname s with - | ADDR_INET(host, port) -> - s, string_of_inet_addr host ^":"^ string_of_int port + let sr = socket PF_INET SOCK_STREAM 0 in + bind sr (ADDR_INET (inet_addr_loopback,0)); listen sr 1; + let sw = socket PF_INET SOCK_STREAM 0 in + bind sw (ADDR_INET (inet_addr_loopback,0)); listen sw 1; + match getsockname sr, getsockname sw with + | ADDR_INET(host, portr), ADDR_INET(_, portw) -> + (sr, sw), + string_of_inet_addr host + ^":"^ string_of_int portr ^":"^ string_of_int portw | _ -> assert false -let accept s = - let r, _, _ = Unix.select [s] [] [] accept_timeout in +let accept (sr,sw) = + let r, _, _ = Unix.select [sr] [] [] accept_timeout in if r = [] then raise (Failure (Printf.sprintf "The spawned process did not connect back in %2.1fs" accept_timeout)); - let cs, _ = Unix.accept s in - Unix.close s; - let cin, cout = Unix.in_channel_of_descr cs, Unix.out_channel_of_descr cs in + let csr, _ = Unix.accept sr in + Unix.close sr; + let cin = Unix.in_channel_of_descr csr in set_binary_mode_in cin true; + let w, _, _ = Unix.select [sw] [] [] accept_timeout in + if w = [] then raise (Failure (Printf.sprintf + "The spawned process did not connect back in %2.1fs" accept_timeout)); + let csw, _ = Unix.accept sw in + Unix.close sw; + let cout = Unix.out_channel_of_descr csw in set_binary_mode_out cout true; - cs, cin, cout + (csr, csw), cin, cout let handshake cin cout = try @@ -116,7 +128,7 @@ let spawn_pipe env prog args = let cout = Unix.out_channel_of_descr master2worker_w in set_binary_mode_in cin true; set_binary_mode_out cout true; - pid, cin, cout, worker2master_r + pid, cin, cout, (worker2master_r, master2worker_w) let filter_args args = let rec aux = function @@ -180,10 +192,10 @@ let spawn ?(prefer_sock=prefer_sock) ?(env=Unix.environment ()) = let pid, oob_resp, oob_req, cin, cout, main, is_sock = spawn_with_control prefer_sock env prog args in - Unix.set_nonblock main; + Unix.set_nonblock (fst main); let gchan = - if is_sock then ML.async_chan_of_socket main - else ML.async_chan_of_file main in + if is_sock then ML.async_chan_of_socket (fst main) + else ML.async_chan_of_file (fst main) in let alive, watch = true, None in let p = { cin; cout; gchan; pid; oob_resp; oob_req; alive; watch } in p.watch <- Some ( diff --git a/lib/system.ml b/lib/system.ml index 73095f9c..ddc56956 100644 --- a/lib/system.ml +++ b/lib/system.ml @@ -118,7 +118,8 @@ let is_in_system_path filename = let open_trapping_failure name = try open_out_bin name - with e when Errors.noncritical e -> error ("Can't open " ^ name) + with e when Errors.noncritical e -> + errorlabstrm "System.open" (str "Can't open " ++ str name) let try_remove filename = try Sys.remove filename @@ -126,7 +127,8 @@ let try_remove filename = msg_warning (str"Could not remove file " ++ str filename ++ str" which is corrupted!") -let error_corrupted file s = error (file ^": " ^ s ^ ". Try to rebuild it.") +let error_corrupted file s = + errorlabstrm "System" (str file ++ str ": " ++ str s ++ str ". Try to rebuild it.") let input_binary_int f ch = try input_binary_int ch @@ -172,47 +174,42 @@ let skip_in_segment f ch = exception Bad_magic_number of string -let raw_extern_intern magic = - let extern_state filename = - let channel = open_trapping_failure filename in - output_binary_int channel magic; - filename, channel - and intern_state filename = - try - let channel = open_in_bin filename in - if not (Int.equal (input_binary_int filename channel) magic) then - raise (Bad_magic_number filename); - channel - with - | End_of_file -> error_corrupted filename "premature end of file" - | Failure s | Sys_error s -> error_corrupted filename s - in - (extern_state,intern_state) +let raw_extern_state magic filename = + let channel = open_trapping_failure filename in + output_binary_int channel magic; + channel -let extern_intern ?(warn=true) magic = - let (raw_extern,raw_intern) = raw_extern_intern magic in - let extern_state name val_0 = - try - let (filename,channel) = raw_extern name in - try - marshal_out channel val_0; - close_out channel - with reraise -> - let reraise = Errors.push reraise in - let () = try_remove filename in - iraise reraise - with Sys_error s -> error ("System error: " ^ s) - and intern_state paths name = +let raw_intern_state magic filename = + try + let channel = open_in_bin filename in + if not (Int.equal (input_binary_int filename channel) magic) then + raise (Bad_magic_number filename); + channel + with + | End_of_file -> error_corrupted filename "premature end of file" + | Failure s | Sys_error s -> error_corrupted filename s + +let extern_state magic filename val_0 = + try + let channel = raw_extern_state magic filename in try - let _,filename = find_file_in_path ~warn paths name in - let channel = raw_intern filename in - let v = marshal_in filename channel in - close_in channel; - v - with Sys_error s -> - error("System error: " ^ s) - in - (extern_state,intern_state) + marshal_out channel val_0; + close_out channel + with reraise -> + let reraise = Errors.push reraise in + let () = try_remove filename in + iraise reraise + with Sys_error s -> + errorlabstrm "System.extern_state" (str "System error: " ++ str s) + +let intern_state magic filename = + try + let channel = raw_intern_state magic filename in + let v = marshal_in filename channel in + close_in channel; + v + with Sys_error s -> + errorlabstrm "System.intern_state" (str "System error: " ++ str s) let with_magic_number_check f a = try f a diff --git a/lib/system.mli b/lib/system.mli index a3d66d57..247d528b 100644 --- a/lib/system.mli +++ b/lib/system.mli @@ -36,11 +36,13 @@ val find_file_in_path : exception Bad_magic_number of string -val raw_extern_intern : int -> - (string -> string * out_channel) * (string -> in_channel) +val raw_extern_state : int -> string -> out_channel -val extern_intern : ?warn:bool -> int -> - (string -> 'a -> unit) * (CUnix.load_path -> string -> 'a) +val raw_intern_state : int -> string -> in_channel + +val extern_state : int -> string -> 'a -> unit + +val intern_state : int -> string -> 'a val with_magic_number_check : ('a -> 'b) -> 'a -> 'b diff --git a/lib/terminal.ml b/lib/terminal.ml index 0f6b23af..58851ed2 100644 --- a/lib/terminal.ml +++ b/lib/terminal.ml @@ -117,7 +117,7 @@ let is_extended = function | `INDEX _ | `RGB _ -> true | _ -> false -let eval st = +let repr st = let fg = match st.fg_color with | None -> [] | Some c -> @@ -152,7 +152,10 @@ let eval st = | Some true -> [7] | Some false -> [27] in - let tags = fg @ bg @ bold @ italic @ underline @ negative in + fg @ bg @ bold @ italic @ underline @ negative + +let eval st = + let tags = repr st in let tags = List.map string_of_int tags in Printf.sprintf "\027[%sm" (String.concat ";" tags) diff --git a/lib/terminal.mli b/lib/terminal.mli index f308ede3..49172e3c 100644 --- a/lib/terminal.mli +++ b/lib/terminal.mli @@ -46,6 +46,9 @@ val make : ?fg_color:color -> ?bg_color:color -> val merge : style -> style -> style (** [merge s1 s2] returns [s1] with all defined values of [s2] overwritten. *) +val repr : style -> int list +(** Generate the ANSI code representing the given style. *) + val eval : style -> string (** Generate an escape sequence from a style. *) diff --git a/lib/util.ml b/lib/util.ml index a8c25f74..a20dba0f 100644 --- a/lib/util.ml +++ b/lib/util.ml @@ -132,3 +132,14 @@ let map_union f g = function type iexn = Exninfo.iexn let iraise = Exninfo.iraise + +let open_utf8_file_in fname = + let is_bom s = + Int.equal (Char.code s.[0]) 0xEF && + Int.equal (Char.code s.[1]) 0xBB && + Int.equal (Char.code s.[2]) 0xBF + in + let in_chan = open_in fname in + let s = " " in + if input in_chan s 0 3 < 3 || not (is_bom s) then seek_in in_chan 0; + in_chan diff --git a/lib/util.mli b/lib/util.mli index 4fce809c..1dc405fc 100644 --- a/lib/util.mli +++ b/lib/util.mli @@ -110,3 +110,6 @@ val map_union : ('a -> 'c) -> ('b -> 'd) -> ('a, 'b) union -> ('c, 'd) union type 'a until = 'a CSig.until = Stop of 'a | Cont of 'a (** Used for browsable-until structures. *) + +val open_utf8_file_in : string -> in_channel +(** Open an utf-8 encoded file and skip the byte-order mark if any. *) diff --git a/lib/xml_lexer.mll b/lib/xml_lexer.mll index a33be9da..290f2c89 100644 --- a/lib/xml_lexer.mll +++ b/lib/xml_lexer.mll @@ -88,7 +88,8 @@ let error lexbuf e = let newline = ['\n'] let break = ['\r'] let space = [' ' '\t'] -let identchar = ['A'-'Z' 'a'-'z' '_' '0'-'9' ':' '-'] +let identchar = ['A'-'Z' 'a'-'z' '_' '0'-'9' ':' '-' '.'] +let ident = ['A'-'Z' 'a'-'z' '_' ':'] identchar* let entitychar = ['A'-'Z' 'a'-'z'] let pcchar = [^ '\r' '\n' '<' '>' '&'] @@ -226,7 +227,7 @@ and entity = parse { raise (Error EUnterminatedEntity) } and ident_name = parse - | identchar+ + | ident { lexeme lexbuf } | _ | eof { error lexbuf EIdentExpected } @@ -252,7 +253,7 @@ and attributes = parse } and attribute = parse - | identchar+ + | ident { lexeme lexbuf } | _ | eof { error lexbuf EAttributeNameExpected } @@ -281,6 +282,11 @@ and dq_string = parse Buffer.add_char tmp (lexeme_char lexbuf 1); dq_string lexbuf } + | '&' + { + Buffer.add_string tmp (entity lexbuf); + dq_string lexbuf + } | eof { raise (Error EUnterminatedString) } | _ @@ -297,6 +303,11 @@ and q_string = parse Buffer.add_char tmp (lexeme_char lexbuf 1); q_string lexbuf } + | '&' + { + Buffer.add_string tmp (entity lexbuf); + q_string lexbuf + } | eof { raise (Error EUnterminatedString) } | _ diff --git a/lib/xml_parser.mli b/lib/xml_parser.mli index cefb4af8..ac2eab35 100644 --- a/lib/xml_parser.mli +++ b/lib/xml_parser.mli @@ -36,10 +36,10 @@ type t (** Several exceptions can be raised when parsing an Xml document : {ul {li {!Xml.Error} is raised when an xml parsing error occurs. the - {!Xml.error_msg} tells you which error occured during parsing - and the {!Xml.error_pos} can be used to retreive the document - location where the error occured at.} - {li {!Xml.File_not_found} is raised when and error occured while + {!Xml.error_msg} tells you which error occurred during parsing + and the {!Xml.error_pos} can be used to retrieve the document + location where the error occurred at.} + {li {!Xml.File_not_found} is raised when an error occurred while opening a file with the {!Xml.parse_file} function.} } *) @@ -71,13 +71,13 @@ val error : error -> string (** Get the Xml error message as a string. *) val error_msg : error_msg -> string -(** Get the line the error occured at. *) +(** Get the line the error occurred at. *) val line : error_pos -> int -(** Get the relative character range (in current line) the error occured at.*) +(** Get the relative character range (in current line) the error occurred at.*) val range : error_pos -> int * int -(** Get the absolute character range the error occured at. *) +(** Get the absolute character range the error occurred at. *) val abs_range : error_pos -> int * int val pos : Lexing.lexbuf -> error_pos @@ -98,7 +98,7 @@ val make : source -> t in the original Xmllight)}. *) val check_eof : t -> bool -> unit -(** Once the parser is configurated, you can run the parser on a any kind +(** Once the parser is configured, you can run the parser on a any kind of xml document source to parse its contents into an Xml data structure. When [do_not_canonicalize] is set, the XML document is given as diff --git a/lib/xml_printer.ml b/lib/xml_printer.ml index eeddd53c..bbb7b51b 100644 --- a/lib/xml_printer.ml +++ b/lib/xml_printer.ml @@ -46,6 +46,8 @@ let buffer_attr tmp (n,v) = match v.[p] with | '\\' -> output "\\\\" | '"' -> output "\\\"" + | '<' -> output "<" + | '&' -> output "&" | c -> output' c done; output' '"' -- cgit v1.2.3