MaTeX

- bug fixed in rendering of application: the head was not rendered sometimes
- we can generate the list of the produced TeX files
- TeX item for comments was missing
test
- bug fixed in matex.sty: pages were not ejected properly causig memory overflow
- now includes the whole \lambda\delta version 1 (737 pages for now)
- object numbering is now supported

diff --git a/matita/components/binaries/matex/Makefile b/matita/components/binaries/matex/Makefile
index 42cf1c1817281cb2701a31a36db564b751921087..342ba027d372949133d921854d3513db1deda788 100644 (file)
--- a/matita/components/binaries/matex/Makefile
+++ b/matita/components/binaries/matex/Makefile
@@ -5,14 +5,20 @@ REQUIRES = helm-ng_library
 
 include ../Makefile.common
 
+PROBE    = ../probe/probe.native
 REGISTRY = $(RT_BASE_DIR)/matita.conf.xml
+OBJS     = Make.objs
 
-OBJS = cic:/matita/lambdadelta/basic_1/pr0/pr0/pr0_confluence.con\
-       cic:/matita/lambdadelta/basic_1/pr0/defs/pr0_ind.con\
-       cic:/matita/lambdadelta/basic_1/pr0/defs/pr0.ind
+BASEURI = cic:/matita/lambdadelta/basic_1/
 
-test:
-       @echo MaTeX: $(OBJS:cic:/matita/lambdadelta/basic_1/pr0/%=%)
-       $(H)./matex.native -O test -t -p $(REGISTRY) $(OBJS)
+test: test/$(OBJS)
+
+$(OBJS):
+       @echo probe: $(BASEURI)
+       $(H)$(PROBE) $(REGISTRY) -g $(BASEURI) -os > $@
+
+test/$(OBJS): $(OBJS) ./matex.native
+       @echo MaTeX: processing $(OBJS)
+       $(H)./matex.native -O test -l $(OBJS) -t -p $(REGISTRY) `cat $<`
 
 .PHONY: test

diff --git a/matita/components/binaries/matex/TeX.ml b/matita/components/binaries/matex/TeX.ml
index 01ab717f1f7898c2beaddc9a686cd0ce62a0feeb..ccf2ffa6a6cdcdb7bfb022297993b3ea4dc5bf27 100644 (file)
--- a/matita/components/binaries/matex/TeX.ml
+++ b/matita/components/binaries/matex/TeX.ml
@@ -17,6 +17,7 @@ type item = Free  of string  (* free text *)
           | Text  of string  (* quoted text *)
           | Macro of string  (* macro *)
           | Group of text    (* group *)
+          | Note  of string  (* comment *)
          
 and text = item list         (* structured text *)
 

diff --git a/matita/components/binaries/matex/TeXOutput.ml b/matita/components/binaries/matex/TeXOutput.ml
index f92101c30738e4d5b4635d57489d8e833d4ad3da..f18b2b44abbf787f3d637bfa11b2ac9aa8d75e2f 100644 (file)
--- a/matita/components/binaries/matex/TeXOutput.ml
+++ b/matita/components/binaries/matex/TeXOutput.ml
@@ -32,6 +32,7 @@ let rec out_item och = function
    | T.Text s  -> P.fprintf och "%s" (X.fold_string quote "" s)
    | T.Macro s -> P.fprintf och "\\%s%%\n" s
    | T.Group t -> P.fprintf och "{%a}%%\n" out_text t
+   | T.Note s  -> P.fprintf och "%% %s\n" s
 
 (* interface functions ******************************************************)
 

diff --git a/matita/components/binaries/matex/engine.ml b/matita/components/binaries/matex/engine.ml
index 5a1a3e3454a6b05e3a4f59878056f3d5afeeb8aa..165986b473e9a115fc0d6068ae4255f6e00889e5 100644 (file)
--- a/matita/components/binaries/matex/engine.ml
+++ b/matita/components/binaries/matex/engine.ml
@@ -141,8 +141,8 @@ let rec proc_proof st ris c t = match t with
       let is_w = proc_term [] c w in
       let ris = mk_open st ris in
       proc_proof (next st) (mk_dec "PRIM" is_w s ris) (K.add_dec s w c) t
