- matex: minor corrections to handle applications with many arguments

- matex test stylesheets: some improvements, notation for ground_1 completed

diff --git a/matita/components/binaries/matex/engine.ml b/matita/components/binaries/matex/engine.ml
index 8ed2a3d5709254b4afc044e75e2a113db6cd5646..2fffd264ce1e416d1b1f324ea3ccf7fa0e2b21f8 100644 (file)
--- a/matita/components/binaries/matex/engine.ml
+++ b/matita/components/binaries/matex/engine.ml
@@ -63,17 +63,20 @@ let mk_ptr st name =
 
 let get_macro s l =
    let rec aux = function
-      | []                                 -> ""
-      | (r, m, a) :: _ when r = s && a = l -> m
-      | _ :: tl                            -> aux tl
+      | []                                    -> "", 0
+      | (r, m, a, x) :: _ when r = s && a = l -> m, x
+      | _ :: tl                               -> aux tl
    in
    aux !G.macro_gref
 
 let get_head = function
    | C.Const c :: ts ->
       let s, _ = K.resolve_reference c in
-      let macro = get_macro s (L.length ts) in
-      if macro <> "" then Some (macro, s, ts) else begin 
+      let macro, x = get_macro s (L.length ts) in
+      if macro <> "" then
+         let ts1, ts2 = X.split_at x ts in
+         Some (macro, s, ts1, ts2)
+      else begin 
          if !G.log_missing then missing s;
          None
       end 
@@ -94,12 +97,17 @@ let rec proc_term st is = function
       T.Macro "LREF" :: T.arg (mk_lname s) :: T.free (mk_ptr st s) :: is
    | C.Appl ts              ->
       begin match get_head ts with
-         | Some (macro, s, ts) ->
-            let riss = L.rev_map (proc_term st []) ts in
-            T.Macro macro :: T.free s :: T.mk_rev_args riss is
-         | None                ->
+         | None                      ->
             let riss = L.rev_map (proc_term st []) ts in
             T.Macro "APPL" :: T.mk_rev_args riss is
+         | Some (macro, s, [], ts)
+         | Some (macro, s, ts, [])   ->
+            let riss = L.rev_map (proc_term st []) ts in
+            T.Macro macro :: T.free s :: T.mk_rev_args riss is
+         | Some (macro, s, ts1, ts2) ->
+            let riss1 = L.rev_map (proc_term st []) ts1 in
+            let riss2 = L.rev_map (proc_term st []) ts2 in
+            T.Macro macro :: T.free s :: T.mk_rev_args riss1 (T.mk_rev_args riss2 is)
       end
    | C.Prod (s, w, t)       ->
       let is_w = proc_term st [] w in

diff --git a/matita/components/binaries/matex/ground.ml b/matita/components/binaries/matex/ground.ml
index 91d85bc36443e1ac1d296abb486762cf14c69ca5..7eebedb7d13e8fa810c4dc0eb867aa038362e474 100644 (file)
--- a/matita/components/binaries/matex/ground.ml
+++ b/matita/components/binaries/matex/ground.ml
@@ -56,6 +56,13 @@ let rec rev_map_append map l r = match l with
    | []       -> r
    | hd :: tl -> rev_map_append map tl (map hd :: r)
 
+let rec split_at x = function
+   | l when x <= 0 -> [], l
+   | []       -> [], []
+   | hd :: tl -> 
+      let l1, l2 = split_at (pred x) tl in
+      hd :: l1, l2
+
 let error s = raise (Error s)
 
 let log s = P.eprintf "MaTeX: %s\n%!" s

