]> matita.cs.unibo.it Git - helm.git/blobdiff - components/grafite_parser/grafiteParser.ml
procedural: bug fixes
[helm.git] / components / grafite_parser / grafiteParser.ml
index 7b515472d2ef386385855a7d78abbf6543513618..63df8ab7f37d1b6a208e89bd16b599ec67da2512 100644 (file)
@@ -25,7 +25,8 @@
 
 (* $Id$ *)
 
-open Printf
+let out = ref ignore
+let set_callback f = out := f
 
 module Ast = CicNotationPt
 
@@ -460,10 +461,10 @@ EXTEND
           LexiconAst.Ident_alias (id, uri)
         else 
           raise
-           (HExtlib.Localized (loc, CicNotationParser.Parse_error (sprintf "Not a valid uri: %s" uri)))
+           (HExtlib.Localized (loc, CicNotationParser.Parse_error (Printf.sprintf "Not a valid uri: %s" uri)))
       else
         raise (HExtlib.Localized (loc, CicNotationParser.Parse_error (
-          sprintf "Not a valid identifier: %s" id)))
+          Printf.sprintf "Not a valid identifier: %s" id)))
     | IDENT "symbol"; symbol = QSTRING;
       instance = OPT [ LPAREN; IDENT "instance"; n = int; RPAREN -> n ];
       SYMBOL "="; dsc = QSTRING ->
@@ -501,11 +502,11 @@ EXTEND
       IDENT "for";
       p2 = 
         [ blob = UNPARSED_AST ->
-            add_raw_attribute ~text:(sprintf "@{%s}" blob)
+            add_raw_attribute ~text:(Printf.sprintf "@{%s}" blob)
               (CicNotationParser.parse_level2_ast
                 (Ulexing.from_utf8_string blob))
         | blob = UNPARSED_META ->
-            add_raw_attribute ~text:(sprintf "${%s}" blob)
+            add_raw_attribute ~text:(Printf.sprintf "${%s}" blob)
               (CicNotationParser.parse_level2_meta
                 (Ulexing.from_utf8_string blob))
         ] ->
@@ -661,13 +662,14 @@ EXTEND
        fun ~include_paths status -> status,LSome (GrafiteAst.Comment (loc, com))
     | (iloc,fname,mode) = include_command ; SYMBOL "."  ->
        fun ~include_paths status ->
-        let buri, fullpath = 
+       let buri, fullpath = 
           DependenciesParser.baseuri_of_script ~include_paths fname 
         in
         let status =
          LexiconEngine.eval_command status 
            (LexiconAst.Include (iloc,buri,mode,fullpath))
         in
+        !out fname;
          status,
           LSome
           (GrafiteAst.Executable