]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/metadata/extractor/meta_lex_ind.l
The metadata extractor now generates also
[helm.git] / helm / metadata / extractor / meta_lex_ind.l
index 2f844f9b6b60f8120e5d8bffce76c065d3729088..271bd7db4aa244120c04c30837818f5b5b771ee3 100644 (file)
@@ -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-Z])+
 
  /***************************************************************/
  /* 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(); */
                    }
 
@@ -294,6 +301,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);
+                 }
+              } 
 
 
 %%