diff --git a/README b/README
index dda77999f..cd954d297 100644
--- a/README
+++ b/README
@@ -181,7 +181,9 @@ src/ Sources for libspot.
man/ Man pages for the above tools.
sanity/ Sanity tests for the whole project.
doc/ Documentation for libspot.
+ org/ Source of userdoc/ as org-mode files.
tl/ Documentation of the Temporal Logic operators.
+ userdoc/ HTML documentation about the command-line tools.
spot.html/ HTML reference manual for the library.
bench/ Benchmarks for ...
emptchk/ ... emptiness-check algorithms,
diff --git a/configure.ac b/configure.ac
index fb4756210..814ad4dba 100644
--- a/configure.ac
+++ b/configure.ac
@@ -91,7 +91,7 @@ if test x$enable_warnings = xyes; then
fi
AM_CONDITIONAL([NEVER], [false])
-# We need the absolute path for dot in the "doc/dot" script. Other place
+# We need the absolute path for dot in the "doc/dot" script. Other places
# only require a relative path.
AC_PATH_PROG([DOT], [dot])
AC_CHECK_PROG([LBT], [lbt], [lbt])
@@ -102,6 +102,7 @@ AC_CHECK_PROG([LTL2NBA], [script4lbtt.py], [script4lbtt.py])
AC_CHECK_PROG([PERL], [perl], [perl])
AC_CHECK_PROG([SPIN], [spin], [spin])
AC_CHECK_PROG([LBTT], [lbtt], [lbtt])
+AC_CHECK_PROG([EMACS], [emacs], [emacs])
AC_CHECK_PROG([LBTT_TRANSLATE], [lbtt-translate], [lbtt-translate])
AX_CHECK_VALGRIND
AC_CHECK_PROG([WRING2LBTT], [wring2lbtt], [wring2lbtt])
@@ -126,6 +127,7 @@ AC_CONFIG_FILES([
doc/Doxyfile
doc/Makefile
doc/tl/Makefile
+ doc/org/init.el
iface/dve2/defs
iface/dve2/Makefile
iface/gspn/defs
diff --git a/doc/Makefile.am b/doc/Makefile.am
index 3e2b033e6..d2c2f2c63 100644
--- a/doc/Makefile.am
+++ b/doc/Makefile.am
@@ -26,7 +26,7 @@ SUBDIRS = tl
.PHONY: doc fast-doc
-all-local: $(srcdir)/stamp
+all-local: $(srcdir)/stamp $(srcdir)/org-stamp
doc:
-rm -f $(srcdir)/stamp
@@ -49,9 +49,34 @@ $(srcdir)/spot.html $(srcdir)/spot.tag: $(srcdir)/stamp
# Spot documentation.
dist_pkgdata_DATA = $(srcdir)/spot.tag
+.PHONY: org
+org:
+ cd $(top_srcdir) && make doc/org/init.el
+ rm -rf $(srcdir)/userdoc; mkdir -p tmp; cd tmp; \
+ $(EMACS) --batch -Q -l $(abs_srcdir)/org/init.el
+ rm -rf tmp
+
+ORG_FILES = \
+ org/.dir-locals.el \
+ org/init.el \
+ org/syntax.css \
+ org/genltl.org \
+ org/ioltl.org \
+ org/ltl2tgba.org \
+ org/ltl2tgta.org \
+ org/ltlcross.org \
+ org/ltlfilt.org \
+ org/randltl.org \
+ org/tools.org
+
+$(srcdir)/org-stamp: $(ORG_FILES) $(configure_ac)
+ make org && touch $@
+
EXTRA_DIST = \
footer.html \
mainpage.dox \
$(srcdir)/stamp \
$(srcdir)/spot.html \
- org/.dir-locals.el
+ $(ORG_FILES) \
+ $(srcdir)/org-stamp \
+ userdoc
diff --git a/doc/org/.gitignore b/doc/org/.gitignore
index 32bc90c2f..f36dec1de 100644
--- a/doc/org/.gitignore
+++ b/doc/org/.gitignore
@@ -5,3 +5,4 @@ err
*.json
scheck.ltl
sum.py
+init.el
diff --git a/doc/org/init.el.in b/doc/org/init.el.in
new file mode 100644
index 000000000..564ac2415
--- /dev/null
+++ b/doc/org/init.el.in
@@ -0,0 +1,33 @@
+(require 'org-publish)
+(require 'org-install)
+
+
+(print (concat "Org " (org-version)))
+(setq org-export-htmlize-output-type 'css)
+
+(setq org-babel-python-command "/usr/bin/python3")
+(org-babel-do-load-languages
+ 'org-babel-load-languages
+ '((sh . t)
+ (dot . t)
+ (python . t)))
+(setq org-confirm-babel-evaluate nil)
+
+(setq org-publish-project-alist
+ '(("spot-html"
+ :base-directory "@abs_top_srcdir@/doc/org/"
+ :base-extension "org"
+ :publishing-directory "@abs_top_srcdir@/doc/userdoc/"
+ :recursive t
+ :publishing-function org-publish-org-to-html
+ :style "\n\n"
+ :auto-preamble t)
+ ("spot-static"
+ :base-directory "@abs_top_srcdir@/doc/org/"
+ :base-extension "css\\|js\\|png\\|jpg\\|gif\\|pdf"
+ :publishing-directory "@abs_top_srcdir@/doc/userdoc/"
+ :recursive t
+ :publishing-function org-publish-attachment)
+ ("spot-all" :components ("spot-html" "spot-static"))))
+
+(org-publish-all t)
diff --git a/doc/org/syntax.css b/doc/org/syntax.css
new file mode 100644
index 000000000..ed1eebe5c
--- /dev/null
+++ b/doc/org/syntax.css
@@ -0,0 +1,875 @@
+