From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Tue, 2 Feb 2016 00:00:19 +0000 (+0000)
Subject: - scope management begins...
X-Git-Tag: make_still_working~652
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=d1493110851b34e70d11eb419e557aad9bc9f2de;p=helm.git

- scope management begins...
- improved style sheet
---

diff --git a/matita/components/binaries/matex/engine.ml b/matita/components/binaries/matex/engine.ml
index 9b7ba8253..cd8ab9a01 100644
--- a/matita/components/binaries/matex/engine.ml
+++ b/matita/components/binaries/matex/engine.ml
@@ -28,8 +28,10 @@ module O = TeXOutput
 module A = Anticipate
 
 type status = {
-   n: string;   (* object name *)
+   g: string;   (* global object name *)
+   l: string;   (* local reference name *)
    s: int list; (* scope *)
+   w: bool;     (* is first construction *)
 } 
 
 (* internal functions *******************************************************)
@@ -99,12 +101,27 @@ let proc_term c t = try proc_term c t with
 (* proof processing *)
 
 let init n = {
-   n = n; s = [];
+   g = n; l = "_"; s = []; w = true
 }
 
-let mk_dec w s is =
+let push st n = {st with
+   l = n; s = 1 :: st.s; w = true
+}
+
+let pop st = {st with
+   w = false; s = match st.s with [] -> [] | i :: tl -> succ i :: tl
+}
+
+let next st = {st with
+   w = false
+}
+
+let mk_open st ris =
+   if st.w then T.Macro "PRIM" :: T.arg "" :: T.Macro "OPEN" :: ris else ris
+
+let mk_dec w s ris =
    let w = if !G.no_types then [] else w in
-   T.Group w :: T.free s :: T.arg s :: T.Macro "DECL" :: is
+   T.Group w :: T.free s :: T.arg s :: T.Macro "DECL" :: ris
 
 let rec proc_proof st ris c t = match t with
    | C.Appl []
@@ -117,7 +134,8 @@ let rec proc_proof st ris c t = match t with
    | C.Lambda (s, w, t)    -> 
       let s = alpha c s in
       let is_w = proc_term c w in
-      proc_proof st (T.Macro "PRIM" :: mk_dec is_w s ris) (K.add_dec s w c) t
+      let ris = mk_open st ris in
+      proc_proof (next st) (T.Macro "PRIM" :: mk_dec 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
       let ris = T.Macro "STEP" :: ris in
@@ -133,10 +151,10 @@ let rec proc_proof st ris c t = match t with
       let is_w = proc_term c w in
       if A.not_prop1 c w then
          let is_v = proc_term c v in
-         proc_proof st (T.Group is_v :: T.Macro "BODY" :: mk_dec is_w s ris) (K.add_def s w v c) t
+         proc_proof (next st) (T.Group is_v :: T.Macro "BODY" :: mk_dec is_w s ris) (K.add_def s w v c) t
       else
-         let ris_v = proc_proof st ris c v in
-         proc_proof st (mk_dec is_w s ris_v) (K.add_def s w v c) t
+         let ris_v = proc_proof (push st s) ris c v in
+         proc_proof (pop st) (mk_dec is_w s ris_v) (K.add_def s w v c) t
 
 let proc_proof c t = try proc_proof (init "") [] c t with 
    | E.ObjectNotFound _ 
diff --git a/matita/components/binaries/matex/test/matex.sty b/matita/components/binaries/matex/test/matex.sty
index 6bbcfe094..de1b6a0f5 100644
--- a/matita/components/binaries/matex/test/matex.sty
+++ b/matita/components/binaries/matex/test/matex.sty
@@ -9,6 +9,7 @@
 
 \newcommand*\Object[3]{\begin{prop}[#1]\hfil\\\setlabel{#1}\ObjLabel{#2}#3\end{prop}}
 
+\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}