From: natile Date: Fri, 11 Oct 2002 07:40:54 +0000 (+0000) Subject: Use patched. X-Git-Tag: BEFORE_METADATA_FOR_SORT_AND_REL~37 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=410e98af46d5b776223452dee2102d9eb14d67e0;p=helm.git Use patched. --- diff --git a/helm/ocaml/mathql_interpreter_galax/use.ml b/helm/ocaml/mathql_interpreter_galax/use.ml index c2a716b23..ab4fa6c73 100644 --- a/helm/ocaml/mathql_interpreter_galax/use.ml +++ b/helm/ocaml/mathql_interpreter_galax/use.ml @@ -5,24 +5,23 @@ open Mathql_semantics;; let rec attl uril svar = match uril with | head::tail -> let suri = List.hd uril in - let len = String.length suri in - let scuri = String.sub suri 4 (len-4) in - if String.contains scuri '#' then - let pos = String.index scuri '#' in + let len = String.length suri in + let scuri = String.sub suri 4 (len-4) in + if String.contains scuri '#' then + let pos = String.index scuri '#' in let s1 = Str.string_before scuri pos in - let xp = Str.string_after scuri pos in - let xp = Str.global_replace (Str.regexp "#xpointer(1") "" xp in - let xp = Str.global_replace (Str.regexp "\/") "," xp in - let xp = Str.global_replace (Str.regexp ")") "" xp in - let scuri = (s1 ^ xp) in - - let uril_tl = List.tl uril in + let xp = Str.string_after scuri pos in + let xp = Str.global_replace (Str.regexp "#xpointer(1") "" xp in + let xp = Str.global_replace (Str.regexp "\/") "," xp in + let xp = Str.global_replace (Str.regexp ")") "" xp in + let scuri = (s1 ^ xp) in + let uril_tl = List.tl uril in {uri = scuri; attributes = [(svar, (List.hd uril_tl))]; extra = ""} :: (attl (List.tl uril_tl) svar) - else + else let uril_tl = List.tl uril in - {uri = scuri; attributes = [(svar, (List.hd - uril_tl))]; extra = ""} :: (attl (List.tl uril_tl) svar) + {uri = scuri; attributes = [(svar, (List.hd + uril_tl))]; extra = ""} :: (attl (List.tl uril_tl) svar) | [] -> []