-   | C.Appl ts              ->
-      let rts = X.rev_neg_filter (A.not_prop2 c) [] ts in
+   | C.Appl (t0 :: ts)     ->
+      let rts = X.rev_neg_filter (A.not_prop2 c) [t0] ts in
       let ris = T.Macro "STEP" :: mk_inferred st c t ris in
       let tts = L.rev_map (proc_term [] c) rts in
       mk_exit st (T.rev_mk_args tts ris)
@@ -174,17 +174,24 @@ let proc_proof rs c t = try proc_proof (init ()) rs c t with
 
 (* top level processing *)
 
+let note = T.Note "This file was automatically generated by MaTeX: do not edit"
+
 let proc_item item s t =
    let is = [T.Macro "end"; T.arg item] in
-   T.Macro "begin" :: T.arg item :: T.arg s :: T.free s :: proc_term is [] t
+   note :: T.Macro "begin" :: T.arg item :: T.arg s :: T.free s :: proc_term is [] t
 
 let proc_top_proof s t =
    let tt = A.process_top_term s t in (* anticipation *)
-   let ris = [T.free s; T.arg s; T.arg "proof"; T.Macro "begin"] in
+   let ris = [T.free s; T.arg s; T.arg "proof"; T.Macro "begin"; note] in
    L.rev (T.arg "proof" :: T.Macro "end" :: proc_proof ris [] tt)
 
 let open_out_tex s =
-   open_out (F.concat !G.out_dir (s ^ T.file_ext))
+   let fname = s ^ T.file_ext in
+   begin match !G.list_och with
+      | None     -> ()
+      | Some och -> P.fprintf och "%s\n" fname
+   end;
+   open_out (F.concat !G.out_dir fname)
 
 let proc_pair s ss u = function
    | None   -> 

diff --git a/matita/components/binaries/matex/matex.ml b/matita/components/binaries/matex/matex.ml
index 59460ce4a116239ce660e4f19387b9c8674b768b..7e296aa0317835233ff38fe9bf6263a1cf30d8c4 100644 (file)
--- a/matita/components/binaries/matex/matex.ml
+++ b/matita/components/binaries/matex/matex.ml
@@ -24,6 +24,7 @@ module K = Kernel
 
 let help_O = "<dir> Set this output directory"
 let help_X = " Clear configuration and options"
+let help_l = "<file> Output the list of generated files in this file"
 let help_p = " omit types (default: no)"
 let help_t = " Test anticipation (default: no)"
 
@@ -47,6 +48,10 @@ let no_init () =
 let malformed s =
    failwith ("MaTeX: main: malformed argument: " ^ s)
 
+let set_list fname =
+   let file = F.concat !G.out_dir fname in
+   G.close_list (); G.list_och := Some (open_out file)
+
 let process s =
    if is_registry s then init s
    else if !G.no_init then no_init ()
@@ -54,12 +59,15 @@ let process s =
    else malformed s
 
 let main =
-try
+begin try
    A.parse [
       "-O", A.String ((:=) G.out_dir), help_O;
       "-X", A.Unit G.clear, help_X;
+      "-l", A.String set_list, help_l;
       "-p", A.Set G.no_types, help_p;
       "-t", A.Set G.test, help_t;
    ] process help
 with
    | X.Error s -> X.log s
+end;
+G.close_list ()

diff --git a/matita/components/binaries/matex/options.ml b/matita/components/binaries/matex/options.ml
index 14dc4e2c9af388932608150f1fab059a9d5e7ee8..ba1f39849e0138b2c9ca6f0880a9facfd520d814 100644 (file)
--- a/matita/components/binaries/matex/options.ml
+++ b/matita/components/binaries/matex/options.ml
@@ -26,6 +26,8 @@ let default_test = false
 
 let default_no_types = false
 
+let default_list_och = None
+
 (* interface ****************************************************************)
 
 let status = new P.status
@@ -40,10 +42,17 @@ let test = ref default_test         (* test anticipation *)
 
 let no_types = ref default_no_types (* omit types *)
 
+let list_och = ref default_list_och (* output stream for list file *)
+
+let close_list () = match !list_och with
+   | None     -> ()
+   | Some och -> close_out och
+
 let clear () =
