From 3dc75a9ff15d4c699a0c6f95bcdc918dde511b8b Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Wed, 8 Sep 2004 13:32:39 +0000 Subject: [PATCH] fixed some illegal backslash escapes --- helm/gTopLevel/oldDisambiguate.ml | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/helm/gTopLevel/oldDisambiguate.ml b/helm/gTopLevel/oldDisambiguate.ml index db118b518..b760b3b8c 100644 --- 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 -- 2.39.2