X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmetadata%2Fextractor%2Fmeta_lex_ind.l;h=9f474bf85c4a68fad7f21c881901a42b2ba17f9f;hb=97c2d258a5c524eb5c4b85208899d80751a2c82f;hp=2f844f9b6b60f8120e5d8bffce76c065d3729088;hpb=407c75f92f1a641dc49243209cd246f6affd924d;p=helm.git

diff --git a/helm/metadata/extractor/meta_lex_ind.l b/helm/metadata/extractor/meta_lex_ind.l
index 2f844f9b6..9f474bf85 100644
--- a/helm/metadata/extractor/meta_lex_ind.l
+++ b/helm/metadata/extractor/meta_lex_ind.l
@@ -83,6 +83,7 @@ char                    *uri;
 char                    *tmp;
 char                    *source_uri; 
 char                    *source_uri_prefix;
+int                     waiting_for_name = 0;
 
 void search(char *uri, int first_child, int position, int depth);
 %}
@@ -94,6 +95,7 @@ void search(char *uri, int first_child, int position, int depth);
 uri                     [^"]+
 digits                  [0-9]+ 
 value                   [^"]+                  
+id                      [a-zA-Z]([-_'a-zA-Z0-9])*
 
  /***************************************************************/
  /* 4. Rules.							*/
@@ -113,14 +115,17 @@ value                   [^"]+
                      constructor=0;
                      position = INTYPE;
                      first_child = HERE;
-                   }
+                     waiting_for_name = 1;
 
-"</arity>"         { tmp = (char *)malloc(sizeof('a')*128);
+                     tmp = (char *)malloc(sizeof('a')*128);
                      strcpy(source_uri,source_uri_prefix);
                      sprintf(tmp,"#xpointer(1/%d)", inductive_type);
                      strcat(source_uri,tmp);
                      /* fprintf(stderr,"cinque"); */
                      free(tmp);
+                   }
+
+"</arity>"         {
                      print_all(source_uri);
                      /* print_file(); */
                    }
@@ -132,14 +137,16 @@ value                   [^"]+
                      constructor++;
                      position = INTYPE;
                      first_child = HERE;
-                   }
+                     waiting_for_name = 1;
 
-"</Constructor>"   { tmp = (char *)malloc(sizeof('a')*128);
+                     tmp = (char *)malloc(sizeof('a')*128);
                      strcpy(source_uri,source_uri_prefix);
                      sprintf(tmp,"#xpointer(1/%d/%d)",inductive_type,constructor);
                      strcat(source_uri,tmp);
                      free(tmp);
-                     print_all(source_uri);
+                   }
+
+"</Constructor>"   { print_all(source_uri);
                      /* print_file(); */
                    }
 
@@ -149,7 +156,8 @@ value                   [^"]+
                        position = MAINHYP;
                     else if (position == MAINHYP)
                         { position = INHYP;
-                          no_open_source++;};
+                          no_open_source = 1;}
+                    else if (position == INHYP) no_open_source++;
                    }
 
 "</decl>"          |
@@ -294,6 +302,16 @@ value                   [^"]+
                             first_child = AFTER;};
                    } 
 
+"name=\""{id} {
+                 if (waiting_for_name == 1) {
+                    waiting_for_name = 0;
+                    strsep(&yytext,&sep);
+                    tmp=(char *)malloc((sizeof(sep)*(strlen(yytext)+1)));
+                    strcpy(tmp,yytext);
+                    print_name(tmp,source_uri);
+                    free(tmp);
+                 }
+              } 
 
 
 %%