X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Fgrafite_parser%2FgrafiteParser.ml;fp=components%2Fgrafite_parser%2FgrafiteParser.ml;h=df18135ac56370767d77c3896855f2f3c62fbba8;hb=f06968e452cca8782e822d98bec9007404abcbbe;hp=c948272ef40ff913d6817275fbfdc4d4b10df460;hpb=94267002fc18aa42a8c09779ad6485f93c3e90fa;p=helm.git

diff --git a/components/grafite_parser/grafiteParser.ml b/components/grafite_parser/grafiteParser.ml
index c948272ef..df18135ac 100644
--- a/components/grafite_parser/grafiteParser.ml
+++ b/components/grafite_parser/grafiteParser.ml
@@ -30,6 +30,8 @@ let set_callback f = out := f
 
 module Ast = CicNotationPt
 
+exception NoInclusionPerformed of string (* full path *)
+
 type 'a localized_option =
    LSome of 'a
  | LNone of GrafiteAst.loc
@@ -41,6 +43,7 @@ type ast_statement =
     GrafiteAst.statement
 
 type statement =
+  ?never_include:bool -> 
   include_paths:string list ->
   LexiconEngine.status ->
     LexiconEngine.status * ast_statement localized_option
@@ -687,17 +690,18 @@ EXTEND
   ];
   statement: [
     [ ex = executable ->
-       fun ~include_paths status -> status,LSome(GrafiteAst.Executable (loc,ex))
+       fun ?(never_include=false) ~include_paths status -> status,LSome(GrafiteAst.Executable (loc,ex))
     | com = comment ->
-       fun ~include_paths status -> status,LSome (GrafiteAst.Comment (loc, com))
+       fun ?(never_include=false) ~include_paths status -> status,LSome (GrafiteAst.Comment (loc, com))
     | (iloc,fname,mode) = include_command ; SYMBOL "."  ->
-       fun ~include_paths status ->
+       fun ?(never_include=false) ~include_paths status ->
 	let _root, buri, fullpath, _rrelpath = 
           Librarian.baseuri_of_script ~include_paths fname 
         in
         let status =
-         LexiconEngine.eval_command status 
-           (LexiconAst.Include (iloc,buri,mode,fullpath))
+         if never_include then raise (NoInclusionPerformed fullpath)
+         else LexiconEngine.eval_command status 
+                (LexiconAst.Include (iloc,buri,mode,fullpath))
         in
 	 !out fname;
          status,
@@ -706,7 +710,7 @@ EXTEND
            (loc,GrafiteAst.Command
             (loc,GrafiteAst.Include (iloc,buri))))
     | scom = lexicon_command ; SYMBOL "." ->
-       fun ~include_paths status ->
+       fun ?(never_include=false) ~include_paths status ->
 	let status = LexiconEngine.eval_command status scom in
          status,LNone loc
     | EOI -> raise End_of_file