Building it manually from individual parts was a bit tricky, but knowing in theory how things should fit together, I managed after two failed attempts. Note that
COQBIN really needs an extra slash at the end, or the Makefile will break down.
Here is a screenshot of Coq/jEdit on Linux with GTK look-and-feel, editing a medium-sized file from the Coq library:
There is an important conceptual difference to Isabelle/jEdit, which edits a whole project (or “session”) with many files active at the same time within the same prover process.
In contrast, Coq has capitalized separate compilation a long time ago, so it is likely that its one-to-one relation of files versus sessions (with a separate coqtop for each) will remain in years to come.
Update 02-Feb-2015: Carst Tankink has just announced the second public beta Coq/jEdit 0.2.0 for Coq 8.5beta1.
Strictly speaking the Isabelle environment is for interactive and automated theorem proving, but its SML IDE support is quite sophisticated: source files are statically checked and semantically evaluated while the user is editing. The annotated sources contain markup about inferred types, references to defining positions of items etc.
As a quick start, see the Documentation panel, section Examples, entry src/Tools/SML/Examples.thy (as of Isabelle2014).
The time where SML sources need to be edited with vi or emacs are over. See also this related thread on Stackoverflow.