matita/matita/contribs/lambdadelta/bin/recomm/recommCheck.ml

   1 module ES = RecommStep
   2 module ET = RecommTypes
   3
   4 let c_line = ref ES.id
   5
   6 let s_line = ref ES.id
   7
   8 let k_final r ws1 ws2 = r, ws1, ws2
   9
  10 type status =
  11   {
  12     r: ET.srcs; (* reversed result *)
  13   }
  14
  15 let init () =
  16   {
  17     r = [];
  18   }
  19
  20 let add src st =
  21   {
  22     r = src :: st.r;
  23   }
  24
  25 let middle st =
  26   match st.r with
  27   | []
  28   | ET.Line _ :: _ -> false
  29   | _              -> true
  30
  31 let mute_o = [|
  32   "                                                                        ";
  33   "       ___                                                              ";
  34   "      ||M||                                                             ";
  35   "      ||A||       A project by Andrea Asperti                           ";
  36   "      ||T||                                                             ";
  37   "      ||I||       Developers:                                           ";
  38   "      ||T||         The HELM team.                                      ";
  39   "      ||A||         http://helm.cs.unibo.it                             ";
  40   "      \\   /                                                             ";
  41   "       \\ /        This file is distributed under the terms of the       ";
  42   "        v         GNU General Public License Version 2                  ";
  43   "";
  44 |]
  45
  46 let bw = ref false
  47
  48 let log_k = ref false
  49 let log_m = ref false
  50 let log_o = ref false
  51 let log_s = ref false
  52 let log_t = ref false
  53
  54 let no_color = "\x1B[0m"
  55 let black    = "\x1B[30m"
  56 let sky      = "\x1B[38;2;0;96;128m"
  57 let blue     = "\x1B[34m"
  58 let prune    = "\x1B[38;2;96;0;128m"
  59 let red      = "\x1B[31m"
  60
  61 let log color s =
  62   if !bw then Printf.printf "%S\n" s else
  63   Printf.printf "%s%S%s\n" color s no_color
  64
  65 let rec recomm srcs st =
  66   match srcs with
  67   | []                             ->
  68     st
  69   | ET.Line _ as hd :: tl          ->
  70     recomm tl @@ add hd @@ st
  71   | ET.Text _ as hd :: tl          ->
  72     recomm tl @@ add hd @@ st
  73   | ET.Mark s as hd :: tl          ->
  74     if !log_m then log red s;
  75     recomm tl @@ add hd @@ st
  76   | ET.Key (s1, s2) as hd :: tl    ->
  77     if middle st then Printf.eprintf "middle: %S\n" s1;
  78     if !log_k then log prune (s1^s2);
  79     recomm tl @@ add hd @@ st
  80   | ET.Title ss :: tl              ->
  81     if middle st then Printf.eprintf "middle: TITLE\n";
  82     let r, ss1, ss2 = !c_line k_final ET.OO [] ss in
  83     let ss2 =
  84       if r <> ET.KO && ss2 = [] then ss2 else "*" :: ss2
  85     in
  86     let ss = List.rev_append ss1 ss2 in
  87     let s = String.concat " " ss in
  88     if !log_t then log blue s;
  89     recomm tl @@ add (ET.Title ss) @@ st
  90   | ET.Slice ss :: tl              ->
  91     if middle st then Printf.eprintf "middle: Section\n";
  92     let r, ss1, ss2 = !s_line k_final ET.OO [] ss in
  93     let ss2 =
  94       if r <> ET.KO && ss2 = [] then ss2 else "*" :: ss2
  95     in
  96     let ss = List.rev_append ss1 ss2 in
  97     let s = String.capitalize_ascii (String.concat " " ss) in
  98     if !log_s then log sky s;
  99     recomm tl @@ add (ET.Slice ss) @@ st
 100   | ET.Other (_, s, _) as hd :: tl ->
 101     if !log_o && not (Array.mem s mute_o) then log black s;
 102     recomm tl @@ add hd @@ st
 103
 104 let recomm_srcs srcs =
 105   let st = recomm srcs @@ init () in
 106   List.rev st.r
 107
 108 let register_c = ES.register c_line
 109
 110 let register_s = ES.register s_line