package codex

  1. Overview
  2. Docs
package codex
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Source file terminal.ml

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
(**************************************************************************)
(*  This file is part of the Codex semantics library.                     *)
(*                                                                        *)
(*  Copyright (C) 2013-2025                                               *)
(*    CEA (Commissariat à l'énergie atomique et aux énergies              *)
(*         alternatives)                                                  *)
(*                                                                        *)
(*  you can redistribute it and/or modify it under the terms of the GNU   *)
(*  Lesser General Public License as published by the Free Software       *)
(*  Foundation, version 2.1.                                              *)
(*                                                                        *)
(*  It is distributed in the hope that it will be useful,                 *)
(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         *)
(*  GNU Lesser General Public License for more details.                   *)
(*                                                                        *)
(*  See the GNU Lesser General Public License version 2.1                 *)
(*  for more details (enclosed in the file LICENSE).                      *)
(*                                                                        *)
(**************************************************************************)

open Common;;

type terminal_code_status = {
  weight: weight;
  color: color option; (* None when we don't know: the "normal" color. *)
  underline: bool;
  italic: bool;
}
let initial_state = { weight = Normal; color = None; underline = false; italic = false }

let nesting_level = ref 0;;
(* let file_nesting_level = ref 0
let open_file_nesting () = incr file_nesting_level
let close_file_nesting () = if !file_nesting_level > 0 then decr file_nesting_level *)
let open_nesting () = incr nesting_level
let close_nesting  () = decr nesting_level

(* Sgr stands for Select Graphic Rendition *)
module AnsiSgrCodes = struct

  (* See the list here https://en.wikipedia.org/wiki/ANSI_escape_code *)
  let normal = "\027[0m";;      (* Reset to normal. *)
  let bold = "\027[1m";;


  let output_code str =
    if Unix.isatty Unix.stdout then
      output_string stdout str
    else ()
  ;;

  let color_to_code = function
    | Black -> "30"                
    | Red -> "31"
    | Green -> "32"
    | Yellow -> "33"
    | Blue -> "34"
    | Magenta -> "35"
    | Cyan -> "36"
    | White -> "37"

  let reset_code = "\027[0m";;
  let middle_gray = "\027[0;38;5;244m";;  

  (* Note that I track the status of colors myself instead of using
     the terminal.  Thus, we prepend every change with 0; to reset
     the terminal before furthre printing. We could instead remember
     the previous status, and output only the changes that we need,
     but why bother. *)

  let to_code ({weight;color;italic;underline} as _x) =
    let code = "\027[0" in
    let code = code ^ (match weight with
        | Normal -> ""
        | Bold -> ";1"
        | Faint -> ";2") in
    let code = code ^ (match italic with
        | false -> ""
        | true -> ";3") in            
    let code = code ^ (match underline with
        | false -> ""
        | true -> ";4") in
    let code = code ^ (match color with
        | None -> ""
        | Some color -> ";" ^ (color_to_code color)) in
    (* (to_string _x) ^  *)code ^ "m"

end;;

(* Note: a part of this code could be shared with the the HTML
   one. On the other hand, the "add more entities" logic is handled
   directly in HTML, so there is no need for it there. *)

(* The terminal only remembers the last code, so we need to remember
   how weight and color adds up. Hmm, not sure about that. *)
let terminal_stag_functions prev =
  let stack = Stack.create () in
  Stack.push initial_state stack;
  let mark_open_stag m =
    let exception Not_handeld in try 
      let cur = Stack.top stack in
      let newer = match m with
        | Weight weight ->{cur with weight}
        | Color color -> {cur with color = Some color}
        | Underline underline -> {cur with underline}
        | Italic italic -> {cur with italic}
        | _ -> raise Not_handeld
      in
      Stack.push newer stack;
      AnsiSgrCodes.to_code newer
    with Not_handeld ->
      (Stack.push (Stack.top stack) stack;
       prev.Format.mark_open_stag m)
  in
  let mark_close_stag _m =
    let _ = Stack.pop stack in
    let prev = Stack.top stack in
    (AnsiSgrCodes.to_code prev)
  in
  let print_open_stag _ = assert false in
  let print_close_stag _ = assert false in
  Format.{ mark_close_stag; mark_open_stag; print_open_stag; print_close_stag }
;;

type line_characters = {
  prefix: string;               (* Prefix to change mode. *)
  vertical_bar: string;         (* │ / | *)
  right_tee: string;            (* ├ / +  *)
  horizontal_bar: string;       (* ─ / -  *)
  up_right_corner: string;      (* └ / `  *)
  postfix: string;              (* Postfix to return to normal mode. *)
}

let unicode_line_characters = {
  prefix="";
  vertical_bar = "│";           (* "\u{2502}" *)
  right_tee = "├";              (* "\u{251c}" *)
  horizontal_bar = "─";         (* "\u{2500}" *)
  up_right_corner = "└";        (* "\u{2514}" *)
  postfix = "";
};;

let vt100_line_characters = {
  prefix = "\027(0";    (* setspecg0: Switch to the graphic character set. *)
  vertical_bar = "\120";
  right_tee = "\116";
  horizontal_bar = "\113";
  up_right_corner = "\109";
  postfix = "\027(B"; (* setusg0: Return to the normal character set. *)
}
;;

let ascii_line_characters = {
  prefix = "";
  vertical_bar = "|";
  right_tee = "+";
  horizontal_bar = "-";
  up_right_corner = "`";
  postfix = ""
};;

type choice = [`Yes | `No | `Terminal | `Autodetect];;

let use_unicode: choice ref = ref `Autodetect;;

let set_use_unicode x = use_unicode := x;;

(* All the methods for line display do not work everywhere. In Emacs,
   use Unicode; in terminals, use VT100; when in doubt, display less
   pretty ASCII. *)
let rec get_line_characters () =
  (* We cache the method, which should be called only once. *)
  match !use_unicode with
  | `Yes -> unicode_line_characters
  | `No -> ascii_line_characters
  | `Terminal -> vt100_line_characters
  | `Autodetect -> begin
      let res = match Sys.getenv "TERM" with
      | exception Not_found ->
         if Unix.isatty Unix.stdout then `No
         else `Yes
      | "dumb" | "emacs" -> `Yes
      | _  when not @@ Unix.isatty Unix.stdout -> `Yes
      | "linux" | "vt100" | "konsole" | "gnome-terminal" | "xterm"
        | "xterm-256color" | "screen" | "tmux" | "cygwin" | "putty"
        | "alacritty" | "kitty" | "fbterm" ->
         `Terminal
      | s when String.starts_with ~prefix:"xterm" s -> `Terminal 
      | s when String.starts_with ~prefix:"rxvt"  s -> `Terminal 
      | s when String.starts_with ~prefix:"linux" s -> `Terminal         
      | s when String.starts_with ~prefix:"vt100" s -> `Terminal 
      | s when String.starts_with ~prefix:"vte" s ->   `Terminal
      | s when String.starts_with ~prefix:"st" s ->    `Terminal
      | s when String.starts_with ~prefix:"eterm" s -> `Terminal
      | _ -> `No            (* We don't know; be safe. *)
      in use_unicode := res;
         get_line_characters ()
    end
;;

let print_initial_indentation ~last =
  (* output_string outc (string_of_int level); *)
  match !nesting_level with
  | 0 -> ()
  | _ ->
    AnsiSgrCodes.(output_code middle_gray);      
    let lc = get_line_characters() in
    output_string stdout lc.prefix;
    for _i = 0 to (!nesting_level - 2) do
      (* String.init (2 * (level - 1)) (fun i -> *)
      output_string stdout lc.vertical_bar;
      output_char stdout ' '
    done;
    output_string stdout (if last then lc.up_right_corner else lc.right_tee);
    output_string stdout lc.horizontal_bar;
    output_string stdout lc.postfix;
    AnsiSgrCodes.(output_code reset_code);   
    


    
;;

let print_normal_indentation ~last tc =
  (* AnsiSgrCodes.(output_code stdout reset_code); *)
  AnsiSgrCodes.(output_code middle_gray);  
  let lc = get_line_characters() in
  output_string stdout lc.prefix;        
  if last then begin
    assert (!nesting_level >= 1);
    for _i = 0 to !nesting_level - 2 do
      output_string stdout lc.vertical_bar;
      output_char stdout ' '
    done;
    output_string stdout "    ";
  end
  else begin
    for _i = 0 to !nesting_level do
      output_string stdout lc.vertical_bar;
      output_char stdout ' '
    done
  end;
  output_string stdout lc.postfix;          
  AnsiSgrCodes.(output_code tc)

;;

(* Print the buffer message, taking care of properly indenting
   everything, and of outputing a last newline if there was none. *)
(* Note: I could have used a symbolc output buffer instead. *)
let printf category ~last formatstring =

  (* let givenk_:(Format.formatter -> unit) option = k in *)
  let buf = Format.make_symbolic_output_buffer () in (* Buffer.create 300 in *)
  let tag = ("[" ^ category ^ "] ") in
  let indentation = String.length tag in
  let ppf = Format.formatter_of_symbolic_output_buffer buf in
  (* Do not print terminal codes when redirecting to a file. *)
  if (Unix.isatty Unix.stdout) then begin
    let formatter_tag_functions = terminal_stag_functions (Format.pp_get_formatter_stag_functions ppf ()) in
    Format.pp_set_formatter_stag_functions ppf formatter_tag_functions;
    Format.pp_set_mark_tags ppf true
  end;

  let k ppf =
    (* Get the list of things that we have to print. *)
    Format.pp_print_flush ppf ();
    let symbolic_item_list = Format.get_symbolic_output_buffer buf in
    
    
    print_initial_indentation ~last;
    (* Begin doing the real output. *)   
    AnsiSgrCodes.(output_code bold);
    output_string stdout tag;
    AnsiSgrCodes.(output_code normal);     


    (* We are folding on the list of symbolic items, and the
       accumulator is here to "cache" things that we do not want to
       print right away. There are two things that we cache:

       - The terminal commands: we have to parse them anyway, and the
         way we produce them ensures that each command replaces the
         previous one, so we make advantage of that to only output the
         last one (we also need to remember what it was when we display
         the tree lines after a line break, to restore it when we print
         the rest of the line). It is represented as a (bool * string),
         where the string is the "current" terminal command, and bool is
         true if it was outputed.

       - The newline and following indentation: we need to track
         that to ensure that each log outputs end with a single
         newline (not 0, not two), no matter if the message was
         designed to end with a newline or not (as Frama-C does). It
         is represented as an int option, where the int is the number
         of spaces. *)
    
    let output_terminal_command = function
      | (true,_) as tc -> tc
      | (false,tc) -> output_string stdout tc; (true,tc)
    in

    let output_newline_and_indent ((_,terminal_command),newline_and_indent) =
      match newline_and_indent with
      | None -> ()
      | Some n ->
        output_string stdout "\n";
        print_normal_indentation ~last terminal_command;
        output_string stdout (String.make (n + indentation - 2) ' ')
    in

    (* The function used to fold on symbolic items. *)
    let rec do_symbolic_output_item ((terminal_command,newline_and_indent) as acc) = function
      | Format.Output_flush -> flush stdout; acc
      | Format.Output_newline -> begin
          match newline_and_indent with
          | None -> ()
          (* Two new lines in a row; we print the first, without its indentation. *)                          
          | Some _ -> output_string stdout "\n"; 
        end;
        (terminal_command,Some 0)
      | Format.(Output_spaces n | Output_indent n) -> begin
          let newline_and_indent = match newline_and_indent with
            | Some m -> Some (m + n)
            | None -> output_string stdout (String.make n ' '); None
          in terminal_command,newline_and_indent
        end
      | Format.Output_string s ->
        (* The string might be empty and only contain newline,
           spaces, and terminal_commands, in which case we do not
           want to print our newline and terminal command.

            Also we want to handle "hard" newlines and "hard" spaces
            that were not given to the format function. For all
            these reasons, we parse the string that we output.*)

        let ((terminal_command,newline_and_indent) as acc),rest = parse_for_empty_beginning acc s 0 in
        match rest with
        | "" -> acc
        | rest ->
          let terminal_command = output_terminal_command terminal_command in
          output_newline_and_indent acc;
          begin match String.index rest '\n' with
            | exception Not_found -> output_string stdout rest; (terminal_command,None)
            | i ->
              (* Print the first sentence, then continue processing for the second. *)
              let fst = String.sub rest 0 i in
              let snd = String.sub rest (i + 1) ((String.length rest) - i - 1) in
              assert(fst <> "");
              output_string stdout fst;
              let acc = (terminal_command,None) in
              let acc = do_symbolic_output_item acc Format.Output_newline in
              let acc = if snd = "" then acc else do_symbolic_output_item acc (Format.Output_string snd) in
              acc
          end

    (* We parse the string, but try to reuse the previous function on symbolic output items when feasible. *)
    and parse_for_empty_beginning acc string idx =
      (* Printf.eprintf "parsing <%s>%!\n" string; *)
      match String.get string idx with
      | exception Invalid_argument _ -> acc, ""
      | ' ' -> parse_for_empty_beginning (do_symbolic_output_item acc (Format.Output_spaces 1)) string (idx + 1)
      | '\n' -> parse_for_empty_beginning (do_symbolic_output_item acc (Format.Output_newline)) string (idx + 1)
      | '\027' ->
        parse_terminal acc string idx
      | _ -> 
        acc, String.sub string idx (String.length string - idx)

    (* We are in a terminal escape sequence, just parse it until the end. *)
    and parse_terminal (oldtc,newline_and_indent) string start_idx =
      assert (String.get string (start_idx + 1) == '[');
      let rec loop : int -> _ * _ = fun idx -> match String.get string idx with
        | ';' | '0' | '1' | '2'| '3'| '4'| '5'| '6'| '7'| '8'| '9' -> loop @@ idx + 1
        | 'm' ->  (String.sub string start_idx (1 + idx - start_idx)), idx + 1
        | c ->
          Printf.printf "Char is %c" c;
          assert false (* Invalid terminal code, or one that we do not use. *)
      in
      let new_terminal_command,idx = loop (start_idx + 2) in
      let newtc = match oldtc with
        | (true, x) when x = new_terminal_command -> oldtc
        | _ -> (false,new_terminal_command)          
      in
      parse_for_empty_beginning (newtc,newline_and_indent) string idx
    in
    let (terminal_command,_newline_and_indent) = List.fold_left do_symbolic_output_item ((true,AnsiSgrCodes.reset_code),None) symbolic_item_list in
    (* Note that we do not consider the final newline_and_indent. *)
    output_string stdout "\n";
    (* Normally the final terminal command should be a reset command. *)
    (* Note: sometimes it is not, when there is a @. in the middle of the printing command. *)
    (* assert (snd terminal_command = AnsiSgrCodes.reset_code); *)
    let _ = output_terminal_command terminal_command in
    ()
  in 
  Format.kfprintf k ppf formatstring
  
;;