diff options
| author | Alasdair Armstrong | 2019-02-12 18:18:05 +0000 |
|---|---|---|
| committer | Alasdair Armstrong | 2019-02-12 18:18:05 +0000 |
| commit | 24fc989891ad266eae642815646294279e2485ca (patch) | |
| tree | d533fc26b5980d1144ee4d7849d3dd0f2a1b0e95 /src/util.ml | |
| parent | b847a472a1f853d783d1af5f8eb033b97f33be5b (diff) | |
| parent | 974494b1dda38c1ee5c1502cc6e448e67a7374ac (diff) | |
Merge remote-tracking branch 'origin/asl_flow2' into sail2
Diffstat (limited to 'src/util.ml')
| -rw-r--r-- | src/util.ml | 30 |
1 files changed, 30 insertions, 0 deletions
diff --git a/src/util.ml b/src/util.ml index 5e5654d1..0ff00df1 100644 --- a/src/util.ml +++ b/src/util.ml @@ -96,6 +96,7 @@ let opt_warnings = ref true let opt_colors = ref true +let opt_verbosity = ref 0 let rec last = function | [x] -> x @@ -465,3 +466,32 @@ let log_line str line msg = "\n[" ^ (str ^ ":" ^ string_of_int line |> blue |> clear) ^ "] " ^ msg let header str n = "\n" ^ str ^ "\n" ^ String.make (String.length str - 9 * n) '=' + +let verbose_endline level str = + if level >= !opt_verbosity then + prerr_endline str + else + () + +let progress prefix msg n total = + if !opt_verbosity > 0 then + let len = truncate ((float n /. float total) *. 50.0) in + let percent = truncate ((float n /. float total) *. 100.0) in + let msg = + if String.length msg <= 20 then + msg ^ ")" ^ String.make (20 - String.length msg) ' ' + else + String.sub msg 0 17 ^ "...)" + in + let str = prefix ^ "[" ^ String.make len '=' ^ String.make (50 - len) ' ' ^ "] " + ^ string_of_int percent ^ "%" + ^ " (" ^ msg + in + prerr_string str; + if n = total then + prerr_char '\n' + else + prerr_string ("\x1B[" ^ string_of_int (String.length str) ^ "D"); + flush stderr + else + () |
