12
12
(***********************************************************************)
14
(* $Id: format.ml,v 1.70.6.1 2007/12/18 09:19:52 weis Exp $ *)
14
(* $Id: format.ml,v 1.74 2008/09/08 12:30:19 weis Exp $ *)
16
(* A pretty-printing facility and definition of formatters for ``parallel''
17
(i.e. unrelated or independent) pretty-printing on multiple out channels. *)
16
19
(**************************************************************
24
external size_of_int : int -> size = "%identity";;
25
external int_of_size : size -> int = "%identity";;
27
external size_of_int : int -> size = "%identity"
29
external int_of_size : size -> int = "%identity"
27
32
(* Tokens are one of the following : *)
88
94
and 'a queue_cell = {
90
96
mutable tail : 'a queue_elem;
94
101
mutable insert : 'a queue_elem;
95
102
mutable body : 'a queue_elem;
98
106
(* The formatter specific tag handling functions. *)
99
107
type formatter_tag_functions = {
182
192
let peek_queue = function
183
193
| { body = Cons { head = x; }; } -> x
184
| _ -> raise Empty_queue;;
194
| _ -> raise Empty_queue
186
197
let take_queue = function
187
198
| { body = Cons { head = x; tail = tl; }; } as q ->
189
200
if tl = Nil then q.insert <- Nil; (* Maintain the invariant. *)
191
| _ -> raise Empty_queue;;
202
| _ -> raise Empty_queue
193
205
(* Enter a token in the pretty-printer queue. *)
194
206
let pp_enqueue state ({length = len} as token) =
195
207
state.pp_right_total <- state.pp_right_total + len;
196
add_queue token state.pp_queue;;
208
add_queue token state.pp_queue
198
211
let pp_clear_queue state =
199
212
state.pp_left_total <- 1; state.pp_right_total <- 1;
200
clear_queue state.pp_queue;;
213
clear_queue state.pp_queue
202
216
(* Pp_infinity: large value for default tokens size.
217
231
pretty-printing algorithm's invariants. Given that this arithmetic
218
232
correctness check is difficult and error prone and given that 1e10
219
233
+ 1 is in practice large enough, there is no need to attempt to set
220
pp_infinity to the theoretically maximum limit. Is it not worth the
234
pp_infinity to the theoretically maximum limit. It is not worth the
223
237
let pp_infinity = 1000000010;;
237
251
let real_indent = min state.pp_max_indent indent in
238
252
state.pp_current_indent <- real_indent;
239
253
state.pp_space_left <- state.pp_margin - state.pp_current_indent;
240
pp_display_blanks state state.pp_current_indent;;
254
pp_display_blanks state state.pp_current_indent
242
257
(* To force a line break inside a block: no offset is added. *)
243
258
let break_line state width = break_new_line state 0 width;;
245
260
(* To format a break that fits on the current line. *)
246
261
let break_same_line state width =
247
262
state.pp_space_left <- state.pp_space_left - width;
248
pp_display_blanks state width;;
263
pp_display_blanks state width
250
266
(* To indent no more than pp_max_indent, if one tries to open a block
251
267
beyond pp_max_indent, then the block is rejected on the left
257
273
(match bl_ty with
258
274
| Pp_fits -> () | Pp_hbox -> ()
259
275
| _ -> break_line state width)
260
| _ -> pp_output_newline state;;
276
| _ -> pp_output_newline state
262
279
(* To skip a token, if the previous line has been broken. *)
263
280
let pp_skip_token state =
265
282
match take_queue state.pp_queue with
266
283
| { elem_size = size; length = len; } ->
267
284
state.pp_left_total <- state.pp_left_total - len;
268
state.pp_space_left <- state.pp_space_left + int_of_size size;;
285
state.pp_space_left <- state.pp_space_left + int_of_size size
270
288
(**************************************************************
272
The main pretting printing functions.
290
The main pretty printing functions.
274
292
**************************************************************)
395
413
(* Print if token size is known or printing is delayed.
396
414
Size is known when not negative.
397
415
Printing is delayed when the text waiting in the queue requires
398
more room to format than exists on the current line. *)
399
let rec advance_left state =
401
match peek_queue state.pp_queue with
402
| { elem_size = size; token = tok; length = len; } ->
403
let size = int_of_size size in
406
(state.pp_right_total - state.pp_left_total <
407
state.pp_space_left)) then
409
ignore(take_queue state.pp_queue);
410
format_pp_token state (if size < 0 then pp_infinity else size) tok;
411
state.pp_left_total <- len + state.pp_left_total;
414
| Empty_queue -> ();;
416
more room to format than exists on the current line.
418
Note: [advance_loop] must be tail recursive to prevent stack overflows. *)
419
let rec advance_loop state =
420
match peek_queue state.pp_queue with
421
| {elem_size = size; token = tok; length = len} ->
422
let size = int_of_size size in
425
(state.pp_right_total - state.pp_left_total < state.pp_space_left))
427
ignore (take_queue state.pp_queue);
428
format_pp_token state (if size < 0 then pp_infinity else size) tok;
429
state.pp_left_total <- len + state.pp_left_total;
434
let advance_left state =
435
try advance_loop state with
416
439
let enqueue_advance state tok = pp_enqueue state tok; advance_left state;;
422
445
let enqueue_string_as state size s =
423
446
let len = int_of_size size in
424
enqueue_advance state (make_queue_elem size (Pp_text s) len);;
447
enqueue_advance state (make_queue_elem size (Pp_text s) len)
426
450
let enqueue_string state s =
427
451
let len = String.length s in
428
enqueue_string_as state (size_of_int len) s;;
452
enqueue_string_as state (size_of_int len) s
430
455
(* Routines for scan stack
431
456
determine sizes of blocks. *)
433
458
(* The scan_stack is never empty. *)
434
459
let scan_stack_bottom =
435
460
let q_elem = make_queue_elem (size_of_int (-1)) (Pp_text "") 0 in
436
[Scan_elem (-1, q_elem)];;
461
[Scan_elem (-1, q_elem)]
438
464
(* Set size of blocks on scan stack:
439
465
if ty = true then size of break is set else size of block is set;
468
494
| _ -> () (* scan_push is only used for breaks and boxes. *)
470
| _ -> () (* scan_stack is never empty. *);;
496
| _ -> () (* scan_stack is never empty. *)
472
499
(* Push a token on scan stack. If b is true set_size is called. *)
473
500
let scan_push state b tok =
474
501
pp_enqueue state tok;
475
502
if b then set_size state true;
476
503
state.pp_scan_stack <-
477
Scan_elem (state.pp_right_total, tok) :: state.pp_scan_stack;;
504
Scan_elem (state.pp_right_total, tok) :: state.pp_scan_stack
479
507
(* To open a new block :
480
508
the user may set the depth bound pp_max_boxes
490
518
scan_push state false elem else
491
519
if state.pp_curr_depth = state.pp_max_boxes
492
then enqueue_string state state.pp_ellipsis;;
520
then enqueue_string state state.pp_ellipsis
494
523
(* The box which is always opened. *)
495
524
let pp_open_sys_box state = pp_open_box_gen state 0 Pp_hovbox;;
497
(* Close a block, setting sizes of its subblocks. *)
526
(* Close a block, setting sizes of its sub blocks. *)
498
527
let pp_close_box state () =
499
528
if state.pp_curr_depth > 1 then
505
534
set_size state true; set_size state false
507
536
state.pp_curr_depth <- state.pp_curr_depth - 1;
510
540
(* Open a tag, pushing it on the tag stack. *)
511
541
let pp_open_tag state tag_name =
537
567
state.pp_print_close_tag tag_name;
538
568
state.pp_tag_stack <- tags
539
569
| _ -> () (* No more tag to close. *)
542
573
let pp_set_print_tags state b = state.pp_print_tags <- b;;
543
574
let pp_set_mark_tags state b = state.pp_mark_tags <- b;;
561
593
state.pp_mark_open_tag <- mot;
562
594
state.pp_mark_close_tag <- mct;
563
595
state.pp_print_open_tag <- pot;
564
state.pp_print_close_tag <- pct;;
596
state.pp_print_close_tag <- pct
566
599
(* Initialize pretty-printer. *)
567
600
let pp_rinit state =
595
629
(* To format a string. *)
596
630
let pp_print_as_size state size s =
597
631
if state.pp_curr_depth < state.pp_max_boxes
598
then enqueue_string_as state size s;;
632
then enqueue_string_as state size s
600
635
let pp_print_as state isize s =
601
pp_print_as_size state (size_of_int isize) s;;
636
pp_print_as_size state (size_of_int isize) s
603
639
let pp_print_string state s =
604
pp_print_as state (String.length s) s;;
640
pp_print_as state (String.length s) s
606
643
(* To format an integer. *)
607
644
let pp_print_int state i = pp_print_string state (string_of_int i);;
636
674
(* To get a newline when one does not want to close the current block. *)
637
675
let pp_force_newline state () =
638
676
if state.pp_curr_depth < state.pp_max_boxes then
639
enqueue_advance state (make_queue_elem (size_of_int 0) Pp_newline 0);;
677
enqueue_advance state (make_queue_elem (size_of_int 0) Pp_newline 0)
641
680
(* To format something if the line has just been broken. *)
642
681
let pp_print_if_newline state () =
643
682
if state.pp_curr_depth < state.pp_max_boxes then
644
enqueue_advance state (make_queue_elem (size_of_int 0) Pp_if_newline 0);;
683
enqueue_advance state (make_queue_elem (size_of_int 0) Pp_if_newline 0)
646
686
(* Breaks: indicate where a block may be broken.
647
687
If line is broken then offset is added to the indentation of the current
654
694
(size_of_int (- state.pp_right_total))
655
695
(Pp_break (width, offset))
657
scan_push state true elem;;
697
scan_push state true elem
659
700
let pp_print_space state () = pp_print_break state 1 0
660
and pp_print_cut state () = pp_print_break state 0 0;;
701
and pp_print_cut state () = pp_print_break state 0 0
662
704
(* Tabulation boxes. *)
663
705
let pp_open_tbox state () =
665
707
if state.pp_curr_depth < state.pp_max_boxes then
667
709
make_queue_elem (size_of_int 0) (Pp_tbegin (Pp_tbox (ref []))) 0 in
668
enqueue_advance state elem;;
710
enqueue_advance state elem
670
713
(* Close a tabulation block. *)
671
714
let pp_close_tbox state () =
675
718
let elem = make_queue_elem (size_of_int 0) Pp_tend 0 in
676
719
enqueue_advance state elem;
677
720
state.pp_curr_depth <- state.pp_curr_depth - 1
680
724
(* Print a tabulation break. *)
681
725
let pp_print_tbreak state width offset =
685
729
(size_of_int (- state.pp_right_total))
686
730
(Pp_tbreak (width, offset))
688
scan_push state true elem;;
732
scan_push state true elem
690
735
let pp_print_tab state () = pp_print_tbreak state 0 0;;
693
738
if state.pp_curr_depth < state.pp_max_boxes then
695
740
make_queue_elem (size_of_int 0) Pp_stab 0 in
696
enqueue_advance state elem;;
741
enqueue_advance state elem
698
744
(**************************************************************
713
759
let pp_set_ellipsis_text state s = state.pp_ellipsis <- s
714
and pp_get_ellipsis_text state () = state.pp_ellipsis;;
760
and pp_get_ellipsis_text state () = state.pp_ellipsis
716
763
(* To set the margin of pretty-printer. *)
718
if n < pp_infinity then n else pred pp_infinity;;
765
if n < pp_infinity then n else pred pp_infinity
720
768
let pp_set_min_space_left state n =
722
770
let n = pp_limit n in
723
771
state.pp_min_space_left <- n;
724
772
state.pp_max_indent <- state.pp_margin - state.pp_min_space_left;
727
776
(* Initially, we have :
728
777
pp_max_indent = pp_margin - pp_min_space_left, and
729
778
pp_space_left = pp_margin. *)
730
779
let pp_set_max_indent state n =
731
pp_set_min_space_left state (state.pp_margin - n);;
780
pp_set_min_space_left state (state.pp_margin - n)
732
782
let pp_get_max_indent state () = state.pp_max_indent;;
734
784
let pp_set_margin state n =
745
795
max (max (state.pp_margin - state.pp_min_space_left)
746
796
(state.pp_margin / 2)) 1 in
747
797
(* Rebuild invariants. *)
748
pp_set_max_indent state new_max_indent;;
798
pp_set_max_indent state new_max_indent
750
801
let pp_get_margin state () = state.pp_margin;;
752
803
let pp_set_formatter_output_functions state f g =
753
804
state.pp_output_function <- f; state.pp_flush_function <- g;;
754
805
let pp_get_formatter_output_functions state () =
755
(state.pp_output_function, state.pp_flush_function);;
806
(state.pp_output_function, state.pp_flush_function)
757
809
let pp_set_all_formatter_output_functions state
758
810
~out:f ~flush:g ~newline:h ~spaces:i =
759
811
pp_set_formatter_output_functions state f g;
760
812
state.pp_output_newline <- (function () -> h ());
761
state.pp_output_spaces <- (function n -> i n);;
813
state.pp_output_spaces <- (function n -> i n)
762
815
let pp_get_all_formatter_output_functions state () =
763
816
(state.pp_output_function, state.pp_flush_function,
764
state.pp_output_newline, state.pp_output_spaces);;
817
state.pp_output_newline, state.pp_output_spaces)
766
820
let pp_set_formatter_out_channel state os =
767
821
state.pp_output_function <- output os;
768
state.pp_flush_function <- (fun () -> flush os);;
822
state.pp_flush_function <- (fun () -> flush os)
770
825
(**************************************************************
825
881
state.pp_output_function blank_line 0 80;
826
882
display_blanks state (n - 80)
829
886
(* Default function to output new lines. *)
830
887
let display_newline state () = state.pp_output_function "\n" 0 1;;
832
let make_formatter f g =
833
let ff = pp_make_formatter f g ignore ignore in
834
ff.pp_output_newline <- display_newline ff;
835
ff.pp_output_spaces <- display_blanks ff;
889
(* Make a formatter with default functions to output spaces and new lines. *)
890
let make_formatter output flush =
891
let ppf = pp_make_formatter output flush ignore ignore in
892
ppf.pp_output_newline <- display_newline ppf;
893
ppf.pp_output_spaces <- display_blanks ppf;
838
897
let formatter_of_out_channel oc =
839
make_formatter (output oc) (fun () -> flush oc);;
898
make_formatter (output oc) (fun () -> flush oc)
841
901
let formatter_of_buffer b =
842
make_formatter (Buffer.add_substring b) ignore;;
902
make_formatter (Buffer.add_substring b) ignore
844
905
let stdbuf = Buffer.create 512;;
907
(* Predefined formatters. *)
846
908
let str_formatter = formatter_of_buffer stdbuf
847
909
and std_formatter = formatter_of_out_channel stdout
848
and err_formatter = formatter_of_out_channel stderr;;
910
and err_formatter = formatter_of_out_channel stderr
850
913
let flush_str_formatter () =
851
914
pp_flush_queue str_formatter false;
852
915
let s = Buffer.contents stdbuf in
853
916
Buffer.reset stdbuf;
856
920
(**************************************************************
948
1012
giving up at character number " ^ string_of_int i ^
949
1013
(if i < Sformat.length fmt
950
1014
then " (" ^ String.make 1 (Sformat.get fmt i) ^ ")."
951
else String.make 1 '.');;
1015
else String.make 1 '.')
953
1018
(* When an invalid format deserves a special error explanation. *)
954
1019
let format_invalid_arg mess fmt i = invalid_arg (giving_up mess fmt i);;
966
1031
try int_of_string s with
967
1032
| Failure s -> invalid_integer fmt i in
970
1036
(* Getting strings out of buffers. *)
971
1037
let get_buffer_out b =
972
1038
let s = Buffer.contents b in
976
1043
(* [ppf] is supposed to be a pretty-printer that outputs in buffer [b]:
977
1044
to extract contents of [ppf] as a string we flush [ppf] and get the string
979
1046
let string_out b ppf =
980
1047
pp_flush_queue ppf false;
983
1051
(* Applies [printer] to a formatter that outputs on a fresh buffer,
984
1052
then returns the resulting material. *)
986
1054
let b = Buffer.create 512 in
987
1055
let ppf = formatter_of_buffer b in
988
1056
printer ppf arg;
991
1060
(* To turn out a character accumulator into the proper string result. *)
992
1061
let implode_rev s0 = function
994
| l -> String.concat "" (List.rev (s0 :: l));;
1063
| l -> String.concat "" (List.rev (s0 :: l))
996
1066
(* [mkprintf] is the printf-like function generator: given the
997
1067
- [to_s] flag that tells if we are printing into a string,
1237
1308
let eprintf fmt = fprintf err_formatter fmt;;
1239
1310
let kbprintf k b =
1240
mkprintf false (fun _ -> formatter_of_buffer b) k;;
1311
mkprintf false (fun _ -> formatter_of_buffer b) k
1242
1314
let bprintf b = kbprintf ignore b;;
1244
1316
let ksprintf k =
1245
1317
let b = Buffer.create 512 in
1246
1318
let k ppf = k (string_out b ppf) in
1247
mkprintf true (fun _ -> formatter_of_buffer b) k;;
1319
mkprintf true (fun _ -> formatter_of_buffer b) k
1249
1322
let kprintf = ksprintf;;
1251
1324
let sprintf fmt = ksprintf (fun s -> s) fmt;;
1253
at_exit print_flush;;
added
removed
stdlib/format.ml
