aboutsummaryrefslogtreecommitdiff
path: root/lib
AgeCommit message (Collapse)Author
2017-10-06Merge PR #1119: Fixing bug BZ#5769 (generating a name "_" out of a type ↵Maxime Dénès
"_something")
2017-10-06Merge PR #1125: [pp] Minor optimization in `Pp.t` construction and gluing.Maxime Dénès
2017-10-05Merge PR #1069: Improve support for -w optionsMaxime Dénès
2017-10-05Merge PR #1041: Miscellaneous fixes about UTF-8 (including a fix to BZ#5715 ↵Maxime Dénès
to escape non-UTF-8 file names)
2017-10-05Merge PR #1059: coq_makefile: make sure compile flags for Coq and ↵Maxime Dénès
coq_makefile are in sync (supersed #1039)…
2017-10-05[pp] Minor optimization in `Pp.t` construction and gluing.Emilio Jesus Gallego Arias
The typical Coq `Pp.t` document contains a lot of "gluing" which produces efficient structures but it is quite painful in serialization. We optimize a common document building case so we don't create as much glue nodes as with the "naive" strategy, and without incurring in the large performance cost full flattening would produce. This is a temporal fixup, see #505 for more context on the discussion and medium-term plans.
2017-10-05Fixing BZ#5769 (variable of type "_something" was named after invalid "_").Hugo Herbelin
2017-10-05Distinguishing pseudo-letters out of the set of unicode letters.Hugo Herbelin
This includes _ and insecable space which can be used in idents and this allows more precise heuristics.
2017-10-05Fixing typos in comments of unicode.ml.Hugo Herbelin
2017-10-03Merge PR #1100: Avoid looping when searching for CoqProject.Maxime Dénès
2017-10-03Merge PR #1015: Adding a function to be typically used to pass values from ↵Maxime Dénès
an OCaml "when" clause to the r.h.s of the matching clause
2017-09-27Avoid looping when searching for CoqProject.Maxime Dénès
This could happen with paths on Windows, or even relative paths on all OSs. Fixes #5730: CoqIDE becomes unresponsive on file open.
2017-09-21Improve support for "-w none" compatibility option.Guillaume Melquiond
If coqtop was started with "-w none" yet the script used "Set Warnings Append", then all the warnings were turned back to their default value. This commit turns "none" (whatever its sign) into "-all" whenever some warning status is modified afterward, in order to prevent the issue.
2017-09-19coq_makefile: make sure compile flags for Coq and coq_makefile are in syncEmilio Jesus Gallego Arias
E.g. -safe-string is set by configure.ml and made available to both make (via config/Makefile) and coq_makefile (via config/coq_config.ml -> lib/envars.ml -> CoqMakefile.in).
2017-09-18Reporting locations in error messages about notation formats.Hugo Herbelin
2017-09-14Using an algebraic type for distinguishing toplevel input from location in file.Hugo Herbelin
2017-09-13A possible fix for BZ#5715 (escape non-utf8 win32 file names).Hugo Herbelin
On Win32, Sys.readdir translates the file names to the charset of the local "code page", which may be not compatible with utf8. Warnings referring to these names can be generated. These warnings may be sent to CoqIDE. To ensure a utf8 compliant communication, we escape non-utf8 file names under win32. In the CoqIDE/Coq communication, Glib.IO.read_chars expects an utf8-encoding and raises otherwise a Glib.Error "Invalid byte sequence in conversion input". This fixes bug #5715 (Hangul characters not recognized in file names) but this does not solve the case of an operating system mounting a file system with a different coding convention than the default one, i.e. unicode using "Normalization Form Canonical Decomposition" in UTF-8 for HFS+ on MacOS X, no encoding for ext3/ext4 on Linux, (non-normalized?) UTF-16 for NTFS on Windows.
2017-09-13Complying more precisely to unicode standard.Hugo Herbelin
In particular, checking that it is at most 4 bytes.
2017-09-13Adding a function to escape strings with non-utf8 characters.Hugo Herbelin
2017-09-12Adding function to be typically used to pass values from an OCaml "when" clause.Hugo Herbelin
2017-09-11Merge PR #987: In Array.smartmap, read and write from same arrayMaxime Dénès
2017-09-04Making detyping potentially lazy.Pierre-Marie Pédrot
The internal detype function takes an additional arguments dictating whether it should be eager or lazy. We introduce a new type of delayed `DAst.t` AST nodes and use it for `glob_constr`. Such type, instead of only containing a value, it can contain a lazy computation too. We use a GADT to discriminate between both uses statically, so that no delayed terms ever happen to be marshalled (which would raise anomalies). We also fix a regression in the test-suite: Mixing laziness and effects is a well-known hell. Here, an exception that was raised for mere control purpose was delayed and raised at a later time as an anomaly. We make the offending function eager.
2017-08-31Merge PR #980: Adding combinators + a canonical renaming in List, Option, NameMaxime Dénès
2017-08-31Merge PR #989: Prevent overallocation in Array.map_to_list and remove custom ↵Maxime Dénès
implementation from Detyping.
2017-08-29Merge PR #773: [flags] Remove XML output flag.Maxime Dénès
2017-08-29Canonically renaming fold_map into fold_left_map in library Option.Hugo Herbelin
Also adding fold_right_map by consistency.
2017-08-29Canonically renaming fold_map into fold_left_map in library Array.Hugo Herbelin
Also renaming fold_map' into fold_right_map, and fold_map2' into fold_right2_map.
2017-08-29Adding combinators + a canonical renaming in cList.ml.Hugo Herbelin
- Adding fold_left2_map/fold_right2_map. - Canonically renaming fold_map/fold_map' into fold_left_map/fold_right_map.
2017-08-22also in Fun1.smartmap, read, write from same arrayPaul Steckler
2017-08-22Prevent overallocation in Array.map_to_list and remove custom implementation ↵Guillaume Melquiond
from Detyping.
2017-08-21read, write from same arrayPaul Steckler
2017-08-17Merge PR #490: A possible fix for #5391 (command line tools do not accept ↵Maxime Dénès
trailing / and \ on windows)
2017-08-16Merge PR #864: Some cleanups after cumulativity for inductive typesMaxime Dénès
2017-08-15Removing trailing "/" and "\" in directory names only on win32.Hugo Herbelin
This refines e234f3ef. By the way, note that e234f3ef fixed #5391 (command line tools do not accept trailing "/" - or "\" - in windows).
2017-08-01[flags] Remove XML output flag.Emilio Jesus Gallego Arias
This is a second try at removing the hooks for the legacy xml export system which can't currently be tested. It is also not included in the API, so it should either be included in it or this PR be applied.
2017-07-31Change the option for cumulativityAmin Timany
2017-07-31Merge PR #761: deprecate Pp.std_ppcmds type and promote Pp.t insteadMaxime Dénès
2017-07-27deprecate Pp.std_ppcmds type aliasMatej Košík
2017-07-26Merge PR #902: Only perform profile initialization and printing when the ↵Maxime Dénès
flag is set.
2017-07-21Adding a V8.7 compatibility version number.Hugo Herbelin
2017-07-21PMP sold us a Timeout on Windows with 1s resolution. Trying to improve it.Maxime Dénès
2017-07-20coq_makefile: use System.exists_dir for better portabilityEnrico Tassi
2017-07-20Windows: Sys.is_dir "foo/" always says no (so we strip trailing slash)Enrico Tassi
2017-07-20Also a less intrusive Profile.init_profile.Hugo Herbelin
Calling it only when there is something to profile, or when profiling is explicitly required with the profile flags, so that profiling in plugins is possible.
2017-07-20A less intrusive Profile.close_profile.Hugo Herbelin
No need to call Gc functions nor Unix timing functions when there is nothing to report. Moreover, PMP observed problems with these functions in the debugger. PMP also reported that Gc.minor takes some noticeable time, so no need to trigger some when unneeded.
2017-07-20Merge PR #898: [pp] Fix bugs 5651 [incorrect thunk in pretty printer]Maxime Dénès
2017-07-20Merge PR #869: Enforce alternating separators in typeclass debug outputMaxime Dénès
2017-07-19[pp] Fix bugs 5651 [incorrect thunk in pretty printer]Emilio Jesus Gallego Arias
Fix bug introduced by a Haskell programmer.
2017-07-17Merge PR #862: Adding support for bindings tags to explicit prefix/suffix ↵Maxime Dénès
rather than colors
2017-07-12format pairs of items for pr_depth to get alternating separatorsPaul Steckler
eval thunks once in prlist_sep_lastsep, make code clearer add typeclass debug output test