-   R.clear ();
+   R.clear (); close_list ();
    no_init := default_no_init;
    out_dir := default_out_dir;
    proc_id := default_proc_id;
    test := default_test;
-   no_types := default_no_types
+   no_types := default_no_types;
+   list_och := default_list_och

diff --git a/matita/components/binaries/matex/options.mli b/matita/components/binaries/matex/options.mli
index 2c0e9b9b6be15bd70da4f7de919ac9715e687bcb..4629423c5d98be2ef8a8b38e994ab08441b5c9e1 100644 (file)
--- a/matita/components/binaries/matex/options.mli
+++ b/matita/components/binaries/matex/options.mli
@@ -21,4 +21,8 @@ val test: bool ref
 
 val no_types: bool ref 
 
+val list_och: out_channel option ref 
+
 val clear: unit -> unit
+
+val close_list: unit -> unit

diff --git a/matita/components/binaries/matex/test/Make b/matita/components/binaries/matex/test/Make
index e69de29bb2d1d6434b8b29ae775ad8c2e48c5391..14c1cbe2294592230d2a5244527b91020dfc4068 100644 (file)
--- a/matita/components/binaries/matex/test/Make
+++ b/matita/components/binaries/matex/test/Make
@@ -0,0 +1,2 @@
+matex.sty
+objs.tex

diff --git a/matita/components/binaries/matex/test/Makefile b/matita/components/binaries/matex/test/Makefile
index 703cbc8fb6ee1d7e6eab2ec04f8471979a081a7a..00db5d1937a68842b05c7c93e679668b92bee612 100644 (file)
--- a/matita/components/binaries/matex/test/Makefile
+++ b/matita/components/binaries/matex/test/Makefile
@@ -6,7 +6,7 @@ UNLOG  = ./unlog.pl
 
 MAIN = test
 
-SOURCES = $(shell cat Make) matex.sty
+SOURCES = $(shell cat Make) $(shell cat Make.objs)
 
 all: $(MAIN).dvi 
 
@@ -36,3 +36,6 @@ $(MAIN).pdf: $(MAIN).ps
 
 $(MAIN).tar: $(MAIN).log
        $(UNLOG) $< $@
+
+objs.tex:
+       @sed "s/\(.*\).tex/\\\\input{\1}/" Make.objs > $@

diff --git a/matita/components/binaries/matex/test/matex.sty b/matita/components/binaries/matex/test/matex.sty
index a37b0054574565b626a2af8ed5b6ea8f4e20ae5d..a889be7ada94521bd77e938d064e7eaef6fe8358 100644 (file)
--- a/matita/components/binaries/matex/test/matex.sty
+++ b/matita/components/binaries/matex/test/matex.sty
@@ -1,5 +1,5 @@
 \NeedsTeXFormat{LaTeX2e}[1995/12/01]
-\ProvidesPackage{matex}[2016/02/15 MaTeX Package]
+\ProvidesPackage{matex}[2016/02/21 MaTeX Package]
 \RequirePackage{xcolor}
 \ExecuteOptions{}
 \ProcessOptions*
