From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Mon, 12 Feb 2007 22:53:46 +0000 (+0000)
Subject: LexiconAstPp: fixed syntax for include
X-Git-Tag: 0.4.95@7852~597
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=9642ec8492f2ef54e280e27a40c2936a02c252f9;p=helm.git

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 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