]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/lambda-delta/common/entity.ml
txtLexer: bug fix in parsing the string tokens
[helm.git] / helm / software / lambda-delta / common / entity.ml
index de06f2924717613014f29960bc3af294526636de..e32b347a84e70589a092138422a0f59dd965d956 100644 (file)
@@ -13,8 +13,11 @@ module O = Options
 
 type uri = NUri.uri
 type id = Aut.id
+type name = id * bool (* token, real? *)
 
-type attr = Name of id * bool (* name, real? *)
+type names = name list
+
+type attr = Name of name      (* name *)
           | Apix of int       (* additional position index *)
          | Mark of int       (* node marker *)
          | Meta of string    (* metaliguistic annotation *)
@@ -88,6 +91,11 @@ let rec priv err f = function
    | _ :: tl   -> priv err f tl
    | []        -> err ()
 
+let rec meta err f = function
+   | Meta s :: _ -> f s
+   | _ :: tl     -> meta err f tl
+   | []          -> err ()
+
 let resolve err f name a =
    let rec aux i = function
       | Name (n, true) :: _ when n = name -> f i
@@ -96,6 +104,11 @@ let resolve err f name a =
    in
    aux 0 a
 
+let rec rev_append_names ns = function
+   | []           -> ns
+   | Name n :: tl -> rev_append_names (n :: ns) tl
+   | _ :: tl      -> rev_append_names ns tl
+
 let xlate f xlate_term = function
    | a, uri, Abst t ->
       let f t = f (a, uri, Abst t) in xlate_term f t
@@ -111,3 +124,4 @@ let initial_status () = {
 let refresh_status st = {st with
    si = !O.si; expand = !O.expand
 }
+