diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/aux_file.ml | 2 | ||||
| -rw-r--r-- | lib/clib.mllib | 6 | ||||
| -rw-r--r-- | lib/explore.ml | 2 | ||||
| -rw-r--r-- | lib/feedback.ml | 254 | ||||
| -rw-r--r-- | lib/feedback.mli | 97 | ||||
| -rw-r--r-- | lib/flags.ml | 5 | ||||
| -rw-r--r-- | lib/flags.mli | 6 | ||||
| -rw-r--r-- | lib/genarg.mli | 51 | ||||
| -rw-r--r-- | lib/lib.mllib | 1 | ||||
| -rw-r--r-- | lib/minisys.ml | 74 | ||||
| -rw-r--r-- | lib/pp.ml | 164 | ||||
| -rw-r--r-- | lib/pp.mli | 139 | ||||
| -rw-r--r-- | lib/ppstyle.ml | 38 | ||||
| -rw-r--r-- | lib/ppstyle.mli | 14 | ||||
| -rw-r--r-- | lib/richpp.ml | 4 | ||||
| -rw-r--r-- | lib/richpp.mli | 5 | ||||
| -rw-r--r-- | lib/serialize.ml | 120 | ||||
| -rw-r--r-- | lib/serialize.mli | 39 | ||||
| -rw-r--r-- | lib/stateid.ml | 26 | ||||
| -rw-r--r-- | lib/stateid.mli | 11 | ||||
| -rw-r--r-- | lib/system.ml | 74 | ||||
| -rw-r--r-- | lib/unicode.ml | 100 | ||||
| -rw-r--r-- | lib/unicode.mli | 19 | ||||
| -rw-r--r-- | lib/xml_lexer.mli | 44 | ||||
| -rw-r--r-- | lib/xml_lexer.mll | 317 | ||||
| -rw-r--r-- | lib/xml_parser.ml | 232 | ||||
| -rw-r--r-- | lib/xml_parser.mli | 106 | ||||
| -rw-r--r-- | lib/xml_printer.ml | 145 | ||||
| -rw-r--r-- | lib/xml_printer.mli | 29 |
29 files changed, 481 insertions, 1643 deletions
diff --git a/lib/aux_file.ml b/lib/aux_file.ml index c814438dd7..096305b987 100644 --- a/lib/aux_file.ml +++ b/lib/aux_file.ml @@ -88,7 +88,7 @@ let load_aux_file_for vfile = | Sys_error s | Scanf.Scan_failure s | Failure s | Invalid_argument s -> Flags.if_verbose - Pp.msg_warning Pp.(str"Loading file "++str aux_fname++str": "++str s); + Feedback.msg_warning Pp.(str"Loading file "++str aux_fname++str": "++str s); empty_aux_file let set h loc k v = set h (Loc.unloc loc) k v diff --git a/lib/clib.mllib b/lib/clib.mllib index 3c1c5da33c..1e33173ee1 100644 --- a/lib/clib.mllib +++ b/lib/clib.mllib @@ -21,20 +21,16 @@ Control Loc CList CString -Serialize Deque CObj CArray CStack Util Stateid -Feedback Pp Ppstyle -Xml_lexer -Xml_parser -Xml_printer Richpp +Feedback CUnix Envars Aux_file diff --git a/lib/explore.ml b/lib/explore.ml index 587db11563..aa7bddf2b4 100644 --- a/lib/explore.ml +++ b/lib/explore.ml @@ -27,7 +27,7 @@ module Make = functor(S : SearchProblem) -> struct | [i] -> int i | i :: l -> pp_rec l ++ str "." ++ int i in - msg_debug (h 0 (pp_rec p) ++ pp) + Feedback.msg_debug (h 0 (pp_rec p) ++ pp) (*s Depth first search. *) diff --git a/lib/feedback.ml b/lib/feedback.ml index 1a90685de6..d6f580fd16 100644 --- a/lib/feedback.ml +++ b/lib/feedback.ml @@ -7,51 +7,14 @@ (************************************************************************) open Xml_datatype -open Serialize -type message_level = +type level = | Debug of string | Info | Notice | Warning | Error -type message = { - message_level : message_level; - message_content : xml; -} - -let of_message_level = function - | Debug s -> - Serialize.constructor "message_level" "debug" [Xml_datatype.PCData s] - | Info -> Serialize.constructor "message_level" "info" [] - | Notice -> Serialize.constructor "message_level" "notice" [] - | Warning -> Serialize.constructor "message_level" "warning" [] - | Error -> Serialize.constructor "message_level" "error" [] -let to_message_level = - Serialize.do_match "message_level" (fun s args -> match s with - | "debug" -> Debug (Serialize.raw_string args) - | "info" -> Info - | "notice" -> Notice - | "warning" -> Warning - | "error" -> Error - | _ -> raise Serialize.Marshal_error) - -let of_message msg = - let lvl = of_message_level msg.message_level in - let content = Serialize.of_xml msg.message_content in - Xml_datatype.Element ("message", [], [lvl; content]) -let to_message xml = match xml with - | Xml_datatype.Element ("message", [], [lvl; content]) -> { - message_level = to_message_level lvl; - message_content = Serialize.to_xml content } - | _ -> raise Serialize.Marshal_error - -let is_message = function - | Xml_datatype.Element ("message", _, _) -> true - | _ -> false - - type edit_id = int type state_id = Stateid.t type edit_or_state_id = Edit of edit_id | State of state_id @@ -71,8 +34,10 @@ type feedback_content = | GlobDef of Loc.t * string * string * string | FileDependency of string option * string | FileLoaded of string * string + (* Extra metadata *) | Custom of Loc.t * string * xml - | Message of message + (* Old generic messages *) + | Message of level * Richpp.richpp type feedback = { id : edit_or_state_id; @@ -80,92 +45,127 @@ type feedback = { route : route_id; } -let to_feedback_content = do_match "feedback_content" (fun s a -> match s,a with - | "addedaxiom", _ -> AddedAxiom - | "processed", _ -> Processed - | "processingin", [where] -> ProcessingIn (to_string where) - | "incomplete", _ -> Incomplete - | "complete", _ -> Complete - | "globref", [loc; filepath; modpath; ident; ty] -> - GlobRef(to_loc loc, to_string filepath, - to_string modpath, to_string ident, to_string ty) - | "globdef", [loc; ident; secpath; ty] -> - GlobDef(to_loc loc, to_string ident, to_string secpath, to_string ty) - | "errormsg", [loc; s] -> ErrorMsg (to_loc loc, to_string s) - | "inprogress", [n] -> InProgress (to_int n) - | "workerstatus", [ns] -> - let n, s = to_pair to_string to_string ns in - WorkerStatus(n,s) - | "goals", [loc;s] -> Goals (to_loc loc, to_string s) - | "custom", [loc;name;x]-> Custom (to_loc loc, to_string name, x) - | "filedependency", [from; dep] -> - FileDependency (to_option to_string from, to_string dep) - | "fileloaded", [dirpath; filename] -> - FileLoaded (to_string dirpath, to_string filename) - | "message", [m] -> Message (to_message m) - | _ -> raise Marshal_error) -let of_feedback_content = function - | AddedAxiom -> constructor "feedback_content" "addedaxiom" [] - | Processed -> constructor "feedback_content" "processed" [] - | ProcessingIn where -> - constructor "feedback_content" "processingin" [of_string where] - | Incomplete -> constructor "feedback_content" "incomplete" [] - | Complete -> constructor "feedback_content" "complete" [] - | GlobRef(loc, filepath, modpath, ident, ty) -> - constructor "feedback_content" "globref" [ - of_loc loc; - of_string filepath; - of_string modpath; - of_string ident; - of_string ty ] - | GlobDef(loc, ident, secpath, ty) -> - constructor "feedback_content" "globdef" [ - of_loc loc; - of_string ident; - of_string secpath; - of_string ty ] - | ErrorMsg(loc, s) -> - constructor "feedback_content" "errormsg" [of_loc loc; of_string s] - | InProgress n -> constructor "feedback_content" "inprogress" [of_int n] - | WorkerStatus(n,s) -> - constructor "feedback_content" "workerstatus" - [of_pair of_string of_string (n,s)] - | Goals (loc,s) -> - constructor "feedback_content" "goals" [of_loc loc;of_string s] - | Custom (loc, name, x) -> - constructor "feedback_content" "custom" [of_loc loc; of_string name; x] - | FileDependency (from, depends_on) -> - constructor "feedback_content" "filedependency" [ - of_option of_string from; - of_string depends_on] - | FileLoaded (dirpath, filename) -> - constructor "feedback_content" "fileloaded" [ - of_string dirpath; - of_string filename ] - | Message m -> constructor "feedback_content" "message" [ of_message m ] - -let of_edit_or_state_id = function - | Edit id -> ["object","edit"], of_edit_id id - | State id -> ["object","state"], Stateid.to_xml id - -let of_feedback msg = - let content = of_feedback_content msg.contents in - let obj, id = of_edit_or_state_id msg.id in - let route = string_of_int msg.route in - Element ("feedback", obj @ ["route",route], [id;content]) -let to_feedback xml = match xml with - | Element ("feedback", ["object","edit";"route",route], [id;content]) -> { - id = Edit(to_edit_id id); - route = int_of_string route; - contents = to_feedback_content content } - | Element ("feedback", ["object","state";"route",route], [id;content]) -> { - id = State(Stateid.of_xml id); - route = int_of_string route; - contents = to_feedback_content content } - | _ -> raise Marshal_error - -let is_feedback = function - | Element ("feedback", _, _) -> true - | _ -> false - let default_route = 0 + +(** Feedback and logging *) +open Pp +open Pp_control + +type logger = level -> std_ppcmds -> unit + +let msgnl_with fmt strm = msg_with fmt (strm ++ fnl ()) +let msgnl strm = msgnl_with !std_ft strm + +(* 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 = str "Debug:" ++ spc () +let info_str = mt () +let warn_str = str "Warning:" ++ spc () +let err_str = str "Error:" ++ spc () + +let make_body quoter info s = quoter (hov 0 (info ++ s)) + +(* Generic logger *) +let gen_logger dbg err level msg = match level with + | Debug _ -> msgnl (make_body dbg dbg_str msg) + | Info -> msgnl (make_body dbg info_str msg) + | Notice -> msgnl msg + | Warning -> Flags.if_warn (fun () -> + msgnl_with !err_ft (make_body err warn_str msg)) () + | Error -> msgnl_with !err_ft (make_body err err_str msg) + +(** Standard loggers *) +let std_logger = gen_logger (fun x -> x) (fun x -> x) + +(* Color logger *) +let color_terminal_logger level strm = + let msg = Ppstyle.color_msg in + match level with + | Debug _ -> msg ~header:("Debug", Ppstyle.debug_tag) !std_ft strm + | Info -> msg !std_ft strm + | Notice -> msg !std_ft strm + | Warning -> + let header = ("Warning", Ppstyle.warning_tag) in + Flags.if_warn (fun () -> msg ~header !err_ft strm) () + | Error -> msg ~header:("Error", Ppstyle.error_tag) !err_ft strm + +(* 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 + +let logger = ref std_logger +let set_logger l = logger := l + +let msg_info x = !logger Info x +let msg_notice x = !logger Notice x +let msg_warning x = !logger Warning x +let msg_error x = !logger Error x +let msg_debug x = !logger (Debug "_") x + +(** Feeders *) +let feeder = ref ignore +let set_feeder f = feeder := f + +let feedback_id = ref (Edit 0) +let feedback_route = ref default_route + +let set_id_for_feedback ?(route=default_route) i = + feedback_id := i; feedback_route := route + +let feedback ?id ?route what = + !feeder { + contents = what; + route = Option.default !feedback_route route; + id = Option.default !feedback_id id; + } + +let feedback_logger lvl msg = + feedback ~route:!feedback_route ~id:!feedback_id + (Message (lvl, Richpp.richpp_of_pp msg)) + +(* Output to file *) +let ft_logger old_logger ft 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 level mesg + | Error -> old_logger 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 + diff --git a/lib/feedback.mli b/lib/feedback.mli index 0d8e20230d..50ffd22db9 100644 --- a/lib/feedback.mli +++ b/lib/feedback.mli @@ -9,27 +9,19 @@ open Xml_datatype (* Old plain messages (used to be in Pp) *) -type message_level = +type level = | Debug of string | Info | Notice | Warning | Error -type message = { - message_level : message_level; - message_content : xml; -} - -val of_message : message -> xml -val to_message : xml -> message -val is_message : xml -> bool - (** Coq "semantic" infos obtained during parsing/execution *) type edit_id = int type state_id = Stateid.t type edit_or_state_id = Edit of edit_id | State of state_id + type route_id = int val default_route : route_id @@ -54,15 +46,88 @@ type feedback_content = (* Extra metadata *) | Custom of Loc.t * string * xml (* Old generic messages *) - | Message of message + | Message of level * Richpp.richpp type feedback = { - id : edit_or_state_id; (* The document part concerned *) + id : edit_or_state_id; (* The document part concerned *) contents : feedback_content; (* The payload *) - route : route_id; (* Extra routing info *) + route : route_id; (* Extra routing info *) } -val of_feedback : feedback -> xml -val to_feedback : xml -> feedback -val is_feedback : xml -> bool +(** {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 = 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 + +val color_terminal_logger : logger +(* This logger will apply the proper {!Pp_style} tags, and in + particular use the formatters {!Pp_control.std_ft} and + {!Pp_control.err_ft} to display those messages. Be careful this is + not compatible with the Emacs mode! *) + +(** [feedback_logger] will produce feedback messages instead IO events *) +val feedback_logger : logger +val emacs_logger : logger + + +(** [set_feeder] A feeder processes the feedback, [ignore] by default *) +val set_feeder : (feedback -> unit) -> unit + +(** [feedback ?id ?route fb] produces feedback fb, with [route] and + [id] set appropiatedly, if absent, it will use the defaults set by + [set_id_for_feedback] *) +val feedback : + ?id:edit_or_state_id -> ?route:route_id -> feedback_content -> unit + +(** [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 +possible don't mix it with goal output (prefer msg_info or +msg_warning) so that interfaces can dispatch outputs easily. Once all +interfaces use the xml-like protocol this constraint can be +relaxed. *) +(* Should we advertise these functions more? Should they be the ONLY + allowed way to output something? *) + +val msg_info : Pp.std_ppcmds -> unit +(** Message that displays information, usually in verbose mode, such as [Foobar + is defined] *) + +val msg_notice : Pp.std_ppcmds -> unit +(** Message that should be displayed, such as [Print Foo] or [Show Bar]. *) + +val msg_warning : Pp.std_ppcmds -> unit +(** Message indicating that something went wrong, but without serious + consequences. *) + +val msg_error : Pp.std_ppcmds -> unit +(** Message indicating that something went really wrong, though still + recoverable; otherwise an exception would have been raised. *) + +val msg_debug : Pp.std_ppcmds -> unit +(** For debugging purposes *) + + + diff --git a/lib/flags.ml b/lib/flags.ml index 9a209a2b3e..ba19c7a63b 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -69,11 +69,15 @@ let priority_of_string = function | "low" -> Low | "high" -> High | _ -> raise (Invalid_argument "priority_of_string") +type tac_error_filter = [ `None | `Only of string list | `All ] +let async_proofs_tac_error_resilience = ref (`Only [ "par" ; "curly" ]) +let async_proofs_cmd_error_resilience = ref true let async_proofs_is_worker () = !async_proofs_worker_id <> "master" let async_proofs_is_master () = !async_proofs_mode = APon && !async_proofs_worker_id = "master" +let async_proofs_delegation_threshold = ref 0.03 let debug = ref false let in_debugger = ref false @@ -221,6 +225,7 @@ let native_compiler = ref false let print_mod_uid = ref false let tactic_context_compat = ref false +let profile_ltac = ref false let dump_bytecode = ref false let set_dump_bytecode = (:=) dump_bytecode diff --git a/lib/flags.mli b/lib/flags.mli index f52a14a303..8fe64d24fa 100644 --- a/lib/flags.mli +++ b/lib/flags.mli @@ -35,6 +35,10 @@ type priority = Low | High val async_proofs_worker_priority : priority ref val string_of_priority : priority -> string val priority_of_string : string -> priority +type tac_error_filter = [ `None | `Only of string list | `All ] +val async_proofs_tac_error_resilience : tac_error_filter ref +val async_proofs_cmd_error_resilience : bool ref +val async_proofs_delegation_threshold : float ref val debug : bool ref val in_debugger : bool ref @@ -144,6 +148,8 @@ val tactic_context_compat : bool ref (** Set to [true] to trigger the compatibility bugged context matching (old context vs. appcontext) is set. *) +val profile_ltac : bool ref + (** Dump the bytecode after compilation (for debugging purposes) *) val dump_bytecode : bool ref val set_dump_bytecode : bool -> unit diff --git a/lib/genarg.mli b/lib/genarg.mli index b8bb6af04a..d7ad9b93b4 100644 --- a/lib/genarg.mli +++ b/lib/genarg.mli @@ -6,6 +6,8 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +(** Generic arguments used by the extension mechanisms of several Coq ASTs. *) + (** The route of a generic argument, from parsing to evaluation. In the following diagram, "object" can be tactic_expr, constr, tactic_arg, etc. @@ -34,36 +36,10 @@ In the following diagram, "object" can be tactic_expr, constr, tactic_arg, etc. effective use {% \end{%}verbatim{% }%} -To distinguish between the uninterpreted (raw), globalized and +To distinguish between the uninterpreted, globalized and interpreted worlds, we annotate the type [generic_argument] by a -phantom argument which is either [constr_expr], [glob_constr] or -[constr]. +phantom argument. -Transformation for each type : -{% \begin{%}verbatim{% }%} -tag raw open type cooked closed type - -BoolArgType bool bool -IntArgType int int -IntOrVarArgType int or_var int -StringArgType string (parsed w/ "") string -PreIdentArgType string (parsed w/o "") (vernac only) -IdentArgType true identifier identifier -IdentArgType false identifier (pattern_ident) identifier -IntroPatternArgType intro_pattern_expr intro_pattern_expr -VarArgType identifier located identifier -RefArgType reference global_reference -QuantHypArgType quantified_hypothesis quantified_hypothesis -ConstrArgType constr_expr constr -ConstrMayEvalArgType constr_expr may_eval constr -OpenConstrArgType open_constr_expr open_constr -ConstrWithBindingsArgType constr_expr with_bindings constr with_bindings -BindingsArgType constr_expr bindings constr bindings -List0ArgType of argument_type -List1ArgType of argument_type -OptArgType of argument_type -ExtraArgType of string '_a '_b -{% \end{%}verbatim{% }%} *) (** {5 Generic types} *) @@ -77,14 +53,14 @@ sig val name : string -> any option end +(** Generic types. The first parameter is the OCaml lowest level, the second one + is the globalized level, and third one the internalized level. *) type (_, _, _) genarg_type = | ExtraArg : ('a, 'b, 'c) ArgT.tag -> ('a, 'b, 'c) genarg_type | ListArg : ('a, 'b, 'c) genarg_type -> ('a list, 'b list, 'c list) genarg_type | OptArg : ('a, 'b, 'c) genarg_type -> ('a option, 'b option, 'c option) genarg_type | PairArg : ('a1, 'b1, 'c1) genarg_type * ('a2, 'b2, 'c2) genarg_type -> ('a1 * 'a2, 'b1 * 'b2, 'c1 * 'c2) genarg_type -(** Generic types. ['raw] is the OCaml lowest level, ['glob] is the globalized - one, and ['top] the internalized one. *) type 'a uniform_genarg_type = ('a, 'a, 'a) genarg_type (** Alias for concision when the three types agree. *) @@ -99,21 +75,18 @@ val create_arg : string -> ('raw, 'glob, 'top) genarg_type (** {5 Specialized types} *) (** All of [rlevel], [glevel] and [tlevel] must be non convertible - to ensure the injectivity of the type inference from type - ['co generic_argument] to [('a,'co) abstract_argument_type]; - this guarantees that, for 'co fixed, the type of - out_gen is monomorphic over 'a, hence type-safe -*) + to ensure the injectivity of the GADT type inference. *) type rlevel = [ `rlevel ] type glevel = [ `glevel ] type tlevel = [ `tlevel ] +(** Generic types at a fixed level. The first parameter embeds the OCaml type + and the second one the level. *) type (_, _) abstract_argument_type = | Rawwit : ('a, 'b, 'c) genarg_type -> ('a, rlevel) abstract_argument_type | Glbwit : ('a, 'b, 'c) genarg_type -> ('b, glevel) abstract_argument_type | Topwit : ('a, 'b, 'c) genarg_type -> ('c, tlevel) abstract_argument_type -(** Type at level ['co] represented by an OCaml value of type ['a]. *) type 'a raw_abstract_argument_type = ('a, rlevel) abstract_argument_type (** Specialized type at raw level. *) @@ -207,9 +180,11 @@ sig end -(** {5 Basic generic type constructors} *) +(** {5 Compatibility layer} + +The functions below are aliases for generic_type constructors. -(** {6 Parameterized types} *) +*) val wit_list : ('a, 'b, 'c) genarg_type -> ('a list, 'b list, 'c list) genarg_type val wit_opt : ('a, 'b, 'c) genarg_type -> ('a option, 'b option, 'c option) genarg_type diff --git a/lib/lib.mllib b/lib/lib.mllib index 2be435f6ff..a6c09058dd 100644 --- a/lib/lib.mllib +++ b/lib/lib.mllib @@ -3,6 +3,7 @@ Bigint Segmenttree Unicodetable Unicode +Minisys System CThread Spawn diff --git a/lib/minisys.ml b/lib/minisys.ml new file mode 100644 index 0000000000..25e4d79c4e --- /dev/null +++ b/lib/minisys.ml @@ -0,0 +1,74 @@ +(************************************************************************) +(* 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 *) +(************************************************************************) + +(** Minisys regroups some code that used to be in System. + Unlike System, this module has no dependency and could + be used for initial compilation target such as coqdep_boot. + The functions here are still available in System thanks to + an include. For the signature, look at the top of system.mli +*) + +(** Dealing with directories *) + +type unix_path = string (* path in unix-style, with '/' separator *) + +type file_kind = + | FileDir of unix_path * (* basename of path: *) string + | FileRegular of string (* basename of file *) + +(* Copy of Filename.concat but assuming paths to always be POSIX *) + +let (//) dirname filename = + let l = String.length dirname in + if l = 0 || dirname.[l-1] = '/' + then dirname ^ filename + else dirname ^ "/" ^ filename + +(* Excluding directories; We avoid directories starting with . as well + as CVS and _darcs and any subdirs given via -exclude-dir *) + +let skipped_dirnames = ref ["CVS"; "_darcs"] + +let exclude_directory f = skipped_dirnames := f :: !skipped_dirnames + +let ok_dirname f = + not (f = "") && f.[0] != '.' && + not (List.mem f !skipped_dirnames) (*&& + (match Unicode.ident_refutation f with None -> true | _ -> false)*) + +(* Check directory can be opened *) + +let exists_dir dir = + try Sys.is_directory dir with Sys_error _ -> false + +let check_unix_dir warn dir = + if (Sys.os_type = "Win32" || Sys.os_type = "Cygwin") && + (String.length dir > 2 && dir.[1] = ':' || + String.contains dir '\\' || + String.contains dir ';') + then warn ("assuming " ^ dir ^ + " to be a Unix path even if looking like a Win32 path.") + +let apply_subdir f path name = + (* we avoid all files and subdirs starting by '.' (e.g. .svn) *) + (* as well as skipped files like CVS, ... *) + if ok_dirname name then + let path = if path = "." then name else path//name in + match try (Unix.stat path).Unix.st_kind with Unix.Unix_error _ -> Unix.S_BLK with + | Unix.S_DIR -> f (FileDir (path,name)) + | Unix.S_REG -> f (FileRegular name) + | _ -> () + +let readdir dir = try Sys.readdir dir with any -> [||] + +let process_directory f path = + Array.iter (apply_subdir f path) (readdir path) + +let process_subdirectories f path = + let f = function FileDir (path,base) -> f path base | FileRegular _ -> () in + process_directory f path @@ -64,13 +64,6 @@ end open Pp_control -(* This should not be used outside of this file. Use - Flags.print_emacs instead. This one is updated when reading - command line options. This was the only way to make [Pp] depend on - an option without creating a circularity: [Flags] -> [Util] -> - [Pp] -> [Flags] *) -let print_emacs = ref false - (* The different kinds of blocks are: \begin{description} \item[hbox:] Horizontal block no line breaking; @@ -339,175 +332,23 @@ let pp_dirs ?pp_tag ft = let () = Format.pp_print_flush ft () in Exninfo.iraise reraise - - -(* pretty print on stdout and stderr *) - -(* 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_info_start = "<infomsg>" -let emacs_quote_info_end = "</infomsg>" - -let emacs_quote g = - 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 hov 0 (str emacs_quote_info_start++ brk(0,0) ++ g ++ brk(0,0) ++ str emacs_quote_info_end) - else hov 0 g - - (* pretty printing functions WITHOUT FLUSH *) let pp_with ?pp_tag ft strm = pp_dirs ?pp_tag ft (Glue.atom (Ppdir_ppcmds strm)) -let ppnl_with ft strm = - pp_dirs ft (Glue.atom (Ppdir_ppcmds (strm ++ fnl ()))) - (* pretty printing functions WITH FLUSH *) let msg_with ft strm = pp_dirs ft (Glue.atom(Ppdir_ppcmds strm) ++ Glue.atom(Ppdir_print_flush)) -let msgnl_with ft strm = - pp_dirs ft (Glue.atom(Ppdir_ppcmds strm) ++ Glue.atom(Ppdir_print_newline)) - -(* pretty printing functions WITHOUT FLUSH *) -let pp x = pp_with !std_ft x -let ppnl x = ppnl_with !std_ft x -let pperr x = pp_with !err_ft x -let pperrnl x = ppnl_with !err_ft x -let message s = ppnl (str s) -let pp_flush x = Format.pp_print_flush !std_ft x -let pperr_flush x = Format.pp_print_flush !err_ft x -let flush_all () = - flush stderr; flush stdout; pp_flush (); pperr_flush () - -(* pretty printing functions WITH FLUSH *) -let msg x = msg_with !std_ft x -let msgnl x = msgnl_with !std_ft x -let msgerr x = msg_with !err_ft x -let msgerrnl x = msgnl_with !err_ft x - -(* Logging management *) - -type message_level = Feedback.message_level = - | Debug of string - | Info - | Notice - | Warning - | Error - -type message = Feedback.message = { - message_level : message_level; - message_content : Xml_datatype.xml; -} - -let of_message = Feedback.of_message -let to_message = Feedback.to_message -let is_message = Feedback.is_message - -type logger = message_level -> std_ppcmds -> unit - -let make_body info s = - emacs_quote (hov 0 (info ++ spc () ++ s)) - -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 - -let std_logger ~id:_ level msg = match level with -| Debug _ -> msgnl (debugbody msg) -| Info -> msgnl (hov 0 msg) -| Notice -> msgnl msg -| Warning -> Flags.if_warn (fun () -> msgnl_with !err_ft (warnbody msg)) () -| Error -> msgnl_with !err_ft (errorbody msg) - -let emacs_logger ~id:_ level mesg = match level with -| Debug _ -> msgnl (debugbody mesg) -| Info -> msgnl (infobody mesg) -| Notice -> msgnl mesg -| Warning -> Flags.if_warn (fun () -> msgnl_with !err_ft (warnbody mesg)) () -| Error -> msgnl_with !err_ft (errorbody mesg) - -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 - (* If mixing some output and a goal display, please use msg_warning, so that interfaces (proofgeneral for example) can easily dispatch them to different windows. *) -let msg_info x = !logger ~id:!feedback_id Info x -let msg_notice x = !logger ~id:!feedback_id Notice x -let msg_warning x = !logger ~id:!feedback_id Warning x -let msg_error x = !logger ~id:!feedback_id Error x -let msg_debug x = !logger ~id:!feedback_id (Debug "_") x - -let set_logger l = logger := (fun ~id:_ lvl msg -> l lvl msg) - -let std_logger lvl msg = std_logger ~id:!feedback_id lvl msg - -(** Feedback *) - -let feeder = ref ignore -let set_id_for_feedback ?(route=Feedback.default_route) i = - feedback_id := i; feedback_route := route -let feedback ?state_id ?edit_id ?route what = - !feeder { - Feedback.contents = what; - Feedback.route = Option.default !feedback_route route; - Feedback.id = - match state_id, edit_id with - | Some id, _ -> Feedback.State id - | None, Some eid -> Feedback.Edit eid - | None, None -> !feedback_id; - } -let set_feeder f = feeder := f -let get_id_for_feedback () = !feedback_id, !feedback_route - -(** Utility *) - +(** Output to a string formatter *) let string_of_ppcmds c = - msg_with Format.str_formatter c; + Format.fprintf Format.str_formatter "@[%a@]" msg_with c; Format.flush_str_formatter () -let log_via_feedback printer = logger := (fun ~id lvl msg -> - !feeder { - Feedback.contents = Feedback.Message { - message_level = lvl; - message_content = printer msg }; - Feedback.route = !feedback_route; - Feedback.id = id }) - (* Copy paste from Util *) let pr_comma () = str "," ++ spc () @@ -597,3 +438,4 @@ let prvect_with_sep sep elem v = prvecti_with_sep sep (fun _ -> elem) v let prvect elem v = prvect_with_sep mt elem v let surround p = hov 1 (str"(" ++ p ++ str")") + diff --git a/lib/pp.mli b/lib/pp.mli index 04a60a7c8d..a18744c376 100644 --- a/lib/pp.mli +++ b/lib/pp.mli @@ -6,32 +6,24 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(** Modify pretty printing functions behavior for emacs ouput (special - chars inserted at some places). This function should called once in - module [Options], that's all. *) -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 (** {6 Formatting commands} *) -val str : string -> std_ppcmds +val str : string -> std_ppcmds val stras : int * string -> std_ppcmds -val brk : int * int -> std_ppcmds -val tbrk : int * int -> std_ppcmds -val tab : unit -> std_ppcmds -val fnl : unit -> std_ppcmds -val pifb : unit -> std_ppcmds -val ws : int -> std_ppcmds -val mt : unit -> std_ppcmds -val ismt : std_ppcmds -> bool - -val comment : int -> std_ppcmds +val brk : int * int -> std_ppcmds +val tbrk : int * int -> std_ppcmds +val tab : unit -> std_ppcmds +val fnl : unit -> std_ppcmds +val pifb : unit -> std_ppcmds +val ws : int -> std_ppcmds +val mt : unit -> std_ppcmds +val ismt : std_ppcmds -> bool + +val comment : int -> std_ppcmds val comments : ((int * int) * string) list ref (** {6 Manipulation commands} *) @@ -100,87 +92,10 @@ sig (** Project an object from a tag. *) end -type tag_handler = Tag.t -> Format.tag - val tag : Tag.t -> std_ppcmds -> std_ppcmds val open_tag : Tag.t -> std_ppcmds val close_tag : unit -> std_ppcmds -(** {6 Sending messages to the user} *) -type message_level = Feedback.message_level = - | Debug of string - | Info - | Notice - | Warning - | Error - -type message = Feedback.message = { - message_level : message_level; - message_content : Xml_datatype.xml; -} - -type logger = message_level -> std_ppcmds -> unit - -(** {6 output functions} - -[msg_notice] do not put any decoration on output by default. If -possible don't mix it with goal output (prefer msg_info or -msg_warning) so that interfaces can dispatch outputs easily. Once all -interfaces use the xml-like protocol this constraint can be -relaxed. *) -(* Should we advertise these functions more? Should they be the ONLY - allowed way to output something? *) - -val msg_info : std_ppcmds -> unit -(** Message that displays information, usually in verbose mode, such as [Foobar - is defined] *) - -val msg_notice : std_ppcmds -> unit -(** Message that should be displayed, such as [Print Foo] or [Show Bar]. *) - -val msg_warning : std_ppcmds -> unit -(** Message indicating that something went wrong, but without serious - consequences. *) - -val msg_error : std_ppcmds -> unit -(** Message indicating that something went really wrong, though still - recoverable; otherwise an exception would have been raised. *) - -val msg_debug : std_ppcmds -> unit -(** For debugging purposes *) - -val std_logger : logger -(** Standard logging function *) - -val set_logger : logger -> unit - -val log_via_feedback : (std_ppcmds -> Xml_datatype.xml) -> unit - -val of_message : message -> Xml_datatype.xml -val to_message : Xml_datatype.xml -> message -val is_message : Xml_datatype.xml -> bool - - -(** {6 Feedback sent, even asynchronously, to the user interface} *) - -(* This stuff should be available to most of the system, line msg_* above. - * But I'm unsure this is the right place, especially for the global edit_id. - * - * 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 assigns 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. *) - -val feedback : - ?state_id:Feedback.state_id -> ?edit_id:Feedback.edit_id -> - ?route:Feedback.route_id -> Feedback.feedback_content -> unit - -val set_id_for_feedback : - ?route:Feedback.route_id -> Feedback.edit_or_state_id -> unit -val set_feeder : (Feedback.feedback -> unit) -> unit -val get_id_for_feedback : unit -> Feedback.edit_or_state_id * Feedback.route_id - (** {6 Utilities} *) val string_of_ppcmds : std_ppcmds -> string @@ -251,31 +166,13 @@ val surround : std_ppcmds -> std_ppcmds val pr_vertical_list : ('b -> std_ppcmds) -> 'b list -> std_ppcmds -(** {6 Low-level pretty-printing functions {% \emph{%}without flush{% }%}. } *) - -val pp_with : ?pp_tag:tag_handler -> Format.formatter -> std_ppcmds -> unit - -(** {6 Pretty-printing functions {% \emph{%}without flush{% }%} on [stdout] and [stderr]. } *) - -(** These functions are low-level interface to printing and should not be used - in usual code. Consider using the [msg_*] function family instead. *) +(** {6 Low-level pretty-printing functions with and without flush} *) -val pp : std_ppcmds -> unit -val ppnl : std_ppcmds -> unit -val pperr : std_ppcmds -> unit -val pperrnl : std_ppcmds -> unit -val pperr_flush : unit -> unit -val pp_flush : unit -> unit -val flush_all: unit -> unit - -(** {6 Deprecated functions} *) - -(** DEPRECATED. Do not use in newly written code. *) +(** FIXME: These ignore the logging settings and call [Format] directly *) +type tag_handler = Tag.t -> Format.tag -val msg_with : Format.formatter -> std_ppcmds -> unit +(** [msg_with fmt pp] Print [pp] to [fmt] and flush [fmt] *) +val msg_with : Format.formatter -> std_ppcmds -> unit -val msg : std_ppcmds -> unit -val msgnl : std_ppcmds -> unit -val msgerr : std_ppcmds -> unit -val msgerrnl : std_ppcmds -> unit -val message : string -> unit (** = pPNL *) +(** [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 diff --git a/lib/ppstyle.ml b/lib/ppstyle.ml index 3ecaac0391..b068788c92 100644 --- a/lib/ppstyle.ml +++ b/lib/ppstyle.ml @@ -107,8 +107,11 @@ let pp_tag t = match Pp.Tag.prj t tag with | None -> "" | Some key -> key +let clear_tag_fn = ref (fun () -> ()) + let init_color_output () = let push_tag, pop_tag, clear_tag = make_style_stack !tags in + clear_tag_fn := clear_tag; let tag_handler = { Format.mark_open_tag = push_tag; Format.mark_close_tag = pop_tag; @@ -116,34 +119,23 @@ let init_color_output () = 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 + 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 color_msg ?header ft strm = let pptag = tag in let open Pp in - let msg ?header ft strm = - let strm = match header with + 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 - () + 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_fn () diff --git a/lib/ppstyle.mli b/lib/ppstyle.mli index 97b5869f9b..1cd701ed4e 100644 --- a/lib/ppstyle.mli +++ b/lib/ppstyle.mli @@ -11,7 +11,8 @@ (** {5 Style tags} *) -type t +type t = string + (** Style tags *) val make : ?style:Terminal.style -> string list -> t @@ -46,12 +47,11 @@ val dump : unit -> (t * Terminal.style option) list (** {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 color_msg : ?header:string * Format.tag -> + Format.formatter -> Pp.std_ppcmds -> unit +(** {!color_msg ?header fmt pp} will format according to the tags + defined in this file *) val pp_tag : Pp.tag_handler (** Returns the name of a style tag that is understandable by the formatters diff --git a/lib/richpp.ml b/lib/richpp.ml index fe3edd99ca..a98273edb2 100644 --- a/lib/richpp.ml +++ b/lib/richpp.ml @@ -194,7 +194,3 @@ let raw_print xml = let () = print xml in Buffer.contents buf -let of_richpp x = Element ("richpp", [], [x]) -let to_richpp xml = match xml with -| Element ("richpp", [], [x]) -> x -| _ -> raise Serialize.Marshal_error diff --git a/lib/richpp.mli b/lib/richpp.mli index 807d52aba4..287d265a8f 100644 --- a/lib/richpp.mli +++ b/lib/richpp.mli @@ -57,10 +57,7 @@ val richpp_of_string : string -> richpp val repr : richpp -> Xml_datatype.xml (** Observe the styled text as XML *) -(** {5 Serialization} *) - -val of_richpp : richpp -> Xml_datatype.xml -val to_richpp : Xml_datatype.xml -> richpp +(** {5 Debug/Compat} *) (** Represent the semi-structured document as a string, dropping any additional information. *) diff --git a/lib/serialize.ml b/lib/serialize.ml deleted file mode 100644 index 685ec6049c..0000000000 --- a/lib/serialize.ml +++ /dev/null @@ -1,120 +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 *) -(************************************************************************) - -open Xml_datatype - -exception Marshal_error - -(** Utility functions *) - -let rec get_attr attr = function - | [] -> raise Not_found - | (k, v) :: l when CString.equal k attr -> v - | _ :: l -> get_attr attr l - -let massoc x l = - try get_attr x l - with Not_found -> raise Marshal_error - -let constructor t c args = Element (t, ["val", c], args) -let do_match t mf = function - | Element (s, attrs, args) when CString.equal s t -> - let c = massoc "val" attrs in - mf c args - | _ -> raise Marshal_error - -let singleton = function - | [x] -> x - | _ -> raise Marshal_error - -let raw_string = function - | [] -> "" - | [PCData s] -> s - | _ -> raise Marshal_error - -(** Base types *) - -let of_unit () = Element ("unit", [], []) -let to_unit : xml -> unit = function - | Element ("unit", [], []) -> () - | _ -> raise Marshal_error - -let of_bool (b : bool) : xml = - if b then constructor "bool" "true" [] - else constructor "bool" "false" [] -let to_bool : xml -> bool = do_match "bool" (fun s _ -> match s with - | "true" -> true - | "false" -> false - | _ -> raise Marshal_error) - -let of_list (f : 'a -> xml) (l : 'a list) = - Element ("list", [], List.map f l) -let to_list (f : xml -> 'a) : xml -> 'a list = function - | Element ("list", [], l) -> List.map f l - | _ -> raise Marshal_error - -let of_option (f : 'a -> xml) : 'a option -> xml = function - | None -> Element ("option", ["val", "none"], []) - | Some x -> Element ("option", ["val", "some"], [f x]) -let to_option (f : xml -> 'a) : xml -> 'a option = function - | Element ("option", ["val", "none"], []) -> None - | Element ("option", ["val", "some"], [x]) -> Some (f x) - | _ -> raise Marshal_error - -let of_string (s : string) : xml = Element ("string", [], [PCData s]) -let to_string : xml -> string = function - | Element ("string", [], l) -> raw_string l - | _ -> raise Marshal_error - -let of_int (i : int) : xml = Element ("int", [], [PCData (string_of_int i)]) -let to_int : xml -> int = function - | Element ("int", [], [PCData s]) -> - (try int_of_string s with Failure _ -> raise Marshal_error) - | _ -> raise Marshal_error - -let of_pair (f : 'a -> xml) (g : 'b -> xml) (x : 'a * 'b) : xml = - Element ("pair", [], [f (fst x); g (snd x)]) -let to_pair (f : xml -> 'a) (g : xml -> 'b) : xml -> 'a * 'b = function - | Element ("pair", [], [x; y]) -> (f x, g y) - | _ -> raise Marshal_error - -let of_union (f : 'a -> xml) (g : 'b -> xml) : ('a,'b) CSig.union -> xml = function - | CSig.Inl x -> Element ("union", ["val","in_l"], [f x]) - | CSig.Inr x -> Element ("union", ["val","in_r"], [g x]) -let to_union (f : xml -> 'a) (g : xml -> 'b) : xml -> ('a,'b) CSig.union = function - | Element ("union", ["val","in_l"], [x]) -> CSig.Inl (f x) - | Element ("union", ["val","in_r"], [x]) -> CSig.Inr (g x) - | _ -> raise Marshal_error - -(** More elaborate types *) - -let of_edit_id i = Element ("edit_id",["val",string_of_int i],[]) -let to_edit_id = function - | Element ("edit_id",["val",i],[]) -> - let id = int_of_string i in - assert (id <= 0 ); - id - | _ -> raise Marshal_error - -let of_loc loc = - let start, stop = Loc.unloc loc in - Element ("loc",[("start",string_of_int start);("stop",string_of_int stop)],[]) -let to_loc xml = - match xml with - | Element ("loc", l,[]) -> - (try - let start = massoc "start" l in - let stop = massoc "stop" l in - Loc.make_loc (int_of_string start, int_of_string stop) - with Not_found | Invalid_argument _ -> raise Marshal_error) - | _ -> raise Marshal_error - -let of_xml x = Element ("xml", [], [x]) -let to_xml xml = match xml with -| Element ("xml", [], [x]) -> x -| _ -> raise Marshal_error diff --git a/lib/serialize.mli b/lib/serialize.mli deleted file mode 100644 index d7c14e7e73..0000000000 --- a/lib/serialize.mli +++ /dev/null @@ -1,39 +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 *) -(************************************************************************) - -open Xml_datatype - -exception Marshal_error - -val massoc: string -> (string * string) list -> string -val constructor: string -> string -> xml list -> xml -val do_match: string -> (string -> xml list -> 'b) -> xml -> 'b -val singleton: 'a list -> 'a -val raw_string: xml list -> string -val of_unit: unit -> xml -val to_unit: xml -> unit -val of_bool: bool -> xml -val to_bool: xml -> bool -val of_list: ('a -> xml) -> 'a list -> xml -val to_list: (xml -> 'a) -> xml -> 'a list -val of_option: ('a -> xml) -> 'a option -> xml -val to_option: (xml -> 'a) -> xml -> 'a option -val of_string: string -> xml -val to_string: xml -> string -val of_int: int -> xml -val to_int: xml -> int -val of_pair: ('a -> xml) -> ('b -> xml) -> 'a * 'b -> xml -val to_pair: (xml -> 'a) -> (xml -> 'b) -> xml -> 'a * 'b -val of_union: ('a -> xml) -> ('b -> xml) -> ('a, 'b) CSig.union -> xml -val to_union: (xml -> 'a) -> (xml -> 'b) -> xml -> ('a, 'b) CSig.union -val of_edit_id: int -> xml -val to_edit_id: xml -> int -val of_loc : Loc.t -> xml -val to_loc : xml -> Loc.t -val of_xml : xml -> xml -val to_xml : xml -> xml diff --git a/lib/stateid.ml b/lib/stateid.ml index 59cf206e2e..500581a39e 100644 --- a/lib/stateid.ml +++ b/lib/stateid.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Xml_datatype - type t = int let initial = 1 let dummy = 0 @@ -15,20 +13,14 @@ let fresh, in_range = let cur = ref initial in (fun () -> incr cur; !cur), (fun id -> id >= 0 && id <= !cur) let to_string = string_of_int -let of_int id = assert(in_range id); id +let of_int id = + (* Coqide too to parse ids too, but cannot check if they are valid. + * Hence we check for validity only if we are an ide slave. *) + if !Flags.ide_slave then assert (in_range id); + id let to_int id = id let newer_than id1 id2 = id1 > id2 -let of_xml = function - | Element ("state_id",["val",i],[]) -> - let id = int_of_string i in - (* Coqide too to parse ids too, but cannot check if they are valid. - * Hence we check for validity only if we are an ide slave. *) - if !Flags.ide_slave then assert(in_range id); - id - | _ -> raise (Invalid_argument "to_state_id") -let to_xml i = Element ("state_id",["val",string_of_int i],[]) - let state_id_info : (t * t) Exninfo.t = Exninfo.make () let add exn ?(valid = initial) id = Exninfo.add exn state_id_info (valid, id) @@ -37,7 +29,13 @@ let get exn = Exninfo.get exn state_id_info let equal = Int.equal let compare = Int.compare -module Set = Set.Make(struct type t = int let compare = compare end) +module Self = struct + type t = int + let compare = compare + let equal = equal +end + +module Set = Set.Make(Self) type ('a,'b) request = { exn_info : t * t; diff --git a/lib/stateid.mli b/lib/stateid.mli index 2c12c30c3c..cd8fddf0ce 100644 --- a/lib/stateid.mli +++ b/lib/stateid.mli @@ -6,26 +6,23 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Xml_datatype - type t val equal : t -> t -> bool val compare : t -> t -> int -module Set : Set.S with type elt = t +module Self : Map.OrderedType with type t = t +module Set : Set.S with type elt = t and type t = Set.Make(Self).t val initial : t val dummy : t val fresh : unit -> t val to_string : t -> string + val of_int : int -> t val to_int : t -> int -val newer_than : t -> t -> bool -(* XML marshalling *) -val to_xml : t -> xml -val of_xml : xml -> t +val newer_than : t -> t -> bool (* Attaches to an exception the concerned state id, plus an optional * state id that is a valid state id before the error. diff --git a/lib/system.ml b/lib/system.ml index e54109a2f3..8b53a11d67 100644 --- a/lib/system.ml +++ b/lib/system.ml @@ -12,65 +12,7 @@ open Pp open Errors open Util -(** Dealing with directories *) - -type unix_path = string (* path in unix-style, with '/' separator *) - -type file_kind = - | FileDir of unix_path * (* basename of path: *) string - | FileRegular of string (* basename of file *) - -(* Copy of Filename.concat but assuming paths to always be POSIX *) - -let (//) dirname filename = - let l = String.length dirname in - if l = 0 || dirname.[l-1] = '/' - then dirname ^ filename - else dirname ^ "/" ^ filename - -(* Excluding directories; We avoid directories starting with . as well - as CVS and _darcs and any subdirs given via -exclude-dir *) - -let skipped_dirnames = ref ["CVS"; "_darcs"] - -let exclude_directory f = skipped_dirnames := f :: !skipped_dirnames - -let ok_dirname f = - not (f = "") && f.[0] != '.' && - not (List.mem f !skipped_dirnames) (*&& - (match Unicode.ident_refutation f with None -> true | _ -> false)*) - -(* Check directory can be opened *) - -let exists_dir dir = - try Sys.is_directory dir with Sys_error _ -> false - -let check_unix_dir warn dir = - if (Sys.os_type = "Win32" || Sys.os_type = "Cygwin") && - (String.length dir > 2 && dir.[1] = ':' || - String.contains dir '\\' || - String.contains dir ';') - then warn ("assuming " ^ dir ^ - " to be a Unix path even if looking like a Win32 path.") - -let apply_subdir f path name = - (* we avoid all files and subdirs starting by '.' (e.g. .svn) *) - (* as well as skipped files like CVS, ... *) - if ok_dirname name then - let path = if path = "." then name else path//name in - match try (Unix.stat path).Unix.st_kind with Unix.Unix_error _ -> Unix.S_BLK with - | Unix.S_DIR -> f (FileDir (path,name)) - | Unix.S_REG -> f (FileRegular name) - | _ -> () - -let readdir dir = try Sys.readdir dir with any -> [||] - -let process_directory f path = - Array.iter (apply_subdir f path) (readdir path) - -let process_subdirectories f path = - let f = function FileDir (path,base) -> f path base | FileRegular _ -> () in - process_directory f path +include Minisys (** Returns the list of all recursive subdirectories of [root] in depth-first search, with sons ordered as on the file system; @@ -88,9 +30,9 @@ let all_subdirs ~unix_path:root = | _ -> () in process_directory f path in - check_unix_dir (fun s -> msg_warning (str s)) root; + check_unix_dir (fun s -> Feedback.msg_warning (str s)) root; if exists_dir root then traverse root [] - else msg_warning (str ("Cannot open " ^ root)); + else Feedback.msg_warning (str ("Cannot open " ^ root)); List.rev !l (* Caching directory contents for efficient syntactic equality of file @@ -149,7 +91,7 @@ let where_in_path ?(warn=true) path filename = | (lpe, f) :: l' -> let () = match l' with | _ :: _ when warn -> - msg_warning + Feedback.msg_warning (str filename ++ str " has been found in" ++ spc () ++ hov 0 (str "[ " ++ hv 0 (prlist_with_sep (fun () -> str " " ++ pr_semicolon()) @@ -205,7 +147,7 @@ let is_in_system_path filename = let lpath = CUnix.path_to_list (Sys.getenv "PATH") in is_in_path lpath filename with Not_found -> - msg_warning (str "system variable PATH not found"); + Feedback.msg_warning (str "system variable PATH not found"); false let open_trapping_failure name = @@ -216,7 +158,7 @@ let open_trapping_failure name = let try_remove filename = try Sys.remove filename with e when Errors.noncritical e -> - msg_warning + Feedback.msg_warning (str"Could not remove file " ++ str filename ++ str" which is corrupted!") let error_corrupted file s = @@ -345,13 +287,13 @@ let with_time time f x = let y = f x in let tend = get_time() in let msg2 = if time then "" else " (successful)" in - msg_info (str msg ++ fmt_time_difference tstart tend ++ str msg2); + Feedback.msg_info (str msg ++ fmt_time_difference tstart tend ++ str msg2); y with e -> let tend = get_time() in let msg = if time then "" else "Finished failing transaction in " in let msg2 = if time then "" else " (failure)" in - msg_info (str msg ++ fmt_time_difference tstart tend ++ str msg2); + Feedback.msg_info (str msg ++ fmt_time_difference tstart tend ++ str msg2); raise e let process_id () = diff --git a/lib/unicode.ml b/lib/unicode.ml index 938e8f1a99..dc852d9819 100644 --- a/lib/unicode.ml +++ b/lib/unicode.ml @@ -240,14 +240,94 @@ let is_basic_ascii s = !ok let ascii_of_ident s = - if is_basic_ascii s then s else - let i = ref 0 and out = ref "" in - begin try while true do + let len = String.length s in + let has_UU i = + i+2 < len && s.[i]='_' && s.[i+1]='U' && s.[i+2]='U' + in + let i = ref 0 in + while !i < len && Char.code s.[!i] < 128 && not (has_UU !i) do + incr i + done; + if !i = len then s else + let out = Buffer.create (2*len) in + Buffer.add_substring out s 0 !i; + while !i < len do let j, n = next_utf8 s !i in - out := - if n >= 128 - then Printf.sprintf "%s__U%04x_" !out n - else Printf.sprintf "%s%c" !out s.[!i]; - i := !i + j - done with End_of_input -> () end; - !out + if n >= 128 then + (Printf.bprintf out "_UU%04x_" n; i := !i + j) + else if has_UU !i then + (Buffer.add_string out "_UUU"; i := !i + 3) + else + (Buffer.add_char out s.[!i]; incr i) + done; + Buffer.contents out + +(* 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 + wrong in very rare cases. Such a wrong case corresponds to any + sequence of a character in range 192..253 immediately followed by a + character in range 128..191 (typical case in french is "déçu" which + is counted 3 instead of 4); then no real harm to use always + utf8_length even if using an iso8859_1 encoding *) + +(** FIXME: duplicate code with Pp *) + +let utf8_length s = + let len = String.length s + and cnt = ref 0 + and nc = ref 0 + and p = ref 0 in + while !p < len do + begin + match s.[!p] with + | '\000'..'\127' -> nc := 0 (* ascii char *) + | '\128'..'\191' -> nc := 0 (* cannot start with a continuation byte *) + | '\192'..'\223' -> nc := 1 (* expect 1 continuation byte *) + | '\224'..'\239' -> nc := 2 (* expect 2 continuation bytes *) + | '\240'..'\247' -> nc := 3 (* expect 3 continuation bytes *) + | '\248'..'\251' -> nc := 4 (* expect 4 continuation bytes *) + | '\252'..'\253' -> nc := 5 (* expect 5 continuation bytes *) + | '\254'..'\255' -> nc := 0 (* invalid byte *) + end ; + incr p ; + while !p < len && !nc > 0 do + match s.[!p] with + | '\128'..'\191' (* next continuation byte *) -> incr p ; decr nc + | _ (* not a continuation byte *) -> nc := 0 + done ; + incr cnt + done ; + !cnt + +(* Variant of String.sub for UTF8 character positions *) +let utf8_sub s start_u len_u = + let len_b = String.length s + and end_u = start_u + len_u + and cnt = ref 0 + and nc = ref 0 + and p = ref 0 in + let start_b = ref len_b in + while !p < len_b && !cnt < end_u do + if !cnt <= start_u then start_b := !p ; + begin + match s.[!p] with + | '\000'..'\127' -> nc := 0 (* ascii char *) + | '\128'..'\191' -> nc := 0 (* cannot start with a continuation byte *) + | '\192'..'\223' -> nc := 1 (* expect 1 continuation byte *) + | '\224'..'\239' -> nc := 2 (* expect 2 continuation bytes *) + | '\240'..'\247' -> nc := 3 (* expect 3 continuation bytes *) + | '\248'..'\251' -> nc := 4 (* expect 4 continuation bytes *) + | '\252'..'\253' -> nc := 5 (* expect 5 continuation bytes *) + | '\254'..'\255' -> nc := 0 (* invalid byte *) + end ; + incr p ; + while !p < len_b && !nc > 0 do + match s.[!p] with + | '\128'..'\191' (* next continuation byte *) -> incr p ; decr nc + | _ (* not a continuation byte *) -> nc := 0 + done ; + incr cnt + done ; + let end_b = !p in + String.sub s !start_b (end_b - !start_b) diff --git a/lib/unicode.mli b/lib/unicode.mli index b8a11e2945..1f8bd44eee 100644 --- a/lib/unicode.mli +++ b/lib/unicode.mli @@ -27,15 +27,22 @@ val ident_refutation : string -> (bool * string) option @raise Assert_failure if the input string is empty. *) val lowercase_first_char : string -> string -(** Return [true] if all UTF-8 characters in the input string are just plain ASCII characters. - Returns [false] otherwise. *) +(** Return [true] if all UTF-8 characters in the input string are just plain + ASCII characters. Returns [false] otherwise. *) val is_basic_ascii : string -> bool -(** [ascii_of_ident s] maps UTF-8 string to a string composed solely from ASCII characters. - Those UTF-8 characters which do not have their ASCII counterparts are - translated to ["__Uxxxx_"] where {i xxxx} are four hexadecimal digits. - @raise Unsupported if the input string contains unsupported UTF-8 characters. *) +(** [ascii_of_ident s] maps UTF-8 string to a string composed solely from ASCII + characters. The non-ASCII characters are translated to ["_UUxxxx_"] where + {i xxxx} is the Unicode index of the character in hexadecimal (from four + to six hex digits). To avoid potential name clashes, any preexisting + substring ["_UU"] is turned into ["_UUU"]. *) val ascii_of_ident : string -> string (** Validate an UTF-8 string *) val is_utf8 : string -> bool + +(** Return the length of a valid UTF-8 string. *) +val utf8_length : string -> int + +(** Variant of {!String.sub} for UTF-8 strings. *) +val utf8_sub : string -> int -> int -> string diff --git a/lib/xml_lexer.mli b/lib/xml_lexer.mli deleted file mode 100644 index e61cb055f7..0000000000 --- a/lib/xml_lexer.mli +++ /dev/null @@ -1,44 +0,0 @@ -(* - * Xml Light, an small Xml parser/printer with DTD support. - * Copyright (C) 2003 Nicolas Cannasse (ncannasse@motion-twin.com) - * - * This library is free software; you can redistribute it and/or - * modify it under the terms of the GNU Lesser General Public - * License as published by the Free Software Foundation; either - * version 2.1 of the License, or (at your option) any later version. - * - * This library is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU - * Lesser General Public License for more details. - * - * You should have received a copy of the GNU Lesser General Public - * License along with this library; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA - *) - -type error = - | EUnterminatedComment - | EUnterminatedString - | EIdentExpected - | ECloseExpected - | ENodeExpected - | EAttributeNameExpected - | EAttributeValueExpected - | EUnterminatedEntity - -exception Error of error - -type token = - | Tag of string * (string * string) list * bool - | PCData of string - | Endtag of string - | Eof - -type pos = int * int * int * int - -val init : Lexing.lexbuf -> unit -val close : unit -> unit -val token : Lexing.lexbuf -> token -val pos : Lexing.lexbuf -> pos -val restore : pos -> unit diff --git a/lib/xml_lexer.mll b/lib/xml_lexer.mll deleted file mode 100644 index 290f2c89ab..0000000000 --- a/lib/xml_lexer.mll +++ /dev/null @@ -1,317 +0,0 @@ -{(* - * Xml Light, an small Xml parser/printer with DTD support. - * Copyright (C) 2003 Nicolas Cannasse (ncannasse@motion-twin.com) - * - * This library is free software; you can redistribute it and/or - * modify it under the terms of the GNU Lesser General Public - * License as published by the Free Software Foundation; either - * version 2.1 of the License, or (at your option) any later version. - * - * This library is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU - * Lesser General Public License for more details. - * - * You should have received a copy of the GNU Lesser General Public - * License along with this library; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA - *) - -open Lexing - -type error = - | EUnterminatedComment - | EUnterminatedString - | EIdentExpected - | ECloseExpected - | ENodeExpected - | EAttributeNameExpected - | EAttributeValueExpected - | EUnterminatedEntity - -exception Error of error - -type pos = int * int * int * int - -type token = - | Tag of string * (string * string) list * bool - | PCData of string - | Endtag of string - | Eof - -let last_pos = ref 0 -and current_line = ref 0 -and current_line_start = ref 0 - -let tmp = Buffer.create 200 - -let idents = Hashtbl.create 0 - -let _ = begin - Hashtbl.add idents "nbsp;" " "; - Hashtbl.add idents "gt;" ">"; - Hashtbl.add idents "lt;" "<"; - Hashtbl.add idents "amp;" "&"; - Hashtbl.add idents "apos;" "'"; - Hashtbl.add idents "quot;" "\""; -end - -let init lexbuf = - current_line := 1; - current_line_start := lexeme_start lexbuf; - last_pos := !current_line_start - -let close lexbuf = - Buffer.reset tmp - -let pos lexbuf = - !current_line , !current_line_start , - !last_pos , - lexeme_start lexbuf - -let restore (cl,cls,lp,_) = - current_line := cl; - current_line_start := cls; - last_pos := lp - -let newline lexbuf = - incr current_line; - last_pos := lexeme_end lexbuf; - current_line_start := !last_pos - -let error lexbuf e = - last_pos := lexeme_start lexbuf; - raise (Error e) - -} - -let newline = ['\n'] -let break = ['\r'] -let space = [' ' '\t'] -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' '<' '>' '&'] - -rule token = parse - | newline | (newline break) | break - { - newline lexbuf; - PCData "\n" - } - | "<!--" - { - last_pos := lexeme_start lexbuf; - comment lexbuf; - token lexbuf - } - | "<?" - { - last_pos := lexeme_start lexbuf; - header lexbuf; - token lexbuf; - } - | '<' space* '/' space* - { - last_pos := lexeme_start lexbuf; - let tag = ident_name lexbuf in - ignore_spaces lexbuf; - close_tag lexbuf; - Endtag tag - } - | '<' space* - { - last_pos := lexeme_start lexbuf; - let tag = ident_name lexbuf in - ignore_spaces lexbuf; - let attribs, closed = attributes lexbuf in - Tag(tag, attribs, closed) - } - | "&#" - { - last_pos := lexeme_start lexbuf; - Buffer.reset tmp; - Buffer.add_string tmp (lexeme lexbuf); - PCData (pcdata lexbuf) - } - | '&' - { - last_pos := lexeme_start lexbuf; - Buffer.reset tmp; - Buffer.add_string tmp (entity lexbuf); - PCData (pcdata lexbuf) - } - | pcchar+ - { - last_pos := lexeme_start lexbuf; - Buffer.reset tmp; - Buffer.add_string tmp (lexeme lexbuf); - PCData (pcdata lexbuf) - } - | eof { Eof } - | _ - { error lexbuf ENodeExpected } - -and ignore_spaces = parse - | newline | (newline break) | break - { - newline lexbuf; - ignore_spaces lexbuf - } - | space + - { ignore_spaces lexbuf } - | "" - { () } - -and comment = parse - | newline | (newline break) | break - { - newline lexbuf; - comment lexbuf - } - | "-->" - { () } - | eof - { raise (Error EUnterminatedComment) } - | _ - { comment lexbuf } - -and header = parse - | newline | (newline break) | break - { - newline lexbuf; - header lexbuf - } - | "?>" - { () } - | eof - { error lexbuf ECloseExpected } - | _ - { header lexbuf } - -and pcdata = parse - | newline | (newline break) | break - { - Buffer.add_char tmp '\n'; - newline lexbuf; - pcdata lexbuf - } - | pcchar+ - { - Buffer.add_string tmp (lexeme lexbuf); - pcdata lexbuf - } - | "&#" - { - Buffer.add_string tmp (lexeme lexbuf); - pcdata lexbuf; - } - | '&' - { - Buffer.add_string tmp (entity lexbuf); - pcdata lexbuf - } - | "" - { Buffer.contents tmp } - -and entity = parse - | entitychar+ ';' - { - let ident = lexeme lexbuf in - try - Hashtbl.find idents (String.lowercase ident) - with - Not_found -> "&" ^ ident - } - | _ | eof - { raise (Error EUnterminatedEntity) } - -and ident_name = parse - | ident - { lexeme lexbuf } - | _ | eof - { error lexbuf EIdentExpected } - -and close_tag = parse - | '>' - { () } - | _ | eof - { error lexbuf ECloseExpected } - -and attributes = parse - | '>' - { [], false } - | "/>" - { [], true } - | "" (* do not read a char ! *) - { - let key = attribute lexbuf in - let data = attribute_data lexbuf in - ignore_spaces lexbuf; - let others, closed = attributes lexbuf in - (key, data) :: others, closed - } - -and attribute = parse - | ident - { lexeme lexbuf } - | _ | eof - { error lexbuf EAttributeNameExpected } - -and attribute_data = parse - | space* '=' space* '"' - { - Buffer.reset tmp; - last_pos := lexeme_end lexbuf; - dq_string lexbuf - } - | space* '=' space* '\'' - { - Buffer.reset tmp; - last_pos := lexeme_end lexbuf; - q_string lexbuf - } - | _ | eof - { error lexbuf EAttributeValueExpected } - -and dq_string = parse - | '"' - { Buffer.contents tmp } - | '\\' [ '"' '\\' ] - { - Buffer.add_char tmp (lexeme_char lexbuf 1); - dq_string lexbuf - } - | '&' - { - Buffer.add_string tmp (entity lexbuf); - dq_string lexbuf - } - | eof - { raise (Error EUnterminatedString) } - | _ - { - Buffer.add_char tmp (lexeme_char lexbuf 0); - dq_string lexbuf - } - -and q_string = parse - | '\'' - { Buffer.contents tmp } - | '\\' [ '\'' '\\' ] - { - Buffer.add_char tmp (lexeme_char lexbuf 1); - q_string lexbuf - } - | '&' - { - Buffer.add_string tmp (entity lexbuf); - q_string lexbuf - } - | eof - { raise (Error EUnterminatedString) } - | _ - { - Buffer.add_char tmp (lexeme_char lexbuf 0); - q_string lexbuf - } diff --git a/lib/xml_parser.ml b/lib/xml_parser.ml deleted file mode 100644 index 8db3f9e8ba..0000000000 --- a/lib/xml_parser.ml +++ /dev/null @@ -1,232 +0,0 @@ -(* - * Xml Light, an small Xml parser/printer with DTD support. - * Copyright (C) 2003 Nicolas Cannasse (ncannasse@motion-twin.com) - * Copyright (C) 2003 Jacques Garrigue - * - * This library is free software; you can redistribute it and/or - * modify it under the terms of the GNU Lesser General Public - * License as published by the Free Software Foundation; either - * version 2.1 of the License, or (at your option) any later version. - * - * This library is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU - * Lesser General Public License for more details. - * - * You should have received a copy of the GNU Lesser General Public - * License along with this library; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA - *) - -open Printf -open Xml_datatype - -type xml = Xml_datatype.xml - -type error_pos = { - eline : int; - eline_start : int; - emin : int; - emax : int; -} - -type error_msg = - | UnterminatedComment - | UnterminatedString - | UnterminatedEntity - | IdentExpected - | CloseExpected - | NodeExpected - | AttributeNameExpected - | AttributeValueExpected - | EndOfTagExpected of string - | EOFExpected - | Empty - -type error = error_msg * error_pos - -exception Error of error - -exception File_not_found of string - -type t = { - mutable check_eof : bool; - mutable concat_pcdata : bool; - source : Lexing.lexbuf; - stack : Xml_lexer.token Stack.t; -} - -type source = - | SChannel of in_channel - | SString of string - | SLexbuf of Lexing.lexbuf - -exception Internal_error of error_msg -exception NoMoreData - -let xml_error = ref (fun _ -> assert false) -let file_not_found = ref (fun _ -> assert false) - -let is_blank s = - let len = String.length s in - let break = ref true in - let i = ref 0 in - while !break && !i < len do - let c = s.[!i] in - (* no '\r' because we replaced them in the lexer *) - if c = ' ' || c = '\n' || c = '\t' then incr i - else break := false - done; - !i = len - -let _raises e f = - xml_error := e; - file_not_found := f - -let make source = - let source = match source with - | SChannel chan -> Lexing.from_channel chan - | SString s -> Lexing.from_string s - | SLexbuf lexbuf -> lexbuf - in - let () = Xml_lexer.init source in - { - check_eof = false; - concat_pcdata = true; - source = source; - stack = Stack.create (); - } - -let check_eof p v = p.check_eof <- v - -let pop s = - try - Stack.pop s.stack - with - Stack.Empty -> - Xml_lexer.token s.source - -let push t s = - Stack.push t s.stack - -let canonicalize l = - let has_elt = List.exists (function Element _ -> true | _ -> false) l in - if has_elt then List.filter (function PCData s -> not (is_blank s) | _ -> true) l - else l - -let rec read_xml do_not_canonicalize s = - let rec read_node s = - match pop s with - | Xml_lexer.PCData s -> PCData s - | Xml_lexer.Tag (tag, attr, true) -> Element (tag, attr, []) - | Xml_lexer.Tag (tag, attr, false) -> - let elements = read_elems tag s in - let elements = - if do_not_canonicalize then elements else canonicalize elements - in - Element (tag, attr, elements) - | t -> - push t s; - raise NoMoreData - - and read_elems tag s = - let elems = ref [] in - (try - while true do - let node = read_node s in - match node, !elems with - | PCData c , (PCData c2) :: q -> - elems := PCData (c2 ^ c) :: q - | _, l -> - elems := node :: l - done - with - NoMoreData -> ()); - match pop s with - | Xml_lexer.Endtag s when s = tag -> List.rev !elems - | t -> raise (Internal_error (EndOfTagExpected tag)) - in - match read_node s with - | (Element _) as node -> - node - | PCData c -> - if is_blank c then - read_xml do_not_canonicalize s - else - raise (Xml_lexer.Error Xml_lexer.ENodeExpected) - -let convert = function - | Xml_lexer.EUnterminatedComment -> UnterminatedComment - | Xml_lexer.EUnterminatedString -> UnterminatedString - | Xml_lexer.EIdentExpected -> IdentExpected - | Xml_lexer.ECloseExpected -> CloseExpected - | Xml_lexer.ENodeExpected -> NodeExpected - | Xml_lexer.EAttributeNameExpected -> AttributeNameExpected - | Xml_lexer.EAttributeValueExpected -> AttributeValueExpected - | Xml_lexer.EUnterminatedEntity -> UnterminatedEntity - -let error_of_exn xparser = function - | NoMoreData when pop xparser = Xml_lexer.Eof -> Empty - | NoMoreData -> NodeExpected - | Internal_error e -> e - | Xml_lexer.Error e -> convert e - | e -> - (*let e = Errors.push e in: We do not record backtrace here. *) - raise e - -let do_parse do_not_canonicalize xparser = - try - Xml_lexer.init xparser.source; - let x = read_xml do_not_canonicalize xparser in - if xparser.check_eof && pop xparser <> Xml_lexer.Eof then raise (Internal_error EOFExpected); - Xml_lexer.close (); - x - with any -> - Xml_lexer.close (); - raise (!xml_error (error_of_exn xparser any) xparser.source) - -let parse ?(do_not_canonicalize=false) p = - do_parse do_not_canonicalize p - -let error_msg = function - | UnterminatedComment -> "Unterminated comment" - | UnterminatedString -> "Unterminated string" - | UnterminatedEntity -> "Unterminated entity" - | IdentExpected -> "Ident expected" - | CloseExpected -> "Element close expected" - | NodeExpected -> "Xml node expected" - | AttributeNameExpected -> "Attribute name expected" - | AttributeValueExpected -> "Attribute value expected" - | EndOfTagExpected tag -> sprintf "End of tag expected : '%s'" tag - | EOFExpected -> "End of file expected" - | Empty -> "Empty" - -let error (msg,pos) = - if pos.emin = pos.emax then - sprintf "%s line %d character %d" (error_msg msg) pos.eline - (pos.emin - pos.eline_start) - else - sprintf "%s line %d characters %d-%d" (error_msg msg) pos.eline - (pos.emin - pos.eline_start) (pos.emax - pos.eline_start) - -let line e = e.eline - -let range e = - e.emin - e.eline_start , e.emax - e.eline_start - -let abs_range e = - e.emin , e.emax - -let pos source = - let line, lstart, min, max = Xml_lexer.pos source in - { - eline = line; - eline_start = lstart; - emin = min; - emax = max; - } - -let () = _raises (fun x p -> - (* local cast : Xml.error_msg -> error_msg *) - Error (x, pos p)) - (fun f -> File_not_found f) diff --git a/lib/xml_parser.mli b/lib/xml_parser.mli deleted file mode 100644 index ac2eab352f..0000000000 --- a/lib/xml_parser.mli +++ /dev/null @@ -1,106 +0,0 @@ -(* - * Xml Light, an small Xml parser/printer with DTD support. - * Copyright (C) 2003 Nicolas Cannasse (ncannasse@motion-twin.com) - * - * This library is free software; you can redistribute it and/or - * modify it under the terms of the GNU Lesser General Public - * License as published by the Free Software Foundation; either - * version 2.1 of the License, or (at your option) any later version. - * - * This library is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU - * Lesser General Public License for more details. - * - * You should have received a copy of the GNU Lesser General Public - * License along with this library; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA - *) - -(** Xml Light Parser - - While basic parsing functions can be used in the {!Xml} module, this module - is providing a way to create, configure and run an Xml parser. - -*) - - -(** An Xml node is either - [Element (tag-name, attributes, children)] or [PCData text] *) -type xml = Xml_datatype.xml - -(** Abstract type for an Xml parser. *) -type t - -(** {6:exc Xml Exceptions} *) - -(** 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 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.} - } - *) - -type error_pos - -type error_msg = - | UnterminatedComment - | UnterminatedString - | UnterminatedEntity - | IdentExpected - | CloseExpected - | NodeExpected - | AttributeNameExpected - | AttributeValueExpected - | EndOfTagExpected of string - | EOFExpected - | Empty - -type error = error_msg * error_pos - -exception Error of error - -exception File_not_found of string - -(** Get a full error message from an Xml error. *) -val error : error -> string - -(** Get the Xml error message as a string. *) -val error_msg : error_msg -> string - -(** Get the line the error occurred at. *) -val line : error_pos -> int - -(** 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 occurred at. *) -val abs_range : error_pos -> int * int - -val pos : Lexing.lexbuf -> error_pos - -(** Several kind of resources can contain Xml documents. *) -type source = -| SChannel of in_channel -| SString of string -| SLexbuf of Lexing.lexbuf - -(** This function returns a new parser with default options. *) -val make : source -> t - -(** When a Xml document is parsed, the parser may check that the end of the - document is reached, so for example parsing ["<A/><B/>"] will fail instead - of returning only the A element. You can turn on this check by setting - [check_eof] to [true] {i (by default, check_eof is false, unlike - in the original Xmllight)}. *) -val check_eof : t -> bool -> unit - -(** 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 - is, without trying to remove blank PCDATA elements. *) -val parse : ?do_not_canonicalize:bool -> t -> xml diff --git a/lib/xml_printer.ml b/lib/xml_printer.ml deleted file mode 100644 index e7e4d0cebc..0000000000 --- a/lib/xml_printer.ml +++ /dev/null @@ -1,145 +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 *) -(************************************************************************) - -open Xml_datatype - -type xml = Xml_datatype.xml - -type target = TChannel of out_channel | TBuffer of Buffer.t - -type t = target - -let make x = x - -let buffer_pcdata tmp text = - let output = Buffer.add_string tmp in - let output' = Buffer.add_char tmp in - let l = String.length text in - for p = 0 to l-1 do - match text.[p] with - | ' ' -> output " "; - | '>' -> output ">" - | '<' -> output "<" - | '&' -> - if p < l - 1 && text.[p + 1] = '#' then - output' '&' - else - output "&" - | '\'' -> output "'" - | '"' -> output """ - | c -> output' c - done - -let buffer_attr tmp (n,v) = - let output = Buffer.add_string tmp in - let output' = Buffer.add_char tmp in - output' ' '; - output n; - output "=\""; - let l = String.length v in - for p = 0 to l - 1 do - match v.[p] with - | '\\' -> output "\\\\" - | '"' -> output "\\\"" - | '<' -> output "<" - | '&' -> output "&" - | c -> output' c - done; - output' '"' - -let to_buffer tmp x = - let pcdata = ref false in - let output = Buffer.add_string tmp in - let output' = Buffer.add_char tmp in - let rec loop = function - | Element (tag,alist,[]) -> - output' '<'; - output tag; - List.iter (buffer_attr tmp) alist; - output "/>"; - pcdata := false; - | Element (tag,alist,l) -> - output' '<'; - output tag; - List.iter (buffer_attr tmp) alist; - output' '>'; - pcdata := false; - List.iter loop l; - output "</"; - output tag; - output' '>'; - pcdata := false; - | PCData text -> - if !pcdata then output' ' '; - buffer_pcdata tmp text; - pcdata := true; - in - loop x - -let pcdata_to_string s = - let b = Buffer.create 13 in - buffer_pcdata b s; - Buffer.contents b - -let to_string x = - let b = Buffer.create 200 in - to_buffer b x; - Buffer.contents b - -let to_string_fmt x = - let tmp = Buffer.create 200 in - let output = Buffer.add_string tmp in - let output' = Buffer.add_char tmp in - let rec loop ?(newl=false) tab = function - | Element (tag, alist, []) -> - output tab; - output' '<'; - output tag; - List.iter (buffer_attr tmp) alist; - output "/>"; - if newl then output' '\n'; - | Element (tag, alist, [PCData text]) -> - output tab; - output' '<'; - output tag; - List.iter (buffer_attr tmp) alist; - output ">"; - buffer_pcdata tmp text; - output "</"; - output tag; - output' '>'; - if newl then output' '\n'; - | Element (tag, alist, l) -> - output tab; - output' '<'; - output tag; - List.iter (buffer_attr tmp) alist; - output ">\n"; - List.iter (loop ~newl:true (tab^" ")) l; - output tab; - output "</"; - output tag; - output' '>'; - if newl then output' '\n'; - | PCData text -> - buffer_pcdata tmp text; - if newl then output' '\n'; - in - loop "" x; - Buffer.contents tmp - -let print t xml = - let tmp, flush = match t with - | TChannel oc -> - let b = Buffer.create 200 in - b, (fun () -> Buffer.output_buffer oc b; flush oc) - | TBuffer b -> - b, (fun () -> ()) - in - to_buffer tmp xml; - flush () diff --git a/lib/xml_printer.mli b/lib/xml_printer.mli deleted file mode 100644 index f24f51fff5..0000000000 --- a/lib/xml_printer.mli +++ /dev/null @@ -1,29 +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 *) -(************************************************************************) - -type xml = Xml_datatype.xml - -type t -type target = TChannel of out_channel | TBuffer of Buffer.t - -val make : target -> t - -(** Print the xml data structure to a source into a compact xml string (without - any user-readable formating ). *) -val print : t -> xml -> unit - -(** Print the xml data structure into a compact xml string (without - any user-readable formating ). *) -val to_string : xml -> string - -(** Print the xml data structure into an user-readable string with - tabs and lines break between different nodes. *) -val to_string_fmt : xml -> string - -(** Print PCDATA as a string by escaping XML entities. *) -val pcdata_to_string : string -> string |