diff --git a/matita/components/binaries/matex/ground.mli b/matita/components/binaries/matex/ground.mli
index 9cc32beda5745c282c487fed54fc01d99b26c343..923ec58b7bab7e0e88cd381c92261a9328a504e9 100644 (file)
--- a/matita/components/binaries/matex/ground.mli
+++ b/matita/components/binaries/matex/ground.mli
@@ -32,3 +32,5 @@ val foldi_left: (int -> 'a -> 'b -> 'a) -> int -> 'a -> 'b list -> 'a
 val rev_mapi: (int -> 'b -> 'a) -> int -> 'b list -> 'a list
 
 val rev_map_append: ('a -> 'b) -> 'a list -> 'b list -> 'b list
+
+val split_at: int -> 'a list -> 'a list * 'a list

diff --git a/matita/components/binaries/matex/matex.ml b/matita/components/binaries/matex/matex.ml
index 30f96287a9132215b7a4332b3d00297d18040cb7..88ae85436d3c06379b5973fb59104fe0a1b90387 100644 (file)
--- a/matita/components/binaries/matex/matex.ml
+++ b/matita/components/binaries/matex/matex.ml
@@ -39,7 +39,7 @@ let alpha_decode = R.triple R.string R.string R.string
 
 let const_decode = R.pair R.string R.string
 
-let macro_decode = R.triple R.string R.string R.int
+let macro_decode = R.quad R.string R.string R.int R.int
 
 let init registry =
    R.load_from registry; 

diff --git a/matita/components/binaries/matex/options.ml b/matita/components/binaries/matex/options.ml
index 1a252214221af200d57194b58a03b0609191c453..b361841c608f8f13cc28d3e3d2759d86d716a5af 100644 (file)
--- a/matita/components/binaries/matex/options.ml
+++ b/matita/components/binaries/matex/options.ml
@@ -70,7 +70,7 @@ let alpha_sort = ref default_alpha          (* data for sort-based alpha-convers
 
 let alpha_gref = ref default_alpha          (* data for constant renaming *)
 
-let macro_gref = ref default_macro          (* data eta-conversion and constant rendering *)
+let macro_gref = ref default_macro          (* data for eta-conversion and constant rendering *)
 
 let is_global_id s =
    !global_alpha && s <> dno_id

diff --git a/matita/components/binaries/matex/options.mli b/matita/components/binaries/matex/options.mli
index da4f7a46dc1ac63c473c16368ef1a05c5cec9417..3801a8d19b1483d24841827e2412bb25cf75832d 100644 (file)
--- a/matita/components/binaries/matex/options.mli
+++ b/matita/components/binaries/matex/options.mli
@@ -39,7 +39,7 @@ val alpha_sort: (string * string * string) list ref
 
 val alpha_gref: (string * string) list ref
 
-val macro_gref: (string * string * int) list ref
+val macro_gref: (string * string * int * int) list ref
 
 val clear: unit -> unit
 

diff --git a/matita/components/binaries/matex/test/ground_1.conf.xml b/matita/components/binaries/matex/test/ground_1.conf.xml
index 77d65746f153c69057c610ddc20a9bc7f69c796e..aff4fc4dd48b40c2199265571907b3b538db9dfb 100644 (file)
--- a/matita/components/binaries/matex/test/ground_1.conf.xml
+++ b/matita/components/binaries/matex/test/ground_1.conf.xml
@@ -1,29 +1,29 @@
 <?xml version="1.0" encoding="utf-8"?>
 <helm_registry>
-<!--
-matita.lambdadelta.ground_1.types.defs.ex2_2.ex2_2.type
-matita.lambdadelta.ground_1.types.defs.ex2_3.ex2_3.type
-matita.lambdadelta.ground_1.types.defs.ex_2.ex_2.type
-matita.lambdadelta.ground_1.types.defs.ex3_2.ex3_2.type
-matita.lambdadelta.ground_1.types.defs.ex3_3.ex3_3.type
-matita.lambdadelta.ground_1.types.defs.ex3_4.ex3_4.type
-matita.lambdadelta.ground_1.types.defs.ex_3.ex_3.type
-matita.lambdadelta.ground_1.types.defs.ex3.ex3.type
-matita.lambdadelta.ground_1.types.defs.ex4_2.ex4_2.type
-matita.lambdadelta.ground_1.types.defs.ex4_3.ex4_3.type
-matita.lambdadelta.ground_1.types.defs.ex4_4.ex4_4.type
-matita.lambdadelta.ground_1.types.defs.ex4_5.ex4_5.type
-matita.lambdadelta.ground_1.types.defs.ex4.ex4.type
-matita.lambdadelta.ground_1.types.defs.ex5_3.ex5_3.type
-matita.lambdadelta.ground_1.types.defs.ex6_6.ex6_6.type
-matita.lambdadelta.ground_1.types.defs.or3.or3.type
-matita.lambdadelta.ground_1.types.defs.or4.or4.type
-matita.lambdadelta.ground_1.types.defs.and3.and3.type
+  <section name="matex.notation">
+    <key name="const">matita.lambdadelta.ground_1.types.defs.ex_2.ex_2.type LEx 3 2</key>
+    <key name="const">matita.lambdadelta.ground_1.types.defs.ex_3.ex_3.type LEx 4 3</key>
+    <key name="const">matita.lambdadelta.ground_1.types.defs.ex2_2.ex2_2.type LEx 4 2</key>
+    <key name="const">matita.lambdadelta.ground_1.types.defs.ex2_3.ex2_3.type LEx 5 3</key>
+    <key name="const">matita.lambdadelta.ground_1.types.defs.ex3.ex3.type LEx 4 1</key>
+    <key name="const">matita.lambdadelta.ground_1.types.defs.ex3_2.ex3_2.type LEx 5 2</key>
+    <key name="const">matita.lambdadelta.ground_1.types.defs.ex3_3.ex3_3.type LEx 6 3</key>
+    <key name="const">matita.lambdadelta.ground_1.types.defs.ex3_4.ex3_4.type LEx 7 4</key>
+    <key name="const">matita.lambdadelta.ground_1.types.defs.ex4.ex4.type LEx 5 1</key>
+    <key name="const">matita.lambdadelta.ground_1.types.defs.ex4_2.ex4_2.type LEx 6 2</key>
+    <key name="const">matita.lambdadelta.ground_1.types.defs.ex4_3.ex4_3.type LEx 7 3</key>
+    <key name="const">matita.lambdadelta.ground_1.types.defs.ex4_4.ex4_4.type LEx 8 4</key>
+    <key name="const">matita.lambdadelta.ground_1.types.defs.ex4_5.ex4_5.type LEx 9 5</key>
+    <key name="const">matita.lambdadelta.ground_1.types.defs.ex5_3.ex5_3.type LEx 8 3</key>
+    <key name="const">matita.lambdadelta.ground_1.types.defs.ex6_6.ex6_6.type LEx 12 6</key>
+    <key name="const">matita.lambdadelta.ground_1.types.defs.and3.and3.type LAnd 3 0</key>
+    <key name="const">matita.lambdadelta.ground_1.types.defs.or3.or3.type LOr 3 0</key>
+    <key name="const">matita.lambdadelta.ground_1.types.defs.or4.or4.type LOr 4 0</key>
 
-matita.lambdadelta.ground_1.blt.defs.blt.blt.type
-matita.lambdadelta.ground_1.plist.defs.papp.papp.type
-matita.lambdadelta.ground_1.plist.defs.PConsTail.PConsTail.type
-matita.lambdadelta.ground_1.plist.defs.PList.PCons.type
-matita.lambdadelta.ground_1.plist.defs.Ss.Ss.type
--->
+    <key name="const">matita.lambdadelta.ground_1.blt.defs.blt.blt.type FunLt 2 0</key>
+    <key name="const">matita.lambdadelta.ground_1.plist.defs.papp.papp.type Append 2 0</key>
+    <key name="const">matita.lambdadelta.ground_1.plist.defs.PConsTail.PConsTail.type RevConsB 3 0</key>
+    <key name="const">matita.lambdadelta.ground_1.plist.defs.PList.PCons.type ConsB 3 0</key>
+    <key name="const">matita.lambdadelta.ground_1.plist.defs.Ss.Ss.type Succ 1 0</key>
+  </section>
 </helm_registry>

diff --git a/matita/components/binaries/matex/test/ground_1.sty b/matita/components/binaries/matex/test/ground_1.sty
index 582e49cefb234f0993af71867b045a8c270f19ed..58f2592de36ae83d8b1fffd5d94ba0316f090393 100644 (file)
--- a/matita/components/binaries/matex/test/ground_1.sty
+++ b/matita/components/binaries/matex/test/ground_1.sty
@@ -1,10 +1,26 @@
 \NeedsTeXFormat{LaTeX2e}[1995/12/01]
-\ProvidesPackage{ground_1}[2016/05/23 Notation for "cic:/matita/lambdadelta/ground_1/"]
+\ProvidesPackage{ground_1}[2016/06/19 Notation for "cic:/matita/lambdadelta/ground_1/"]
+\RequirePackage{matex}
 \ExecuteOptions{}
 \ProcessOptions*
 
 \makeatletter
 
+\newcommand*\ld@cm[1]{\setpunctlink{,}{#1}}
+\newcommand*\ld@oa[1]{\setopenlink{\langle}{#1}}
+\newcommand*\ld@ca[1]{\setcloselink{\rangle}{#1}}
+
+\newcommand*\ld@append[1]{\setbinlink{@}{#1}}
+\newcommand*\ld@cons[1]{\setbinlink{\copyright}{#1}}
+\newcommand*\ld@funlt[1]{\setbinlink{\olessthan}{#1}}
+
+\newcommand*\ld@tupleB[3]{\ld@oa{#1}#2\ld@cm{#1}#3\ld@ca{#1}}
+
+\newcommand*\Append[3]{#2\ld@append{#1}#3}
+\newcommand*\ConsB[4]{\ld@tupleB{#1}{#2}{#3}\ld@cons{#1}#4}
+\newcommand*\FunLt[3]{#2\ld@funlt{#1}#3}
+\newcommand*\RevConsB[4]{#2\ld@cons{#1}\ld@tupleB{#1}{#3}{#4}}
+
 \makeatother
 
 \endinput

diff --git a/matita/components/binaries/matex/test/legacy_1.conf.xml b/matita/components/binaries/matex/test/legacy_1.conf.xml
index e215669f8284e3bf8cbfe5c7ab111f09b41804eb..606b6b7762255ecf1cc8e80d4a449cc286b52ee2 100644 (file)
--- a/matita/components/binaries/matex/test/legacy_1.conf.xml
+++ b/matita/components/binaries/matex/test/legacy_1.conf.xml
@@ -1,18 +1,18 @@
 <?xml version="1.0" encoding="utf-8"?>
 <helm_registry>
   <section name="matex.notation">
-    <key name="const">matita.lambdadelta.legacy_1.coq.defs.ex.ex.type LExAA 2</key>
-    <key name="const">matita.lambdadelta.legacy_1.coq.defs.ex2.ex2.type LExBA 3</key>
-    <key name="const">matita.lambdadelta.legacy_1.coq.defs.land.land.type LAndB 2</key>
-    <key name="const">matita.lambdadelta.legacy_1.coq.defs.or.or.type LOrB 2</key>
+    <key name="const">matita.lambdadelta.legacy_1.coq.defs.ex.ex.type LEx 2 1</key>
+    <key name="const">matita.lambdadelta.legacy_1.coq.defs.ex2.ex2.type LEx 3 1</key>
+    <key name="const">matita.lambdadelta.legacy_1.coq.defs.land.land.type LAnd 2 0</key>
+    <key name="const">matita.lambdadelta.legacy_1.coq.defs.or.or.type LOr 2 0</key>
 
-    <key name="const">matita.lambdadelta.legacy_1.coq.defs.eq.eq.type EQ 3</key>
-    <key name="const">matita.lambdadelta.legacy_1.coq.defs.le.le.type LE 2</key>
-    <key name="const">matita.lambdadelta.legacy_1.coq.defs.lt.type LT 2</key>
-    <key name="const">matita.lambdadelta.legacy_1.coq.defs.minus.minus.type Minus 2</key>
-    <key name="const">matita.lambdadelta.legacy_1.coq.defs.nat.S.type Succ 1</key>
-    <key name="const">matita.lambdadelta.legacy_1.coq.defs.not.type LNot 1</key>
-    <key name="const">matita.lambdadelta.legacy_1.coq.defs.plus.plus.type Plus 2</key>
-    <key name="const">matita.lambdadelta.legacy_1.coq.defs.pred.type Pred 1</key>
+    <key name="const">matita.lambdadelta.legacy_1.coq.defs.eq.eq.type EQ 3 0</key>
+    <key name="const">matita.lambdadelta.legacy_1.coq.defs.le.le.type LE 2 0</key>
+    <key name="const">matita.lambdadelta.legacy_1.coq.defs.lt.type LT 2 0</key>
+    <key name="const">matita.lambdadelta.legacy_1.coq.defs.minus.minus.type Minus 2 0</key>
+    <key name="const">matita.lambdadelta.legacy_1.coq.defs.nat.S.type Succ 1 0</key>
+    <key name="const">matita.lambdadelta.legacy_1.coq.defs.not.type LNot 1 0</key>
+    <key name="const">matita.lambdadelta.legacy_1.coq.defs.plus.plus.type Plus 2 0</key>
+    <key name="const">matita.lambdadelta.legacy_1.coq.defs.pred.type Pred 1 0</key>
   </section>
 </helm_registry>

diff --git a/matita/components/binaries/matex/test/legacy_1.sty b/matita/components/binaries/matex/test/legacy_1.sty
index 10edd9b625af3d1743705afae2bf302c68ea8e2f..0ee7783459dd7d0311096061b3e0acbb16ed0847 100644 (file)
--- a/matita/components/binaries/matex/test/legacy_1.sty
+++ b/matita/components/binaries/matex/test/legacy_1.sty
@@ -1,5 +1,5 @@
 \NeedsTeXFormat{LaTeX2e}[1995/12/01]
-\ProvidesPackage{legacy_1}[2016/06/06 Notation for "cic:/matita/lambdadelta/legacy_1/"]
+\ProvidesPackage{legacy_1}[2016/06/19 Notation for "cic:/matita/lambdadelta/legacy_1/"]
 \RequirePackage{matex}
 \RequirePackage{fdsymbol}
 \ExecuteOptions{}
@@ -17,16 +17,17 @@
 \newcommand*\ld@eq[1]{\setrellink{=}{#1}}
 \newcommand*\ld@le[1]{\setrellink{\le}{#1}}
 \newcommand*\ld@lt[1]{\setrellink{<}{#1}}
-\newcommand*\ld@minus[1]{\setbinlink{+}{#1}}
+\newcommand*\ld@minus[1]{\setbinlink{-}{#1}}
 \newcommand*\ld@lnot[1]{\setoplink{\lnot}{#1}}
-\newcommand*\ld@plus[1]{\setbinlink{-}{#1}}
+\newcommand*\ld@plus[1]{\setbinlink{+}{#1}}
 \newcommand*\ld@pred[1]{\setoplink{\downspoon}{#1}}
 \newcommand*\ld@succ[1]{\setoplink{\upspoon}{#1}}
 
-\newcommand*\LAndB[3]{#2\ld@land{#1}#3}
-\newcommand*\LOrB[3]{#2\ld@lor{#1}#3}
-\newcommand*\LExAA[3]{\ld@lex{#1}#3}
-\newcommand*\LExBA[4]{\ld@lex{#1}#3\ld@and{#1}#4}
+\newcommand*\ld@list[2]{\ma@list\relax\ma@arg{#1{#2}}\relax}
+
+\newcommand*\LAnd[1]{\ld@list\ld@land{#1}}
+\newcommand*\LOr[1]{\ld@list\ld@lor{#1}}
+\newcommand*\LEx[1]{\ld@lex{#1}\ma@list\relax\ma@skip\relax{\ld@list\ld@and{#1}}}
 
 \newcommand*\EQ[4]{#3\ld@eq{#1}#4}
 \newcommand*\LE[3]{#2\ld@le{#1}#3}

diff --git a/matita/components/binaries/matex/test/matex.sty b/matita/components/binaries/matex/test/matex.sty
index 9b2e412c7ff13975116135b25ceb7cebe70e805e..a46b2af1b264840cca78e867e0dd9ac02f67f283 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/06/12 MaTeX Package]
+\ProvidesPackage{matex}[2016/06/19 MaTeX Package]
 \RequirePackage{xcolor}
 \RequirePackage{stix}
 \ExecuteOptions{}
@@ -47,6 +47,9 @@
 \newcommand*\setoplink[2]{\mathop{\ma@setlink{#1}{#2}}}
 \newcommand*\setbinlink[2]{\mathbin{\ma@setlink{#1}{#2}}}
 \newcommand*\setrellink[2]{\mathrel{\ma@setlink{#1}{#2}}}
+\newcommand*\setopenlink[2]{\mathopen{\ma@setlink{#1}{#2}}}
+\newcommand*\setcloselink[2]{\mathclose{\ma@setlink{#1}{#2}}}
+\newcommand*\setpunctlink[2]{\mathpunct{\ma@setlink{#1}{#2}}}
 
 \newcommand*\ObjIncNode{}
 \newcommand*\ObjNode{}
@@ -62,20 +65,21 @@
 \newenvironment{ma@step}[1]{\color{#1}}{\par}
 
 \newcommand*\ma@tmp{}
-\newcommand*\ma@skip[4]{}
-\newcommand*\ma@next[5]{\def\ma@tmp{#5}%
-   \ifx\ma@tmp\empty #4\let\ma@tmp=\ma@skip\else #1#2{#5}\let\ma@tmp=\ma@next\fi
-   \ma@tmp #3#2#3#4%
+\newcommand*\ma@last[4]{#4}
+\newcommand*\ma@list[5]{\def\ma@tmp{#5}%
+   \ifx\ma@tmp\empty\let\ma@tmp=\ma@last\else #1#2{#5}\let\ma@tmp=\ma@list\fi
+   \ma@tmp{#3}{#2}{#3}{#4}%
 }
-\newcommand*\ma@thop[1]{\mathop{#1}\allowbreak}
+\newcommand*\ma@thop[1]{\mathpunct{#1}\allowbreak}
 \newcommand*\ma@cm{\ma@thop{,}}
 \newcommand*\ma@or{\mathbin\vert}
 \newcommand*\ma@cp{)\allowbreak}
 \newcommand*\ma@qm{\mathord{?}}
 \newcommand*\ma@arg[1]{#1}
-\newcommand*\ma@args{(\ma@next\relax\ma@arg\ma@cm\ma@cp}
-\newcommand*\ma@cases{\ma@next\relax\ma@arg\ma@or\relax}
+\newcommand*\ma@args{(\ma@list\relax\ma@arg\ma@cm\ma@cp}
+\newcommand*\ma@cases{\ma@list\relax\ma@arg\ma@or\relax}
 \newcommand*\ma@bind{\ma@thop{}}
+\newcommand*\ma@skip[1]{}
 
 \newcommand*\PROP{\mathord\mathrm{PROP}}
 \newcommand*\CROP[1]{\mathord\mathrm{CROP}}
@@ -106,7 +110,7 @@
    \else\begin{ma@step}{#4}$\mathbf{\ma@setopttarget{#5}{#6}}$%
    \fi
 }
-\newcommand*\ma@tail{\ma@next\ma@with\ma@term\ma@comma\ma@stop}
+\newcommand*\ma@tail{\ma@list\ma@with\ma@term\ma@comma\ma@stop}
 \newcommand*\ma@type[1]{\def\ma@tmp{#1}%
    \ifx\ma@tmp\empty\mathrm{(omitted)}\else #1\fi
 }

diff --git a/matita/components/registry/helm_registry.ml b/matita/components/registry/helm_registry.ml
index 877de0a1c0cc8c108dbdf67b6a14199f5557285e..08b1bb76f893320db7ca6db238bfacb0c16634c2 100644 (file)
--- a/matita/components/registry/helm_registry.ml
+++ b/matita/components/registry/helm_registry.ml
@@ -121,6 +121,12 @@ let triple fst_unmarshaller snd_unmarshaller trd_unmarshaller v =
   | [fst; snd; trd] -> fst_unmarshaller fst, snd_unmarshaller snd, trd_unmarshaller trd
   | _ -> raise (Type_error "not a triple")
 
+(* FG *)
+let quad fst_unmarshaller snd_unmarshaller trd_unmarshaller fth_unmarshaller v =
+  match Str.split spaces_rex v with
+  | [fst; snd; trd; fth] -> fst_unmarshaller fst, snd_unmarshaller snd, trd_unmarshaller trd, fth_unmarshaller fth
+  | _ -> raise (Type_error "not a quad")
+
   (* escapes for xml configuration file *)
 let (escape, unescape) =
   let (in_enc, out_enc) = (`Enc_utf8, `Enc_utf8) in
@@ -220,6 +226,10 @@ let get_pair registry fst_unmarshaller snd_unmarshaller =
 let get_triple registry fst_unmarshaller snd_unmarshaller trd_unmarshaller =
   get_typed registry (triple fst_unmarshaller snd_unmarshaller trd_unmarshaller) 
 
+(* FG *)
+let get_quad registry fst_unmarshaller snd_unmarshaller trd_unmarshaller fth_unmarshaller =
+  get_typed registry (quad fst_unmarshaller snd_unmarshaller trd_unmarshaller fth_unmarshaller) 
+
 let set_list registry marshaller ~key ~value =
   (* since ocaml hash table are crazy... *)
   while Hashtbl.mem registry key do
@@ -424,6 +434,7 @@ let get_opt_default unmarshaller = get_opt_default default_registry unmarshaller
 let get_list unmarshaller = get_list default_registry unmarshaller
 let get_pair unmarshaller = get_pair default_registry unmarshaller
 let get_triple unmarshaller = get_triple default_registry unmarshaller
+let get_quad unmarshaller = get_quad default_registry unmarshaller
 let set_typed marshaller = set_typed default_registry marshaller
 let set_opt unmarshaller = set_opt default_registry unmarshaller
 let set_list marshaller = set_list default_registry marshaller

diff --git a/matita/components/registry/helm_registry.mli b/matita/components/registry/helm_registry.mli
index 68434603dbe4e08243203304f2aeb0ffb794af0d..29dd335faab474926b877f38d7d53864fda31f97 100644 (file)
--- a/matita/components/registry/helm_registry.mli
+++ b/matita/components/registry/helm_registry.mli
@@ -134,6 +134,7 @@ val float:        string -> float
 val bool:         string -> bool
 val pair:         (string -> 'a) -> (string -> 'b) -> string -> 'a * 'b
 val triple:       (string -> 'a) -> (string -> 'b) -> (string -> 'c) -> string -> 'a * 'b * 'c
+val quad:         (string -> 'a) -> (string -> 'b) -> (string -> 'c) -> (string -> 'd) -> string -> 'a * 'b * 'c * 'd
 
 (** {3 Typed getters} *)
 
@@ -154,6 +155,9 @@ val get_pair: (string -> 'a) -> (string -> 'b) -> string -> 'a * 'b
   (** decode values which are blank separated list of values, of length 3 *)
 val get_triple: (string -> 'a) -> (string -> 'b) -> (string -> 'c) -> string -> 'a * 'b * 'c
 
+  (** decode values which are blank separated list of values, of length 4 *)
+val get_quad: (string -> 'a) -> (string -> 'b) -> (string -> 'c) -> (string -> 'd) -> string -> 'a * 'b * 'c * 'd
+
 (** {4 Shorthands} *)
 
 val get_string: string -> string