From e4753fc1a4dbc9a6d2144383d805ec626fa93070 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 18 Jun 2009 14:46:17 +0000 Subject: [PATCH] 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 --- .../components/grafite_parser/grafiteParser.ml | 16 ++++++++-------- .../components/grafite_parser/grafiteParser.mli | 4 ++-- helm/software/matita/matitacLib.ml | 8 ++++---- helm/software/matita/tests/depends | 1 + 4 files changed, 15 insertions(+), 14 deletions(-) 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 -- 2.39.2