** Efficacité, bugs, robustesse CoqIDE **

- Suppression d'une source de fuite mémoire dans declare_mod.ml (la
  table de hash library_table n'était pas synchronisée avec le reset
  et elle grossissait à chaque rejeu de la session; utilisation au
  passage d'une map pour que la synchronisation avec le reset soit
  plus rapide). [mod_typing.ml]

- Correction d'un bug de synchronisation pour le niveau pattern 200.
  [pcoq.ml4]

- Suppression d'un vieux reste du traducteur [constructeur VernacVar]

- Robustesse et uniformité accrue dans CoqIDE vis à vis du statut de
  chacune des commandes vernaculaires par l'utilisation d'une fonction
  d'assignation d'attributs à chaque commande vernac.

  Correction de ce qui semble être des bizarreries
  (VernacDeclareTacticDefinition considéré comme ouvrant un but;
  suppression des "loc" dans les Reset: ne pouvait pas faire
  fonctionner correctement update_on_end_of_segment).

  Suppression de la nécessité d'expliciter si une commande retourne
  des messages dépendants du mode "verbose" (on suppose que chaque
  commande sait ce qu'elle doit dire selon la position du flag verbose).

  Sinon, le mécanisme de Reset de CoqIDE reste pauvre. CoqIDE ne
  sait revenir qu'aux états associés à des noms et cela ne vaut pas
  l'approche de Proof General. Il sera sans doute opportun de se
  brancher sur l'architecture de Pierre Courtieu à base de "Backtrack".

  La restriction des buts imbriqués a-t-elle vraiment une raison
  d'être ? En plus les commandes non cablées en dur comme Next
  Obligation ne sont pas prises en compte.

  Interdiction, dès Coq, d'ouvrir sections ou modules si preuve en cours.

  Réparation approximative de l'option "Help for Keyword" de Coqide
  mais encore à faire pour plus de robustesse (makefile, installation,
  synchronisation entre la version du fichier index_urls.txt et la
  version du refman, ...).



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

1 files changed, 9 insertions, 0 deletions

diff --git a/Makefile.doc b/Makefile.doc
index 3f28adf46..69726e9cb 100644
--- a/Makefile.doc
+++ b/Makefile.doc
@@ -198,6 +198,15 @@ doc/RecTutorial/RecTutorial.v.pdf: doc/common/version.tex doc/common/title.tex d
 doc/RecTutorial/RecTutorial.v.html: doc/RecTutorial/RecTutorial.v.tex
 	(cd doc/RecTutorial; hevea -exec xxdate.exe RecTutorial.v)
 
+######################################################################
+# Index file for CoqIDE
+######################################################################
+
+# Not robust, improve...
+ide/index_urls.txt: doc/refman/html/index.html
+	- rm ide/index_url.txt
+	cat doc/refman/html/command-index.html doc/refman/html/tactic-index.html | grep li-itemize | grep HREF | sed -e 's@.*<TT>\(.*\)</TT>.*, <A HREF="\(.*\)">.*@\1,\2@' > ide/index_urls.txt
+
 
 ######################################################################
 # Install all documentation files