X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Flambda-delta%2Ftext%2FtxtParser.mly;h=694e308913178f912d176590ec0c1904bcb1fdc0;hb=a3b9fc77770f42070632bcb575546678025e09b2;hp=05af001e74fe8fd2a56f149f873062c74a427830;hpb=4c157ac5c58f34fffc98289c2d2e71032d584a83;p=helm.git

diff --git a/helm/software/lambda-delta/text/txtParser.mly b/helm/software/lambda-delta/text/txtParser.mly
index 05af001e7..694e30891 100644
--- a/helm/software/lambda-delta/text/txtParser.mly
+++ b/helm/software/lambda-delta/text/txtParser.mly
@@ -24,19 +24,18 @@
  */
 
 %{
+   module O = Options
    module T = Txt
    
-   let debug = false
-
-   let _ = Parsing.set_trace debug
+   let _ = Parsing.set_trace !O.debug_parser
 %}
    %token <int> IX
    %token <string> ID STR
    %token OP CP OB CB OA CA FS CN CM EQ STAR HASH PLUS TE WTO STO 
-   %token REQUIRE GRAPH DECL AX DEF TH OPEN CLOSE SORTS EOF
+   %token GRAPH DECL AX DEF TH GEN REQ OPEN CLOSE SORTS EOF
 
    %start entry
-   %type <Txt.command option * bool> entry
+   %type <Txt.command option> entry
 
    %nonassoc CP CB CA
    %right WTO STO
@@ -123,30 +122,32 @@
       | TH   { T.Th  }
    ;
    xentity:
-      | REQUIRE ids
-         { Some (T.Require $2)                           }
       | GRAPH ID
-         { Some (T.Graph $2)                             }
+         { T.Graph $2                             }
       | decl comment ID CN term
-         { Some (T.Entity ($1, $3, $2, $5))              }
+         { T.Entity ($1, $3, $2, $5)              }
       | def comment ID EQ term
-         { Some (T.Entity ($1, $3, $2, $5))              }
+         { T.Entity ($1, $3, $2, $5)              }
       | def comment ID EQ term CN term
-         { Some (T.Entity ($1, $3, $2, T.Cast ($7, $5))) }
+         { T.Entity ($1, $3, $2, T.Cast ($7, $5)) }
+      | GEN term
+         { T.Generate [$2]                        }
+      | GEN terms
+         { T.Generate $2                          }      
+      | REQ ids
+         { T.Require $2                           }
       | OPEN ID                           
-         { Some (T.Section (Some $2))                    }
+         { T.Section (Some $2)                    }
       | CLOSE                             
-         { Some (T.Section None)                         }
+         { T.Section None                         }
       | SORTS sorts
-         { Some (T.Sorts $2)                             }
-      | EOF                               
-         { None                                          }
+         { T.Sorts $2                             }
    ;
    start: 
-      | GRAPH {} | decl {} | def {} 
-      | REQUIRE {} | OPEN {} | CLOSE {} | SORTS {} | EOF {}
+      | GRAPH {} | decl {} | def {} | GEN {} |
+      | REQ {} | OPEN {} | CLOSE {} | SORTS {} | EOF {}
    ;
    entry:
-      | xentity       { $1, false }
-      | xentity start { $1, true  }
+      | xentity start { Some $1 }
+      | EOF           { None    }
    ;