coq/ide/utils, branch master

[ide] Move common protocol library to its own folder/object.

2018-05-24T11:21:59+00:00

The `ide` folder contains two different binaries, the language server
`coqidetop` and `coqide` itself.

Even if these binaries are in the same folder, the only thing they
have in common is that they link to the protocol files. In the OCaml
world, having "doubly" linked files in the same project is considered
a bit of an ugly practice, and some build tools such as Dune disallow it.q

Thus, to clean up the build, we move the common protocol files to its
own library `ideprotocol`.

This helps towards Dune integration and towards having an IDE
standalone target, such as the one that was implemented here:
https://github.com/ejgallego/coqide-exp

Drop '.' from CErrors.anomaly, insert it in args

2017-06-03T00:06:05+00:00

As per https://github.com/coq/coq/pull/716#issuecomment-305140839

Partially using
```bash
git grep --name-only 'anomaly\s*\(~label:"[^"]*"\s*\)\?\(Pp.\)\?(\(\(Pp.\)\?str\)\?\s*".*[^\.!]")' | xargs sed s'/\(anomaly\s*\(~label:"[^"]*"\s*\)\?\(Pp.\)\?(\(\(Pp.\)\?str\)\?\s*".*\s*[^\.! ]\)\s*")/\1.")/g' -i
```
and
```bash
git grep --name-only ' !"' | xargs sed s'/ !"/!"/g' -i
```
The rest were manually edited by looking at the results of
```bash
git grep anomaly | grep '\.ml' | grep -v 'anomaly\s*\(~label:"[^"]*"\s*\)\?\(Pp\.\)\?(\(\(Pp.\)\?str\)\?\s*".*\(\.\|!\)")' | grep 'anomaly\($\|[^_]\)' | less
```

Removing dead code in CoqIDE.

2016-09-21T13:14:05+00:00

There was a pile of dead code inherited from Cameleon just sitting around and
not used at all. This code was introduced in 2003 and never actually used.

CLEANUP: removing a function that duplicates its counterpart already present in the Ocaml standard library

2016-08-30T08:36:59+00:00

Removing dead code and unused opens.

2016-05-08T17:59:03+00:00

Switch the few remaining iso-latin-1 files to utf8

2014-12-09T13:27:21+00:00

"allows to", like "allowing to", is improper

2014-08-25T13:22:40+00:00

It's possible that I should have removed more "allows", as many
instances of "foo allows to bar" could have been replaced by "foo bars"
(e.g., "[Qed] allows to check and save a complete proof term" could be
"[Qed] checks and saves a complete proof term"), but not always (e.g.,
"the optional argument allows to ignore universe polymorphism" should
not be "the optional argument ignores universe polymorphism" but "the
optional argument allows the caller to instruct Coq to ignore universe
polymorphism" or something similar).

Remove many superfluous 'open' indicated by ocamlc -w +33

2014-03-05T14:41:21+00:00

 With ocaml 4.01, the 'unused open' warning also checks the mli :-)

 Beware: some open are reported as useless when compiling with camlp5,
 but are necessary for compatibility with camlp4. These open are now
 marked with a comment.

Coqide: use labels for all labelled functions

2012-12-08T20:44:56+00:00

 This isn't mandatory, but it's a good practice.
 For instance it allows to easily locate all ~callback arguments.
 Cf. warning 6 of OCaml 4

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16051 85f007b7-540e-0410-9357-904b9bb8a0f7

Coqide uses Glib to get the XDG_DATA/CONFIG_HOME/DIRS

2012-09-12T14:10:37+00:00

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15793 85f007b7-540e-0410-9357-904b9bb8a0f7