aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools/coqdoc/main.ml
Commit message (Collapse)AuthorAge
* Update copyright headers.Gravatar Maxime Dénès2016-01-20
|
* Clarifying the doc of coqdoc --utf8 as discussed on coq-club on August 19, 2015.Gravatar Hugo Herbelin2015-09-26
|
* Remove usage of Printexc.catch in the tools, as it is deprecated since 2001.Gravatar Guillaume Melquiond2015-07-30
| | | | | | | | "This function is deprecated: the runtime system is now able to print uncaught exceptions as precisely as Printexc.catch does. Moreover, calling Printexc.catch makes it harder to track the location of the exception using the debugger or the stack backtrace facility. So, do not use Printexc.catch in new code."
* Update headers.Gravatar Maxime Dénès2015-01-12
|
* Switch the few remaining iso-latin-1 files to utf8Gravatar Pierre Letouzey2014-12-09
|
* coqdoc is minimaly -Q awareGravatar Pierre Boutillier2014-07-03
|
* Updating headers.Gravatar herbelin2012-08-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added checksums to glob files and warned about possibly missingGravatar herbelin2011-10-29
| | | | | | packages for utf8. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14623 85f007b7-540e-0410-9357-904b9bb8a0f7
* In Coq_config: get rid of coqsrc and make coqlib optionalGravatar glondu2011-09-27
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | I assume that once Coq is installed in non-local mode and run from its installed path, sources are no longer available. The coqsrc variable doesn't make any sense, then, and its intended value can always be inferred from Sys.executable_name. Moving it to Envars.coqroot. Make coqlib optional. Currently, it is set to None only in -local mode or with ocamlbuild. When set to None, -local layout is assumed (binaries in ./bin, library in .). The behaviour should not be changed when an explicit coqlib has been given to ./configure. This commit should make it possible to run a Coq compiled with -local from anywhere (no hard-coded absolute path embedded in the executables, intermediary step to bug #2565). It WILL BREAK settings re-using source trees after installation in non-local mode (are there actual use cases for that?). Hard-coded absolute paths still remain: - in the build system, so the need to re-run ./configure after moving the source tree is still expected for now; - in coqrunbyteflags, I think we are limited by ocaml itself; - docdir. All absolute paths should be removed, ultimately. As a side-effect, simplify computing of Envars.coqbin. I don't see any good reason to keep it as a function. Disclaimers: - initialization of Sys.executable_name is not consistent across all architectures; relying so much on it might trigger bugs. I'm pretty sure something will explode if one adds arbitrary symlinks on top of that; - ocamlbuild stuff not tested. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14500 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix for handling of -R "" in coqdoc (bug #2423).Gravatar herbelin2011-04-25
| | | | | | (submitted by Tom Prince <tom.prince@ualberta.net>) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14063 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coqdoc patches from UPenn (thanks to C. Casinghino). This introduces theGravatar msozeau2010-09-28
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | ability to format inference rules (delimited by [[[ ]]]) and adds some new flags. Here's the message from Chris: - coqdoc now has support for inference rules inside coqdoc comments. These should be enclosed in triple square brackets with the following format. [[[ |- t1 : Bool |- t2 : T |- t3 : T ---------------------------- (T_If) |- if t1 then t2 else t3 : T ]]] The rule's name is optional. Multiple inference rules may be included in the same [[[ ]]] block, separated by blank lines. See http://www.cis.upenn.edu/~bcpierce/sf/Stlc.html#lab469 for some examples of the output. The output will only be pretty in html - in other formats it is printed verbatim (though it shouldn't be hard to add latex support, and I may soon). - Two new coqdoc flags have been added. First, --inline-notmono causes inline code to be printed in a proportional width font (adjustable in the css file). Second, --no-glob tells coqdoc not to look for .glob files (no links will be inserted for identifiers when this flag is used). - Finally, the handling of paragraphs and whitespace around lists has been made somewhat saner. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13473 85f007b7-540e-0410-9357-904b9bb8a0f7
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13323 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remove compile-command pragmas for emacsGravatar letouzey2010-05-19
| | | | | | | | | | | | | | | | | | | These declarations (e.g. make -C .. bin/coqtop.byte) are quite annoying when debugging stuff over the whole archive: all of a sudden, M-x recompile isn't doing what you intended just because you've visited some specific files. Instead: - Feel free to rather add intermediate targets in the Makefile if they aren't there yet. - For avoiding typing the -C with many .. after, you can have a look at my recursively-descending make: http://www.pps.jussieu.fr/~letouzey/download/make.sh which is to be renamed make and placed in a bin dir with more priority than /usr/bin. Beware! I've already add a few bad surprises with this hack, but it's really convenient nonetheless. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13014 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
| | | | | | | | | | | - Many of them were broken, some of them after Pierre B's rework of mli for ocamldoc, but not only (many bad annotation, many files with no svn property about Id, etc) - Useless for those of us that work with git-svn (and a fortiori in a forthcoming git-only setting) - Even in svn, they seem to be of little interest git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12972 85f007b7-540e-0410-9357-904b9bb8a0f7
* New model for user-driven translation of tokens in coqdocGravatar herbelin2010-04-06
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | In the initial model (formerly to r11432), coqdoc parsed separatedly letters and symbolic characters and was thus not able to translate tokens mixing letters and symbolic characters such as "\in" or "=_h". Revision 11432 extended the definition of translatable tokens by supporting letters in it with the benefit of supporting "\in" or "=_h" but added the constraint of requiring spaces to correctly separate tokens in expressions such as "x : nat" which otherwise would be split into "x" and ":nat", then leading to fail understanding "nat" as a proper reference. The new model renounces to define a lexical category of tokens and uses instead a dynamically extensible sublexer similar to the one used in the Coq lexer. The new model works even if tokens are not separated by spaces in the source file and it thus solves problems such as the one mentioned in bug #2273 (failure to link C in "`(!C)"). However, it imposes a stronger discipline in writing the lexing rules in cpretty.mll because the characters that can eventually contribute to the application of a printing rule are buffered in the sublexer and no output is allowed to occur until the buffer of the sublexer if flushed. The theoretical overhead due to the intermediate use of buffers is apparently less than 5%. More details on the token cutting discipline can be found in the new file token.mli. Incidentally fixed two small problems with notation links in LaTeX: made escaping of characters in LaTeX labels more robust so that notations do not easily get the same label name; avoid only highlighting the first '"' of a notation def (failing to have now a better highlighting strategy). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12905 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixed small bugs introduced in commit 12890 (bug #2286, that comesGravatar herbelin2010-03-30
| | | | | | | from a incorrect computation of logical names + bug in rendering of name-based notations, aka abbreviations or syntactic definitions). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12893 85f007b7-540e-0410-9357-904b9bb8a0f7
* Several bug-fixes and improvements of coqdocGravatar herbelin2010-03-29
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | - make links to section variables working (used qualified names for disambiguation and fixed the place in intern_var where to dump them) (wish #2277) - mapping of physical to logical paths now follows coq (see bug #2274) (incidentally, it was also incorrectly seeing foobar.v as a in directory foo) - added links for notations - added new category "other" for indexing entries not starting with latin letter (e.g. notations or non-latin identifiers which was otherwise broken) - protected non-notation strings (from String.v) from utf8 symbol interpretation - incidentally quoted parseable _ in notations to avoid confusion with placeholder in the "_ + _" form of notation - improved several "Sys_error" error messages - fixed old bug about second dot of ".." being interpreted as regular dot - removed obsolete lexer in index.mll (and renamed index.mll to index.ml) - added a test-suite file for testing various features of coqdoc Things that still do not work: - when a notation is redefined several times in the same scope, only the link to the first definition works - if chars and symbols are not separated in advance, idents that immediately follow symbols are not detected (e.g. as in {True}+{True} where coqdoc sees a symbol "+{True}") - parentheses, curly brackets and semi-colon not linked in notations Things that can probably be improved: - all notations are indexed in the same category "other"; can we do better? - all non-latin identifiers (e.g. Greek letters) are also indexed in the same "other" category; can we do better? - globalization data for notations could be compacted (currently there is one line per each proper location covered by the notation) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12890 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added option --external to coqdoc to bind an url to an external library.Gravatar herbelin2009-10-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12426 85f007b7-540e-0410-9357-904b9bb8a0f7
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
* Incorporate coqdoc changes by the UPenn team (B.Pierce, C. Casinghino,Gravatar msozeau2009-09-04
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | M. Greenberg) and add support for interpolation to HTML output. The patch is mostly backwards-compatible, except for the CSS style which needs more readaptation. Doc for the new options will come as well. - lists have been updated substantially. In particular, multiparagraph list items are now supported and sublists work better, using an "off-side" rule. - the "--index" flag allows one to change the name of the generated index file (good since index.html has a special meaning). - the "--toc-depth <int>" flag allows one to limit how many levels are included in the toc. - the "--lib-name <string>" flag allows one to specify what libraries are called, instead of just sticking "Library" before each module name (for example, "Module" or "Chapter" might be more sensible in some contexts). Additionally "--no-lib-name" eliminates this extra title completely. - the "--lib-subtitles" flag allows one to specify subtitles for libraries. When enabled, the beginning of each file is checked for a comment of the form: (** * ModuleName : text *) and the text will be printed as a subtitle in the appropriate places. - Text can be made italic by putting it inside underscores, as in: _emphasized text_. This has the advantage of looking OK in the .v file as well. A few simple rules are followed to make sure identifiers with underscores aren't accidentally made italic. - Various changes have been made in an attempt to beautify the output, especially in html, while allowing the .v sources to look decent as well. Mostly these involve whitespace. - The coqdoc.css file has been changed. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12308 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add --plain-comments patch by F. Garillot, which also addsGravatar msozeau2009-09-03
| | | | | | | | | interpretation of [[ etc... inside (* *) comments when --parse-comments is used. Add some additional fixes from B. Pierce on formatting verbatim and the HTML Toc. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12307 85f007b7-540e-0410-9357-904b9bb8a0f7
* Report de la révision #12104 (Maj lien site web de Coq)Gravatar notin2009-04-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12105 85f007b7-540e-0410-9357-904b9bb8a0f7
* pretty.mll of coqdoc becomes cpretty.mll (avoid clash with a camlp5 file)Gravatar letouzey2009-03-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12011 85f007b7-540e-0410-9357-904b9bb8a0f7
* coqdoc fixes and support for parsing regular comments (request byGravatar msozeau2009-03-22
| | | | | | | | | | | | B. Pierce on coq-club). - Output regular comments, enclosed in a span in HTML (with (* *) delimiters) and inside a new environment in LaTeX. - HTML output: put the span inside anchors in links, so as to keep the same style as for definitions (customizable in the CSS). - Better handling of Next Obligation. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12004 85f007b7-540e-0410-9357-904b9bb8a0f7
* Report des revisions #11826, #11828 et #11829 de v8.2 vers trunkGravatar notin2009-02-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11915 85f007b7-540e-0410-9357-904b9bb8a0f7
* Patch by Brian Campbell to output more information on the exception thatGravatar msozeau2009-01-15
| | | | | | | made a glob file unreadable. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11788 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suite de la révision #11756Gravatar notin2009-01-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11757 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nettoyage des variables Coq et amélioration de coqmktop. LesGravatar notin2008-12-19
| | | | | | | | | | | | | | | | | | | | | | | | | | | principaux changements sont: - coqtop (et coqc) maintenant insensible aux variables d'environnement COQTOP, COQBIN et COQLIB; le chemin vers les librairies Coq peut être spécifié par l'option -coqlib - coqmktop prend 4 nouvelles options: -boot, -coqlib, -camlbin et -camlp4bin; en mode boot, coqmktop se réfère à Coq_config pour les chemins des exécutables OCaml; en dehors du mode boot, coqmktop cherche les exécutables OCaml dans PATH - installation des *.cmxs *.o et *.a en plus des *.cm[ioxa]; ceux-ci étant installé en copiant l'architecture des sources (ie lib.cmxa est installé dans COQLIB/lib/lib.cmxa) - coq_makefile prend maintenant 3 paramètres sous forme de variables d'environnement: COQBIN pour dire où trouver les exécutables Coq, CAMLBIN et CAMLP4BIN pour les exécutables OCaml et Camlp4/5; les chemins vers les librairies sont déduits en utilisant -where Le tout a testé avec Ssreflect (cf coq-contribs) en essayant de simuler les conditions de la vie réelle (Ocaml pas dans le PATH, installation binaire relocalisée, ...). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11707 85f007b7-540e-0410-9357-904b9bb8a0f7
* Amélioration du README.doc et de l'installation de la docGravatar notin2008-11-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11591 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout d'une option -raw pour Coqdoc (sortie en texte brut)Gravatar notin2008-10-31
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11529 85f007b7-540e-0410-9357-904b9bb8a0f7
* Improvements in coqdoc:Gravatar msozeau2008-09-25
| | | | | | | | | | | | | | | | - Better handling of spaces by actually ignoring what's inside proof scripts in light/gallina mode (detection of [Proof with] vs [Proof.] vs [Proof t.] and [Qed]/[Save]/...). - Provide fancy replacements for forall,/\,... etc in HTML in case the utf8 option is on. - Use typesetting information in HTML output and customize the CSS accordingly. The default color scheme follows closely the one set by Conor for Epigram; of course one can change it. - A try at interpolating identifiers in comments if they are defined in the same module, with a corresponding flag. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11421 85f007b7-540e-0410-9357-904b9bb8a0f7
* Rétablissement de l'option -dump-glob de coq top et de l'option -glob-from ↵Gravatar notin2008-07-18
| | | | | | de coqdoc (compatibilité) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11236 85f007b7-540e-0410-9357-904b9bb8a0f7
* Improvements on coqdoc by adding more information into .globGravatar msozeau2008-05-30
| | | | | | | | | | | | | | | | | | | | | | | files, about definitions and type of references. - Add missing location information on fixpoints/cofixpoint in topconstr and syntactic definitions in vernacentries for correct dumping. - Dump definition information in vernacentries: defs, constructors, projections etc... - Modify coqdoc/index.mll to use this information instead of trying to scan the file. - Use the type information in latex output, update coqdoc.sty accordingly. - Use the hyperref package to do crossrefs between definition and references to coq objects in latex. Next step is to test and debug it on bigger developments. On the side: - Fix Program Let which was adding a Global definition. - Correct implicits for well-founded Program Fixpoints. - Add new [Method] declaration kind. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11024 85f007b7-540e-0410-9357-904b9bb8a0f7
* add support for pdf in coqdoc, add export to pdf in coqide, port open and ↵Gravatar jnarboux2008-05-28
| | | | | | save as dialogs of coqide to a not deprecated widget, add filtering of *.v files in these dialogs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11006 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout d'options a coqdoc pour l'entete htmlGravatar notin2008-04-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10764 85f007b7-540e-0410-9357-904b9bb8a0f7
* Génération d'une toc en html et avec l'option -psGravatar notin2008-02-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10597 85f007b7-540e-0410-9357-904b9bb8a0f7
* Amélioration de la gestion des chemins physiques (corrige au passage le bug ↵Gravatar notin2008-02-27
| | | | | | #939 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10594 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction d'un bug de Coqdoc (indentation des lignes)Gravatar notin2008-02-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10583 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug de Coqdoc avec l'option -RGravatar notin2008-02-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10569 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction du bug #1512Gravatar notin2008-02-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10562 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression de l'option -glob-from de Coqdoc: les globalisations sontGravatar notin2008-02-13
| | | | | | | | lues directement des fichiers .glob git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10559 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction des bugs #1455 et #1456Gravatar notin2007-03-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9728 85f007b7-540e-0410-9357-904b9bb8a0f7
* A tentative fix for bug #1455Gravatar lmamane2007-03-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9726 85f007b7-540e-0410-9357-904b9bb8a0f7
* Option --coqlib_path pour coqdoc (suite et fin)Gravatar notin2006-05-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8777 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout d'une option --coqlib_path pour Coqdoc (modification suggérée par S. ↵Gravatar notin2006-05-02
| | | | | | Mimram) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8775 85f007b7-540e-0410-9357-904b9bb8a0f7
* git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8762 ↵Gravatar notin2006-04-28
| | | | 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout de la doc de l'option -stdout de coqdocGravatar notin2006-04-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8749 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction d'un bug dans coqdoc sur l'utilisation de l'option -o et la ↵Gravatar notin2006-04-26
| | | | | | création du fichier de style git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8734 85f007b7-540e-0410-9357-904b9bb8a0f7
* - correction d'un bug dans coqdoc (multi_index)Gravatar notin2006-03-28
| | | | | | | - modif. de la génération de la doc de stdlib git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8669 85f007b7-540e-0410-9357-904b9bb8a0f7
* r8709@thot: notin | 2006-03-25 01:48:46 +0100Gravatar notin2006-03-25
| | | | | | | | - Ajout de FSets dans la doc de stdlib - coqdoc copie la feuille de style dans le répertoire courant git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8663 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-28 07:09:04 +0000