X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fgrafite_parser%2FgrafiteParser.ml;h=e83152226f257cb21132fbb3abee6b0f3c271ae7;hb=f7f2a793b445a052138cd3df377a9e417f6e37c4;hp=e480efd34f1cbfbc77656716ee0f4f9ff0b59f66;hpb=55b82bd235d82ff7f0a40d980effe1efde1f5073;p=helm.git

diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml
index e480efd34..e83152226 100644
--- a/helm/software/components/grafite_parser/grafiteParser.ml
+++ b/helm/software/components/grafite_parser/grafiteParser.ml
@@ -31,15 +31,17 @@ module Ast = CicNotationPt
 
 type 'a localized_option =
    LSome of 'a
- | LNone of Token.flocation
+ | LNone of GrafiteAst.loc
 
-type statement =
- include_paths:string list ->
- LexiconEngine.status ->
-  LexiconEngine.status *
+type ast_statement =
   (CicNotationPt.term, CicNotationPt.term,
    CicNotationPt.term GrafiteAst.reduction, CicNotationPt.obj, string)
-    GrafiteAst.statement localized_option
+    GrafiteAst.statement
+
+type statement =
+  include_paths:string list ->
+  LexiconEngine.status ->
+    LexiconEngine.status * ast_statement localized_option
 
 let grammar = CicNotationParser.level2_ast_grammar
 
@@ -140,16 +142,12 @@ EXTEND
         GrafiteAst.ClearBody (loc,id)
     | IDENT "change"; what = pattern_spec; "with"; t = tactic_term ->
         GrafiteAst.Change (loc, what, t)
-    | IDENT "compare"; t = tactic_term ->
-        GrafiteAst.Compare (loc,t)
     | IDENT "constructor"; n = int ->
         GrafiteAst.Constructor (loc, n)
     | IDENT "contradiction" ->
         GrafiteAst.Contradiction loc
     | IDENT "cut"; t = tactic_term; ident = OPT [ "as"; id = IDENT -> id] ->
         GrafiteAst.Cut (loc, ident, t)
-    | IDENT "decide"; IDENT "equality" ->
-        GrafiteAst.DecideEquality loc
     | IDENT "decompose"; types = OPT ident_list0; what = IDENT;
       (num, idents) = intros_spec ->
         let types = match types with None -> [] | Some types -> types in
@@ -343,7 +341,7 @@ EXTEND
         GrafiteAst.WMatch (loc,t)
     | [ IDENT "whelp"; IDENT "instance" ] ; t = term -> 
         GrafiteAst.WInstance (loc,t)
-    | [ IDENT "whelp"; IDENT "locate" ] ; id = IDENT -> 
+    | [ IDENT "whelp"; IDENT "locate" ] ; id = QSTRING -> 
         GrafiteAst.WLocate (loc,id)
     | [ IDENT "whelp"; IDENT "elim" ] ; t = term ->
         GrafiteAst.WElim (loc, t)
@@ -451,7 +449,10 @@ EXTEND
   ];
   
   include_command: [ [
-      IDENT "include" ; path = QSTRING -> loc,path
+      IDENT "include" ; path = QSTRING -> 
+        loc,path,LexiconAst.WithPreferences
+    | IDENT "include'" ; path = QSTRING -> 
+        loc,path,LexiconAst.WithoutPreferences
    ]];
 
   grafite_command: [ [
@@ -530,11 +531,11 @@ EXTEND
        fun ~include_paths status -> status,LSome(GrafiteAst.Executable (loc,ex))
     | com = comment ->
        fun ~include_paths status -> status,LSome (GrafiteAst.Comment (loc, com))
-    | (iloc,fname) = include_command ; SYMBOL "."  ->
+    | (iloc,fname,mode) = include_command ; SYMBOL "."  ->
        fun ~include_paths status ->
         let path = DependenciesParser.baseuri_of_script ~include_paths fname in
         let status =
-         LexiconEngine.eval_command status (LexiconAst.Include (iloc,path))
+         LexiconEngine.eval_command status (LexiconAst.Include (iloc,path,mode))
         in
          status,
           LSome