From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Thu, 18 Jun 2009 14:46:17 +0000 (+0000)
Subject: callbacks were taking in input a status bu were not using them.
X-Git-Tag: make_still_working~3848
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=e4753fc1a4dbc9a6d2144383d805ec626fa93070;p=helm.git

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 ea74231ad..688e21b8a 100644
--- 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 08015d8dd..d657e4975 100644
--- 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 b3b95325a..baac2409c 100644
--- 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 190d7bf6d..f4e143981 100644
--- 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