propagating the arithmetics library, partial commit

[helm.git] / matita / matita / contribs / lambdadelta / bin / recomm / recommCheck.ml

diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/recommCheck.ml b/matita/matita/contribs/lambdadelta/bin/recomm/recommCheck.ml
index 93d1d03162f09db324668c9dbb34cad206ef3b94..53e68f84bdb20185521285680d5fed7fc2ebd56e 100644 (file)
--- a/matita/matita/contribs/lambdadelta/bin/recomm/recommCheck.ml
+++ b/matita/matita/contribs/lambdadelta/bin/recomm/recommCheck.ml
@@ -5,7 +5,7 @@ let c_line = ref ES.id
 
 let s_line = ref ES.id
 
-let k_final b ws1 ws2 = b, ws1, ws2  
+let k_final r ws1 ws2 = r, ws1, ws2
 
 type status =
   {
@@ -29,16 +29,17 @@ let middle st =
   | _              -> true
 
 let mute_o = [|
-  "___                                                              ";
-  "||M||                                                             ";
-  "||A||       A project by Andrea Asperti                           ";
-  "||T||                                                             ";
-  "||I||       Developers:                                           ";
-  "||T||         The HELM team.                                      ";
-  "||A||         http://helm.cs.unibo.it                             ";
-  "\\   /                                                             ";
-  "\\ /        This file is distributed under the terms of the       ";
-  "v         GNU General Public License Version 2                  ";
+  "                                                                        ";
+  "       ___                                                              ";
+  "      ||M||                                                             ";
+  "      ||A||       A project by Andrea Asperti                           ";
+  "      ||T||                                                             ";
+  "      ||I||       Developers:                                           ";
+  "      ||T||         The HELM team.                                      ";
+  "      ||A||         http://helm.cs.unibo.it                             ";
+  "      \\   /                                                             ";
+  "       \\ /        This file is distributed under the terms of the       ";
+  "        v         GNU General Public License Version 2                  ";
   "";
 |]
 
@@ -63,40 +64,40 @@ let log color s =
 
 let rec recomm srcs st =
   match srcs with
-  | []                             ->
+  | []                                ->
     st
-  | ET.Line _ as hd :: tl          ->
+  | ET.Line _ as hd :: tl             ->
     recomm tl @@ add hd @@ st
-  | ET.Text _ as hd :: tl          ->
+  | ET.Text _ as hd :: tl             ->
     recomm tl @@ add hd @@ st
-  | ET.Mark s as hd :: tl          ->
+  | ET.Mark s as hd :: tl             ->
     if !log_m then log red s;
     recomm tl @@ add hd @@ st
-  | ET.Key (s1, s2) as hd :: tl    ->
+  | ET.Key (s1, s2) as hd :: tl       ->
     if middle st then Printf.eprintf "middle: %S\n" s1;
     if !log_k then log prune (s1^s2);
     recomm tl @@ add hd @@ st
-  | ET.Title ss as hd :: tl        ->
+  | ET.Title ss :: tl                 ->
     if middle st then Printf.eprintf "middle: TITLE\n";
-    let b, ss1, ss2 = !c_line k_final false [] ss in
+    let r, ss1, ss2 = !c_line k_final ET.OO [] ss in
     let ss2 =
-      if ss2 = [] then ss2 else "*" :: ss2
+      if r <> ET.KO && ss2 = [] then ss2 else "*" :: ss2
     in
     let ss = List.rev_append ss1 ss2 in
     let s = String.concat " " ss in
     if !log_t then log blue s;
-    recomm tl @@ add hd @@ st
-  | ET.Slice ss as hd :: tl        ->
+    recomm tl @@ add (ET.Title ss) @@ st
+  | ET.Slice ss :: tl                 ->
     if middle st then Printf.eprintf "middle: Section\n";
-    let b, ss1, ss2 = !s_line k_final false [] ss in
+    let r, ss1, ss2 = !s_line k_final ET.OO [] ss in
     let ss2 =
-      if ss2 = [] then ss2 else "*" :: ss2
+      if r <> ET.KO && ss2 = [] then ss2 else "*" :: ss2
     in
     let ss = List.rev_append ss1 ss2 in
     let s = String.capitalize_ascii (String.concat " " ss) in
     if !log_s then log sky s;
-    recomm tl @@ add hd @@ st
-  | ET.Other (_, s, _) as hd :: tl ->
+    recomm tl @@ add (ET.Slice ss) @@ st
+  | ET.Other (_, _, s, _) as hd :: tl ->
     if !log_o && not (Array.mem s mute_o) then log black s;
     recomm tl @@ add hd @@ st