remove coqdocjs as submodule and add it normally

Author: amintimany

.gitmodules

@@ -1,3 +0,0 @@
-[submodule "coqdocjs"]
-	path = coqdocjs
-	url = https://github.com/coq-community/coqdocjs.git

coqdocjs

@@ -0,0 +1,34 @@
+.*.aux
+.*.d
+*.a
+*.cma
+*.cmi
+*.cmo
+*.cmx
+*.cmxa
+*.cmxs
+*.glob
+*.ml.d
+*.ml4.d
+*.mli.d
+*.mllib.d
+*.mlpack.d
+*.native
+*.o
+*.v.d
+*.vio
+*.vo
+*.vok
+*.vos
+.DS_Store
+.coq-native/
+.csdp.cache
+.lia.cache
+.nia.cache
+.nlia.cache
+.nra.cache
+csdp.cache
+lia.cache
+nia.cache
+nlia.cache
+nra.cache

coqdocjs/.gitignore

@@ -0,0 +1,21 @@
+Copyright (c) 2016, Tobias Tebbi
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions are met:
+    * Redistributions of source code must retain the above copyright
+      notice, this list of conditions and the following disclaimer.
+    * Redistributions in binary form must reproduce the above copyright
+      notice, this list of conditions and the following disclaimer in the
+      documentation and/or other materials provided with the distribution.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND
+ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED
+WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
+DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDERS BE LIABLE FOR ANY
+DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES
+(INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
+LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND
+ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
+SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

coqdocjs/LICENSE

@@ -0,0 +1,19 @@
+COQDOCJS_DIR ?= coqdocjs
+EXTRA_DIR = $(COQDOCJS_DIR)/extra
+COQDOCFLAGS ?= \
+  --toc --toc-depth 2 --html --interpolate \
+  --index indexpage --no-lib-name --parse-comments \
+  --with-header $(EXTRA_DIR)/header.html --with-footer $(EXTRA_DIR)/footer.html
+export COQDOCFLAGS
+COQMAKEFILE ?= Makefile.coq
+COQDOCJS_LN ?= false
+
+coqdoc: $(COQMAKEFILE)
+	$(MAKE) -f $^ html
+ifeq ($(COQDOCJS_LN),true)
+	ln -sf ../$(EXTRA_DIR)/resources html
+else
+	cp -R $(EXTRA_DIR)/resources html
+endif
+
+.PHONY: coqdoc

coqdocjs/Makefile.doc

@@ -0,0 +1,44 @@
+# CoqdocJS
+
+CoqdocJS is a little script to dynamically improve the coqdoc output.
+The result can be seen here:
+
+https://www.ps.uni-saarland.de/autosubst/doc/Ssr.POPLmark.html
+
+It offers the following features:
+- Customizable Unicode display:
+	It only changes the display, copy-paste from the website produces pure ASCII.
+	It only replaces complete identifiers or notation tokens, possibly terminated by numbers or apostrophes.
+	It does not replace randomly, like in "omega." or "tauto."
+	To add new symbols, edit [config.js](extra/resources/config.js).
+- Proof hiding:
+	All proofs longer than one line are hidden by default. They can be uncovered by clicking on "Proof...".
+
+All of this works with the ordinary coqdoc, by asking coqdoc to use a header file including the javascript files and some custom CSS.
+
+## Usage
+
+1. Clone this repository as a subdirectory or submodule;
+2. Include [Makefile.doc] in your `Makefile`, or copy it as, e.g., `Makefile.coq.local`;
+3. Run `make coqdoc` to build documentations.
+
+A minimal example is shown [here](example).
+
+### Environment Variables
+Name | Usage | Default
+---|---|---
+`COQDOCFLAGS` | Override the flags passed to `coqdoc` | see [Makefile.doc]
+`COQDOCEXTRAFLAGS` | Extend the flags passed to `coqdoc` | empty
+`COQDOCJS_LN` | If set to `true` then symlink resource files; otherwise copy | `false`
+`COQDOCJS_DIR` | Folder containing CoqdocJS | `coqdocjs`
+`COQMAKEFILE` | Makefile generated by `coq_makefile` | `Makefile.coq`
+
+## Files
+
+- [Makefile.doc]: a generic Makefile setup that calls coqc and coqdoc with the right parameters
+- [config.js](extra/resources/config.js): contains the unicode replacement table
+- [coqdoc.css](extra/resources/coqdoc.css): a replacement for the default Coqdoc CSS style. Can be removed to use the default style
+- [coqdocjs.js](extra/resources/coqdocjs.js) and [coqdocjs.css](extra/resources/coqdocjs.css): the script rewriting the DOM and adding the dynamic features with a corresponding CSS style
+- [header.html](extra/header.html) and [footer.html](extra/footer.html): custom header and footer files used in every generated html file
+
+[Makefile.doc]: Makefile.doc

coqdocjs/README.md

@@ -0,0 +1,3 @@
+Makefile.coq
+Makefile.coq.conf
+html/

coqdocjs/example/.gitignore

@@ -0,0 +1,21 @@
+COQMAKEFILE ?= Makefile.coq
+COQDOCEXTRAFLAGS = -s
+COQDOCJS_LN = true
+COQ_PROJ ?= _CoqProject
+
+all: $(COQMAKEFILE)
+	$(MAKE) -f $^ $@
+
+clean: $(COQMAKEFILE)
+	$(MAKE) -f $^ cleanall
+	$(RM) $^ $^.conf
+
+$(COQMAKEFILE): $(COQ_PROJ)
+	$(COQBIN)coq_makefile -f $^ -o $@
+
+force $(COQ_PROJ) Makefile: ;
+
+%: $(COQMAKEFILE) force
+	@+$(MAKE) -f $< $@
+
+.PHONY: clean all force

coqdocjs/example/Makefile

@@ -0,0 +1 @@
+coqdocjs/Makefile.doc

coqdocjs/example/Makefile.coq.local

@@ -0,0 +1,4 @@
+# CoqdocJS Usage Example
+This folder contains a minimal example to use CoqdocJS in your project.
+
+You can build the docs with `make coqdoc`.