** 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, 7 insertions, 4 deletions

diff --git a/ide/ideutils.ml b/ide/ideutils.ml
index b79e4b936..f4fd73d6f 100644
--- a/ide/ideutils.ml
+++ b/ide/ideutils.ml
@@ -268,9 +268,11 @@ let run_command f c =
   (Unix.close_process_full (cin,cout,cerr),  Buffer.contents result)
 
 let browse f url =
-  let l,r = !current.cmd_browse in
-  let (_s,_res) = run_command f (l ^ url ^ r) in
-  ()
+  let com = Flags.subst_command_placeholder !current.cmd_browse url in
+  let (s,_res) = run_command f com in
+  if s = Unix.WEXITED 127 then
+    prerr_endline
+      ("Could not execute\n  \""^com^"\"\ncheck your preferences for setting a valid browser command")
 
 let url_for_keyword =
   let ht = Hashtbl.create 97 in
@@ -295,7 +297,8 @@ let url_for_keyword =
 
 let browse_keyword f text = 
   try let u = url_for_keyword text in browse f (!current.doc_url ^ u) 
-  with _ -> ()
+  with Not_found ->
+    prerr_endline ("No documentation found for "^text)
 
 
 let underscore = Glib.Utf8.to_unichar "_" (ref 0)