From 7208928de37565a9e38f9540f2bfb1e7a3b877e6 Mon Sep 17 00:00:00 2001
From: ppedrot
Date: Mon, 17 Sep 2012 20:46:20 +0000
Subject: More cleaning on Utils and CList. Some parts of the code being
 peculiarly messy, I hope I did not introduce too many bugs.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15815 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 checker/checker.ml | 16 +++++++++-------
 1 file changed, 9 insertions(+), 7 deletions(-)

(limited to 'checker')

diff --git a/checker/checker.ml b/checker/checker.ml
index f43a03f4a5..a75aed5332 100644
--- a/checker/checker.ml
+++ b/checker/checker.ml
@@ -72,18 +72,20 @@ let add_path ~unix_path:dir ~coq_root:coq_dirpath =
 let convert_string d =
   try id_of_string d
   with _ ->
-    if_verbose msg_warning
-      (str ("Directory "^d^" cannot be used as a Coq identifier (skipped)"));
-    flush_all ();
-    failwith "caught"
+    if_verbose msg_warning (str ("Directory "^d^" cannot be used as a Coq identifier (skipped)"));
+    raise Exit
 
 let add_rec_path ~unix_path ~coq_root =
   if exists_dir unix_path then
     let dirs = all_subdirs ~unix_path in
     let prefix = repr_dirpath coq_root in
-    let convert_dirs (lp,cp) =
-      (lp,make_dirpath (List.map convert_string (List.rev cp)@prefix)) in
-    let dirs = map_succeed convert_dirs dirs in
+    let convert_dirs (lp, cp) =
+      try
+        let path = List.map convert_string (List.rev cp) @ prefix in
+        Some (lp, Names.make_dirpath path)
+      with Exit -> None
+    in
+    let dirs = List.map_filter convert_dirs dirs in
     List.iter Check.add_load_path dirs;
     Check.add_load_path (unix_path, coq_root)
   else
-- 
cgit v1.2.3