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