@@ -17,20 +17,23 @@
 \newcommand*\ma@qed{ma@blue}
 
 \newcommand*\setlabel[1]{\protected@edef\@currentlabel{#1}}
+\newcommand*\neverindent{\setlength\parindent{0pt}}
 
 \newcommand*\ObjLabel[1]{\label{obj:#1}}
 \newcommand*\ObjRef[1]{\ref{obj:#1}}
+\newcommand*\ObjIncNode{}
+\newcommand*\ObjNode{}
 
 \newcommand*\ma@setlabel[2]{\setlabel{#1}\ObjLabel{#2}}
-\newcommand*\ma@thehead[2]{\textbf{#1 (#2)}\\}
-\newcommand*\ma@theneck[1]{\textsl{#1}\\}
+\newcommand*\ma@thehead[2]{\ObjIncNode\textbf{#1 \ObjNode(#2)}\neverindent\par}
+\newcommand*\ma@theneck[1]{\textsl{#1}\neverindent\par}
 
-\newenvironment{axiom}[2]{\ma@setlabel{#1}{#2}\ma@thehead{Axiom}{#1}}{}
-\newenvironment{declaration}[2]{\ma@setlabel{#1}{#2}\ma@thehead{Declaration}{#1}}{}
-\newenvironment{definition}[2]{}{}
-\newenvironment{proposition}[2]{\ma@setlabel{#1}{#2}\ma@thehead{Proposition}{#1}}{}
-\newenvironment{proof}[2]{\ma@theneck{Proof}}{}
-\newenvironment{ma@step}[1]{\color{#1}}{\\}
+\newenvironment{axiom}[2]{\ma@setlabel{#1}{#2}\ma@thehead{Axiom}{#1}}{\par}
+\newenvironment{declaration}[2]{\ma@setlabel{#1}{#2}\ma@thehead{Declaration}{#1}}{\par}
+\newenvironment{definition}[2]{}{\par}
+\newenvironment{proposition}[2]{\ma@setlabel{#1}{#2}\ma@thehead{Proposition}{#1}}{\par}
+\newenvironment{proof}[2]{\ma@theneck{Proof}}{\par}
+\newenvironment{ma@step}[1]{\color{#1}}{\par}
 
 \newcommand*\ma@tmp{}
 \newcommand*\ma@skip[4]{}
@@ -63,7 +66,7 @@
 \newcommand*\EXIT[1]{\ma@head{}{}{\ma@exit}{end} of block #1\ma@stop}
 \newcommand*\OPEN[3]{\ma@head{}{}{\ma@open}{#1} is this block #3\ma@stop}
 \newcommand*\PRIM[3]{\ma@head{}{}{\ma@prim}{#1} will have type #3\ma@stop}
-\newcommand*\DECL[3]{\ma@head{\ma@qed}{\_QED}{\ma@fwd}{#1} has type #3\\}
+\newcommand*\DECL[3]{\ma@head{\ma@qed}{\_QED}{\ma@fwd}{#1} has type #3\par}
 \newcommand*\BODY[1]{being #1\ma@stop}
 \newcommand*\STEP[1]{by #1\ma@tail}
 \newcommand*\DEST[1]{by cases on #1\ma@tail}

diff --git a/matita/components/binaries/matex/test/test.tex b/matita/components/binaries/matex/test/test.tex
index 057a1f54b1e9912f234acc58820c707fe401a5f5..a85f8c8f6234112dcef1a32dfd9d0be9bd2ef392 100644 (file)
--- a/matita/components/binaries/matex/test/test.tex
+++ b/matita/components/binaries/matex/test/test.tex
@@ -4,53 +4,13 @@
 \usepackage[american]{babel}
 \usepackage{matex}
 
-\begin{document}
-
-\input{matita.lambdadelta.basic_1.pr0.defs.pr0.pr0_beta.type}
-
-\bigskip
-
-\input{matita.lambdadelta.basic_1.pr0.defs.pr0.pr0_comp.type}
-
-\bigskip
-
-\input{matita.lambdadelta.basic_1.pr0.defs.pr0.pr0_delta.type}
-
-\bigskip
-
-\input{matita.lambdadelta.basic_1.pr0.defs.pr0.pr0_refl.type}
-
-\bigskip
-
-\input{matita.lambdadelta.basic_1.pr0.defs.pr0.pr0_tau.type}
-
-\bigskip
-
-\input{matita.lambdadelta.basic_1.pr0.defs.pr0.pr0.type}
+\newcounter{node}
+\renewcommand*\ObjIncNode{\stepcounter{node}}
+\renewcommand*\ObjNode{\arabic{node} }
 
-\bigskip
-
-\input{matita.lambdadelta.basic_1.pr0.defs.pr0.pr0_upsilon.type}
-
-\bigskip
-
-\input{matita.lambdadelta.basic_1.pr0.defs.pr0.pr0_zeta.type}
-
-\bigskip
-
-\input{matita.lambdadelta.basic_1.pr0.defs.pr0_ind.pr0_ind.type}
-
-\bigskip
-
-\input{matita.lambdadelta.basic_1.pr0.defs.pr0_ind.pr0_ind.body}
-
-\bigskip
-
-\input{matita.lambdadelta.basic_1.pr0.pr0.pr0_confluence.type}
-
-\bigskip
+\begin{document}
 
-\input{matita.lambdadelta.basic_1.pr0.pr0.pr0_confluence.body}
+\input{objs}
 
 \bigskip