diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/cErrors.ml | 2 | ||||
| -rw-r--r-- | lib/control.ml | 6 | ||||
| -rw-r--r-- | lib/coqProject_file.ml | 10 | ||||
| -rw-r--r-- | lib/coqProject_file.mli | 1 | ||||
| -rw-r--r-- | lib/dune | 2 | ||||
| -rw-r--r-- | lib/loc.ml | 15 | ||||
| -rw-r--r-- | lib/loc.mli | 2 | ||||
| -rw-r--r-- | lib/system.mli | 1 |
8 files changed, 24 insertions, 15 deletions
diff --git a/lib/cErrors.ml b/lib/cErrors.ml index 811fcf4063..79f0a806a7 100644 --- a/lib/cErrors.ml +++ b/lib/cErrors.ml @@ -112,7 +112,7 @@ let iprint_no_report (e, info) = let _ = register_handler begin function | UserError(s, pps) -> - hov 0 (where s ++ pps) + where s ++ pps | _ -> raise Unhandled end diff --git a/lib/control.ml b/lib/control.ml index 3fbeb168c4..e09068740d 100644 --- a/lib/control.ml +++ b/lib/control.ml @@ -62,8 +62,8 @@ let windows_timeout n f x e = let res = f x in let () = killed := true in let cur = Unix.gettimeofday () in - (** The thread did not interrupt, but the computation took longer than - expected. *) + (* The thread did not interrupt, but the computation took longer than + expected. *) let () = if float_of_int n <= cur -. init then begin exited := true; raise Sys.Break @@ -71,7 +71,7 @@ let windows_timeout n f x e = res with | Sys.Break -> - (** Just in case, it could be a regular Ctrl+C *) + (* Just in case, it could be a regular Ctrl+C *) if not !exited then begin killed := true; raise Sys.Break end else raise e | e -> diff --git a/lib/coqProject_file.ml b/lib/coqProject_file.ml index 868042303d..d908baa1e8 100644 --- a/lib/coqProject_file.ml +++ b/lib/coqProject_file.ml @@ -24,7 +24,6 @@ type project = { v_files : string sourced list; mli_files : string sourced list; - ml4_files : string sourced list; mlg_files : string sourced list; ml_files : string sourced list; mllib_files : string sourced list; @@ -62,7 +61,6 @@ let mk_project project_file makefile install_kind use_ocamlopt = { v_files = []; mli_files = []; - ml4_files = []; mlg_files = []; ml_files = []; mllib_files = []; @@ -220,7 +218,9 @@ let process_cmd_line ~warning_fn orig_dir proj args = | ".v" -> { proj with v_files = proj.v_files @ [sourced f] } | ".ml" -> { proj with ml_files = proj.ml_files @ [sourced f] } - | ".ml4" -> { proj with ml4_files = proj.ml4_files @ [sourced f] } + | ".ml4" -> + let msg = Printf.sprintf "camlp5 macro files not supported anymore, please port %s to coqpp" f in + raise (Parsing_error msg) | ".mlg" -> { proj with mlg_files = proj.mlg_files @ [sourced f] } | ".mli" -> { proj with mli_files = proj.mli_files @ [sourced f] } | ".mllib" -> { proj with mllib_files = proj.mllib_files @ [sourced f] } @@ -248,9 +248,9 @@ let rec find_project_file ~from ~projfile_name = else find_project_file ~from:newdir ~projfile_name ;; -let all_files { v_files; ml_files; mli_files; ml4_files; mlg_files; +let all_files { v_files; ml_files; mli_files; mlg_files; mllib_files; mlpack_files } = - v_files @ mli_files @ ml4_files @ mlg_files @ ml_files @ mllib_files @ mlpack_files + v_files @ mli_files @ mlg_files @ ml_files @ mllib_files @ mlpack_files let map_sourced_list f l = List.map (fun x -> f x.thing) l ;; diff --git a/lib/coqProject_file.mli b/lib/coqProject_file.mli index 20b276ce8c..39c5d019d0 100644 --- a/lib/coqProject_file.mli +++ b/lib/coqProject_file.mli @@ -22,7 +22,6 @@ type project = { v_files : string sourced list; mli_files : string sourced list; - ml4_files : string sourced list; mlg_files : string sourced list; ml_files : string sourced list; mllib_files : string sourced list; @@ -4,4 +4,4 @@ (public_name coq.lib) (wrapped false) (modules_without_implementation xml_datatype) - (libraries threads coq.clib coq.config)) + (libraries dynlink coq.clib coq.config)) diff --git a/lib/loc.ml b/lib/loc.ml index 1a09091bff..c08648911b 100644 --- a/lib/loc.ml +++ b/lib/loc.ml @@ -22,15 +22,19 @@ type t = { bol_pos_last : int; (** position of the beginning of end line *) bp : int; (** start position *) ep : int; (** end position *) + comm : string; (** start comment *) + ecomm : string (** end comment *) } let create fname line_nb bol_pos bp ep = { fname = fname; line_nb = line_nb; bol_pos = bol_pos; - line_nb_last = line_nb; bol_pos_last = bol_pos; bp = bp; ep = ep; } + line_nb_last = line_nb; bol_pos_last = bol_pos; bp = bp; ep = ep; + comm = ""; ecomm = "" } let make_loc (bp, ep) = { fname = ToplevelInput; line_nb = -1; bol_pos = 0; line_nb_last = -1; bol_pos_last = 0; - bp = bp; ep = ep; } + bp = bp; ep = ep; + comm = ""; ecomm = "" } let mergeable loc1 loc2 = loc1.fname = loc2.fname @@ -45,7 +49,8 @@ let merge loc1 loc2 = bol_pos = loc1.bol_pos; line_nb_last = loc2.line_nb_last; bol_pos_last = loc2.bol_pos_last; - bp = loc1.bp; ep = loc2.ep; } + bp = loc1.bp; ep = loc2.ep; + comm = loc1.comm; ecomm = loc2.comm } else loc1 else if loc2.ep < loc1.ep then { fname = loc2.fname; @@ -53,7 +58,9 @@ let merge loc1 loc2 = bol_pos = loc2.bol_pos; line_nb_last = loc1.line_nb_last; bol_pos_last = loc1.bol_pos_last; - bp = loc2.bp; ep = loc1.ep; } + bp = loc2.bp; ep = loc1.ep; + comm = loc2.comm; ecomm = loc1.comm + } else loc2 let merge_opt l1 l2 = match l1, l2 with diff --git a/lib/loc.mli b/lib/loc.mli index 23df1ebd9a..c46311b639 100644 --- a/lib/loc.mli +++ b/lib/loc.mli @@ -22,6 +22,8 @@ type t = { bol_pos_last : int; (** position of the beginning of end line *) bp : int; (** start position *) ep : int; (** end position *) + comm : string; (** start comment *) + ecomm : string (** end comment *) } (** {5 Location manipulation} *) diff --git a/lib/system.mli b/lib/system.mli index f13fd30923..a3b79ee528 100644 --- a/lib/system.mli +++ b/lib/system.mli @@ -102,6 +102,7 @@ type time val get_time : unit -> time val time_difference : time -> time -> float (** in seconds *) + val fmt_time_difference : time -> time -> Pp.t val with_time : batch:bool -> ('a -> 'b) -> 'a -> 'b |