X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Flambda-delta%2Fautomath%2FautParser.mly;h=ed5da5a647a7c8ccf64a0555d09d2e707b0da658;hb=e17c4da82bd52712f03c112660c52eb8f1783843;hp=c8e836e79809b7a82f9b397e472064573e100c28;hpb=2b821e608cc1fceebc13e85867a244fe02edf71e;p=helm.git

diff --git a/helm/software/lambda-delta/automath/autParser.mly b/helm/software/lambda-delta/automath/autParser.mly
index c8e836e79..ed5da5a64 100644
--- a/helm/software/lambda-delta/automath/autParser.mly
+++ b/helm/software/lambda-delta/automath/autParser.mly
@@ -25,14 +25,18 @@
 
 %{
    module A = Aut
+
+   let debug = false
+
+   let _ = Parsing.set_trace debug
 %}
    %token <int> NUM
    %token <string> IDENT
    %token EOF MINUS PLUS TIMES AT FS CN CM SC QT TD OP CP OB CB OA CA
    %token TYPE PROP DEF EB E PN EXIT
     
-   %start book
-   %type <Aut.item list> book   
+   %start entry
+   %type <Aut.command option * bool> entry   
 %%
    path: MINUS {} | FS {} ;
    oftype: CN {} | CM {} ;
@@ -71,25 +75,28 @@
       | term          { [$1]     }
       | term CM terms { $1 :: $3 }
    ;
-   item:
-      | PLUS IDENT                    { A.Section (Some (true, $2))  }
-      | PLUS TIMES IDENT              { A.Section (Some (false, $3)) }
-      | MINUS IDENT                   { A.Section None               }
-      | EXIT                          { A.Section None               }
-      | star                          { A.Context None               }
-      | qid star                      { A.Context (Some $1)          }
-      | IDENT DEF EB sc term          { A.Block ($1, $5)             }
-      | IDENT sc term DEF EB          { A.Block ($1, $3)             }
-      | OB IDENT oftype term CB       { A.Block ($2, $4)             }
-      | IDENT DEF PN sc term          { A.Decl ($1, $5)              }
-      | IDENT sc term DEF PN          { A.Decl ($1, $3)              }
-      | IDENT DEF expand term sc term { A.Def ($1, $6, $3, $4)       }
-      | IDENT sc term DEF expand term { A.Def ($1, $3, $5, $6)       }
-   ;
-   items:
-      |            { []       }
-      | item items { $1 :: $2 }
-   ;
-   book:
-      | items eof { $1 }
+   
+   start:
+      | PLUS {} | MINUS {} | EXIT {} | eof {}
+      | star {} | IDENT {} | OB {} 
+   ; 
+   entity:
+      | PLUS IDENT                    { Some (A.Section (Some (true, $2)))  }
+      | PLUS TIMES IDENT              { Some (A.Section (Some (false, $3))) }
+      | MINUS IDENT                   { Some (A.Section None)               }
+      | EXIT                          { Some (A.Section None)               }
+      | star                          { Some (A.Context None)               }
+      | qid star                      { Some (A.Context (Some $1))          }
+      | IDENT DEF EB sc term          { Some (A.Block ($1, $5))             }
+      | IDENT sc term DEF EB          { Some (A.Block ($1, $3))             }
+      | OB IDENT oftype term CB       { Some (A.Block ($2, $4))             }
+      | IDENT DEF PN sc term          { Some (A.Decl ($1, $5))              }
+      | IDENT sc term DEF PN          { Some (A.Decl ($1, $3))              }
+      | IDENT DEF expand term sc term { Some (A.Def ($1, $6, $3, $4))       }
+      | IDENT sc term DEF expand term { Some (A.Def ($1, $3, $5, $6))       }
+      | eof                           { None                                }
    ;
+   entry:
+      | entity       { $1, false }
+      | entity start { $1, true }
+