callbacks were taking in input a status bu were not using them.

thanks to the new #type for statuses this was a problem, and Obj.magic
was required to fix them. Removed both the dummy parameter and the
unsafe cast

diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml
index ea74231adb46762d2a5c41e7af435b0855a38e62..688e21b8ac1a89b703c2380c4f9b039792219df3 100644 (file)
--- a/helm/software/components/grafite_parser/grafiteParser.ml
+++ b/helm/software/components/grafite_parser/grafiteParser.ml
@@ -51,11 +51,11 @@ type 'status parser_status = {
   statement : #LE.status as 'status statement Grammar.Entry.e;
 }
 
-let grafite_callback = ref (fun _ _ -> ())
-let set_grafite_callback cb = grafite_callback := Obj.magic cb
+let grafite_callback = ref (fun _ -> ())
+let set_grafite_callback cb = grafite_callback := cb
 
-let lexicon_callback = ref (fun _ _ -> ())
-let set_lexicon_callback cb = lexicon_callback := Obj.magic cb
+let lexicon_callback = ref (fun _ -> ())
+let set_lexicon_callback cb = lexicon_callback := cb
 
 let initial_parser () = 
   let grammar = CicNotationParser.level2_ast_grammar () in
@@ -938,19 +938,19 @@ EXTEND
     [ ex = executable ->
        fun ?(never_include=false) ~include_paths status ->
           let stm = G.Executable (loc, ex) in
-          Obj.magic !grafite_callback status stm;
+          !grafite_callback stm;
          status, LSome stm
     | com = comment ->
        fun ?(never_include=false) ~include_paths status -> 
           let stm = G.Comment (loc, com) in
-          Obj.magic !grafite_callback status stm;
+          !grafite_callback stm;
          status, LSome stm
     | (iloc,fname,normal,mode) = include_command ; SYMBOL "."  ->
        fun ?(never_include=false) ~include_paths status ->
          let stm =
             G.Executable (loc, G.Command (loc, G.Include (iloc, normal, fname)))
          in
-          Obj.magic !grafite_callback status stm;
+          !grafite_callback stm;
          let _root, buri, fullpath, _rrelpath = 
             Librarian.baseuri_of_script ~include_paths fname 
           in
@@ -964,7 +964,7 @@ EXTEND
          status, LSome stm
     | scom = lexicon_command ; SYMBOL "." ->
        fun ?(never_include=false) ~include_paths status ->
-          !lexicon_callback status scom;         
+          !lexicon_callback scom;        
          let status = LE.eval_command status scom in
           status, LNone loc
     | EOI -> raise End_of_file

diff --git a/helm/software/components/grafite_parser/grafiteParser.mli b/helm/software/components/grafite_parser/grafiteParser.mli
index 08015d8dd187406adf1e76854f39868222102cc6..d657e49752e2e23ac0e64dfcc2448cf6a12625a7 100644 (file)
--- a/helm/software/components/grafite_parser/grafiteParser.mli
+++ b/helm/software/components/grafite_parser/grafiteParser.mli
@@ -48,11 +48,11 @@ val statement: unit -> #LexiconEngine.status statement Grammar.Entry.e
 
 (* this callback is called before every grafite statement *)
 val set_grafite_callback:
-   (#LexiconEngine.status -> ast_statement -> unit) -> unit 
+   (ast_statement -> unit) -> unit 
 
 (* this callback is called before every lexicon command *)
 val set_lexicon_callback:
-   (#LexiconEngine.status -> LexiconAst.command -> unit) -> unit 
+   (LexiconAst.command -> unit) -> unit 
 
 val push : unit -> unit
 val pop : unit -> unit

diff --git a/helm/software/matita/matitacLib.ml b/helm/software/matita/matitacLib.ml
index b3b95325acc8a66ec7fc7e6c5237538975fb7078..baac2409cf1a3243cd5833ffb7ddd81091bf7061 100644 (file)
--- a/helm/software/matita/matitacLib.ml
+++ b/helm/software/matita/matitacLib.ml
@@ -69,7 +69,7 @@ let dump f =
    let och = open_out f in
    let nl () =  output_string och (pp_statement nl_ast) in
    MatitaMisc.out_preamble och;
-   let grafite_parser_cb status = function
+   let grafite_parser_cb = function
       | G.Executable (_, G.Macro (_, G.Inline (_, uri, params))) ->
          let str =
             ApplyTransformation.txt_of_inline_macro params uri
@@ -81,7 +81,7 @@ let dump f =
       | stm ->
          output_string och (pp_statement stm); nl (); nl ()
    in
-   let lexicon_parser_cb status cmd =
+   let lexicon_parser_cb cmd =
          output_string och (pp_lexicon cmd); nl (); nl ()
    in
    begin fun () ->
@@ -91,8 +91,8 @@ let dump f =
    end, 
    begin fun x ->
       close_out och;
-      GrafiteParser.set_grafite_callback (fun _ _ -> ());
-      GrafiteParser.set_lexicon_callback (fun _ _ -> ());
+      GrafiteParser.set_grafite_callback (fun _ -> ());
+      GrafiteParser.set_lexicon_callback (fun _ -> ());
       Helm_registry.set_bool "matita.moo" true;
       x
    end

diff --git a/helm/software/matita/tests/depends b/helm/software/matita/tests/depends
index 190d7bf6dc2bbb536b5b32fa7cce9680c6d25a6f..f4e143981ab699c411755762954bcf153e7d476d 100644 (file)
--- a/helm/software/matita/tests/depends
+++ b/helm/software/matita/tests/depends
@@ -332,6 +332,7 @@ TPTP/Veloci/LCL115-2.p.ma logic/equality.ma
 absurd.ma coq.ma
 TPTP/Veloci/GRP182-4.p.ma logic/equality.ma
 destruct.ma datatypes/constructors.ma logic/equality.ma nat/nat.ma
+foproof.ma ng_pts.ma
 TPTP/Veloci/COL064-5.p.ma logic/equality.ma
 TPTP/Veloci/GRP513-1.p.ma logic/equality.ma
 TPTP/Veloci/LAT033-1.p.ma logic/equality.ma