X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Flambda-delta%2Fsrc%2Ftext%2FtxtParser.mly;h=2c9abe0793115c8991eb3614236d16860348ddbd;hb=fa5cd121c672589afc0ac8ddd5d184897a38c7c6;hp=1eae31980929ea9ab3295fc7ac972a027a8ef0a1;hpb=5280ec9794de75e63ffc01bddf1756ebcca02be0;p=helm.git

diff --git a/helm/software/lambda-delta/src/text/txtParser.mly b/helm/software/lambda-delta/src/text/txtParser.mly
index 1eae31980..2c9abe079 100644
--- a/helm/software/lambda-delta/src/text/txtParser.mly
+++ b/helm/software/lambda-delta/src/text/txtParser.mly
@@ -33,7 +33,7 @@
    %token <int> IX
    %token <string> ID STR
    %token OP CP OB CB OA CA FS CN CM EQ STAR HASH PLUS TE WTO STO CT
-   %token GRAPH DECL AX CONG DEF TH GEN REQ OPEN CLOSE SORTS EOF
+   %token GRAPH MAIN DECL AX CONG DEF TH GEN REQ OPEN CLOSE SORTS EOF
 
    %start entry
    %type <Txt.command option> entry
@@ -49,9 +49,14 @@
       |    {}
       | FS {}
    ;
+   main:
+      |      { false }
+      | MAIN { true  }
+   ;
    comment:
-      |     { "" }
-      | STR { $1 }
+      |         { "", "" }
+      | STR     { "", $1 }
+      | STR STR { $1, $2 }
    ;
    ids:
       | ID        { [$1]     }
@@ -129,25 +134,25 @@
    ;
    xentity:
       | GRAPH ID
-         { T.Graph $2                                 }
-      | decl level comment ID CN term
-         { T.Entity ($1, $2, $4, $3, $6)              }
-      | def level comment ID EQ term
-         { T.Entity ($1, $2, $4, $3, $6)              }
-      | def level comment ID EQ term CN term
-         { T.Entity ($1, $2, $4, $3, T.Cast ($8, $6)) }
+         { T.Graph $2                                     }
+      | main decl level comment ID CN term
+         { T.Entity ($1, $2, $3, $5, $4, $7)              }
+      | main def level comment ID EQ term
+         { T.Entity ($1, $2, $3, $5, $4, $7)              }
+      | main def level comment ID EQ term CN term
+         { T.Entity ($1, $2, $3, $5, $4, T.Cast ($9, $7)) }
       | GEN term
-         { T.Generate [$2]                            }
+         { T.Generate [$2]                                }
       | GEN terms
-         { T.Generate $2                              }      
+         { T.Generate $2                                  }      
       | REQ ids
-         { T.Require $2                               }
+         { T.Require $2                                   }
       | OPEN ID                           
-         { T.Section (Some $2)                        }
+         { T.Section (Some $2)                            }
       | CLOSE                             
-         { T.Section None                             }
+         { T.Section None                                 }
       | SORTS sorts
-         { T.Sorts $2                                 }
+         { T.Sorts $2                                     }
    ;
    start: 
       | GRAPH {} | decl {} | def {} | GEN {} |