LexiconAstPp: fixed syntax for include

TermContentPres: fixed syntax for letin
lexiconEngine: moved callback from grafiteParser
matitac: -dump patched

diff --git a/components/content_pres/termContentPres.ml b/components/content_pres/termContentPres.ml
index a8bfe114746f5c9d79968d7c96141de6d8f27646..9f720e33b9a29740d414f6b5a0cd0d793ae0f2ef 100644 (file)
--- 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 f3dd386a91540b15c729dbf22a0b4c7c25fcaf4a..64c10b9b47e575db35b37981aa79ffc15c95d3b8 100644 (file)
--- 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 f38f0e5dc3e4dde8a76ee9e95c5b5a141c94ad03..6d941d5db4286fce0156b700927592bdcfaf58a7 100644 (file)
--- 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 0b2c9463936671edcb78b812dddeef60760986df..ad317bec77ba62f39c677a20c2d265ba8df93594 100644 (file)
--- 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 1e1fe61c05147eef1dd8df67231df4f18ee3b7b1..a0792d2281fd09bfc4ecf2fa0d05beb7ddf23327 100644 (file)
--- 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 00201c9fbf5147f43e3e04565607bf1b01298447..eab7e53e75af3e059e60b8bf0c2a5df9c4aebde9 100644 (file)
--- 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 be6546e8d237437e803f29558289be92929e1c8c..34e0639e3aa62ebfd422fb7a02c7a5ac7e5d1d6b 100644 (file)
--- 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