fixed some illegal backslash escapes

diff --git a/helm/gTopLevel/oldDisambiguate.ml b/helm/gTopLevel/oldDisambiguate.ml
index db118b5187516a129ed59278a3e2cd059f9a2953..b760b3b8ce86d4c6e3ee3dd19fe934b7cd741195 100644 (file)
--- a/helm/gTopLevel/oldDisambiguate.ml
+++ b/helm/gTopLevel/oldDisambiguate.ml
@@ -322,12 +322,13 @@ module EnvironmentP3 =
     let regexpr =
      let alfa = "[a-zA-Z_-]" in
      let digit = "[0-9]" in
-     let ident = alfa ^ "\(" ^ alfa ^ "\|" ^ digit ^ "\)*" in
-     let blanks = "\( \|\t\|\n\)+" in
+     let ident = alfa ^ "\\(" ^ alfa ^ "\\|" ^ digit ^ "\\)*" in
+     let blanks = "\\( \\|\t\\|\n\\)+" in
      let nonblanks = "[^ \t\n]+" in
-     let uri = "/\(" ^ ident ^ "/\)*" ^ nonblanks in (* not very strict check *)
+     let uri = "/\\(" ^ ident ^ "/\\)*" ^ nonblanks in
+      (* not very strict check *)
       Str.regexp
-       ("alias" ^ blanks ^ "\(" ^ ident ^ "\)" ^ blanks ^ "\(" ^ uri ^ "\)")
+       ("alias" ^ blanks ^ "\\(" ^ ident ^ "\\)" ^ blanks ^ "\\(" ^ uri ^ "\\)")
     in
      let rec aux n =
       try