From 9642ec8492f2ef54e280e27a40c2936a02c252f9 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Mon, 12 Feb 2007 22:53:46 +0000 Subject: [PATCH] LexiconAstPp: fixed syntax for include TermContentPres: fixed syntax for letin lexiconEngine: moved callback from grafiteParser matitac: -dump patched --- components/content_pres/termContentPres.ml | 4 ++-- components/grafite_parser/grafiteParser.ml | 5 ----- components/grafite_parser/grafiteParser.mli | 3 --- components/lexicon/lexiconAstPp.ml | 4 ++-- components/lexicon/lexiconEngine.ml | 5 +++++ components/lexicon/lexiconEngine.mli | 2 ++ matita/matitac.ml | 11 +++++++---- 7 files changed, 18 insertions(+), 16 deletions(-) diff --git a/components/content_pres/termContentPres.ml b/components/content_pres/termContentPres.ml index a8bfe1147..9f720e33b 100644 --- a/components/content_pres/termContentPres.ml +++ b/components/content_pres/termContentPres.ml @@ -199,9 +199,9 @@ let pp_ast0 t k = add_level_info Ast.let_in_prec Ast.let_in_assoc (hvbox false true [ hvbox false true [ - keyword "let"; + keyword "let"; space; hvbox false true [ - aux_var var; builtin_symbol "\\def"; break; top_pos (k s) ]; + aux_var var; space; builtin_symbol "\\def"; break; top_pos (k s) ]; break; keyword "in" ]; break; k t ]) diff --git a/components/grafite_parser/grafiteParser.ml b/components/grafite_parser/grafiteParser.ml index f3dd386a9..64c10b9b4 100644 --- a/components/grafite_parser/grafiteParser.ml +++ b/components/grafite_parser/grafiteParser.ml @@ -60,10 +60,6 @@ type by_continuation = | BYC_letsuchthat of string * CicNotationPt.term * string * CicNotationPt.term | BYC_wehaveand of string * CicNotationPt.term * string * CicNotationPt.term -let out = ref ignore - -let set_callback f = out := f - EXTEND GLOBAL: term statement; constructor: [ [ name = IDENT; SYMBOL ":"; typ = term -> (name, typ) ] ]; @@ -678,7 +674,6 @@ EXTEND (loc,GrafiteAst.Include (iloc,buri)))) | scom = lexicon_command ; SYMBOL "." -> fun ~include_paths status -> - !out scom; let status = LexiconEngine.eval_command status scom in status,LNone loc | EOI -> raise End_of_file diff --git a/components/grafite_parser/grafiteParser.mli b/components/grafite_parser/grafiteParser.mli index f38f0e5dc..6d941d5db 100644 --- a/components/grafite_parser/grafiteParser.mli +++ b/components/grafite_parser/grafiteParser.mli @@ -38,9 +38,6 @@ type statement = LexiconEngine.status -> LexiconEngine.status * ast_statement localized_option -(* this callback is called on every lexicon command *) -val set_callback: (LexiconAst.command -> unit) -> unit - val parse_statement: Ulexing.lexbuf -> statement (** @raise End_of_file *) val statement: statement Grammar.Entry.e diff --git a/components/lexicon/lexiconAstPp.ml b/components/lexicon/lexiconAstPp.ml index 0b2c94639..ad317bec7 100644 --- a/components/lexicon/lexiconAstPp.ml +++ b/components/lexicon/lexiconAstPp.ml @@ -79,9 +79,9 @@ let pp_notation dir_opt l1_pattern assoc prec l2_pattern = let pp_command = function | Include (_,_,mode,path) -> (* not precise, since path is absolute *) if mode = WithPreferences then - "include " ^ path + "include \"" ^ path ^ "\".\n" else - "include' " ^ path + "include' \"" ^ path ^ "\".\n" | Alias (_,s) -> pp_alias s | Interpretation (_, dsc, (symbol, arg_patterns), cic_appl_pattern) -> pp_interpretation dsc symbol arg_patterns cic_appl_pattern diff --git a/components/lexicon/lexiconEngine.ml b/components/lexicon/lexiconEngine.ml index 1e1fe61c0..a0792d228 100644 --- a/components/lexicon/lexiconEngine.ml +++ b/components/lexicon/lexiconEngine.ml @@ -25,6 +25,10 @@ (* $Id$ *) +let out = ref ignore + +let set_callback f = out := f + (* lexicon file name * ma file name *) exception IncludedFileNotCompiled of string * string exception MetadataNotFound of string (* file name *) @@ -112,6 +116,7 @@ let set_proof_aliases mode status new_aliases = let rec eval_command ?(mode=LexiconAst.WithPreferences) status cmd = + !out cmd; let notation_ids' = CicNotation.process_notation cmd in let status = { status with notation_ids = notation_ids' @ status.notation_ids } in diff --git a/components/lexicon/lexiconEngine.mli b/components/lexicon/lexiconEngine.mli index 00201c9fb..eab7e53e7 100644 --- a/components/lexicon/lexiconEngine.mli +++ b/components/lexicon/lexiconEngine.mli @@ -42,3 +42,5 @@ val set_proof_aliases: (DisambiguateTypes.Environment.key * DisambiguateTypes.codomain_item) list -> status +(* this callback is called on every lexicon command *) +val set_callback: (LexiconAst.command -> unit) -> unit diff --git a/matita/matitac.ml b/matita/matitac.ml index be6546e8d..34e0639e3 100644 --- a/matita/matitac.ml +++ b/matita/matitac.ml @@ -26,6 +26,7 @@ (* $Id$ *) module G = GrafiteAst +module L = LexiconAst (* from transcript *) @@ -63,16 +64,18 @@ let dump f = let path = Filename.concat rt_base_dir "matita.ma.templ" in let lines = 14 in out_preamble och (path, lines); - let grafite_parser_cb ast = - output_string och (LexiconAstPp.pp_command ast) + let lexicon_engine_cb = function + | L.Include _ as ast -> output_string och (LexiconAstPp.pp_command ast) + | _ -> () in let matita_engine_cb = function - | G.Executable (_, G.Macro (_, G.Inline _)) -> () + | G.Executable (_, G.Macro (_, G.Inline _)) + | G.Executable (_, G.Command (_, G.Include _)) -> () | ast -> output_string och (pp_ast_statement ast) in let matitac_lib_cb = output_string och in -(* GrafiteParser.set_callback grafite_parser_cb; *) + LexiconEngine.set_callback lexicon_engine_cb; MatitaEngine.set_callback matita_engine_cb; MatitacLib.set_callback matitac_lib_cb; at_exit atexit -- 2.39.2