From f93c0057cfca9610e40f9214b286174a041e422a Mon Sep 17 00:00:00 2001 From: =?utf8?q?Kim=20Nguy=E1=BB=85n?= Date: Mon, 4 Mar 2013 18:52:37 +0100 Subject: [PATCH] Replace internal use of str_formatter with local buffered formatter in Atom.print and Formula.print. Use of str_formatter in both was not re-entrant and caused printing error when displaying a formula containing an Atom. --- src/auto/ata.ml | 62 +++++++++++++++++++++++++++++-------------------- 1 file changed, 37 insertions(+), 25 deletions(-) diff --git a/src/auto/ata.ml b/src/auto/ata.ml index aa4fb38..e07aa3f 100644 --- a/src/auto/ata.ml +++ b/src/auto/ata.ml @@ -14,7 +14,7 @@ (***********************************************************************) (* - Time-stamp: + Time-stamp: *) INCLUDE "utils.ml" @@ -45,11 +45,15 @@ struct let make_ctx a b c d e = { left = a; right = b; up1 = c; up2 = d; epsilon = e } - include Hcons.Make(Node) + include Hcons.Make(Node) + let _pr_buff = Buffer.create 10 + let _str_fmt = formatter_of_buffer _pr_buff + let _flush_str_fmt () = pp_print_flush _str_fmt (); + let s = Buffer.contents _pr_buff in + Buffer.clear _pr_buff; s let print ppf a = - let _ = flush_str_formatter() in - let fmt = str_formatter in + let _ = _flush_str_fmt () in let m, b, s = a.node in let dir,num = @@ -60,9 +64,9 @@ struct | `Up1 -> Pretty.up_arrow, Pretty.subscript 1 | `Up2 -> Pretty.up_arrow, Pretty.subscript 2 in - fprintf fmt "%s%s" dir num; - State.print fmt s; - let str = flush_str_formatter() in + fprintf _str_fmt "%s%s" dir num; + State.print _str_fmt s; + let str = _flush_str_fmt () in if b then fprintf ppf "%s" str else Pretty.pp_overline ppf str @@ -132,17 +136,20 @@ let add_trans a q s f = in Hashtbl.replace a.transitions q ntrs +let _pr_buff = Buffer.create 50 +let _str_fmt = formatter_of_buffer _pr_buff +let _flush_str_fmt () = pp_print_flush _str_fmt (); + let s = Buffer.contents _pr_buff in + Buffer.clear _pr_buff; s let print fmt a = fprintf fmt - "Unique ID: %i@\n\ - States %a@\n\ + "\nInternal UID: %i@\n\ + States: %a@\n\ Selection states: %a@\n\ Alternating transitions:@\n" (a.id :> int) StateSet.print a.states -(* StateSet.print a.top_states - StateSet.print a.bottom_states *) StateSet.print a.selection_states; let trs = Hashtbl.fold @@ -154,21 +161,26 @@ let print fmt a = let c = State.compare q1 q2 in - (if c == 0 then QNameSet.compare s1 s2 else c)) trs in - let sfmt = str_formatter in - let _ = flush_str_formatter () in - let strs_strings, maxs = List.fold_left (fun (accl, accm) (q, s, f) -> - let s1 = State.print sfmt q; flush_str_formatter () in - let s2 = QNameSet.print sfmt s; flush_str_formatter () in - let s3 = SFormula.print sfmt f; flush_str_formatter () in - ( (s1, s2, s3) :: accl, - max - accm (2 + String.length s1 + String.length s2)) - ) ([], 0) sorted_trs + let _ = _flush_str_fmt () in + let strs_strings, max_pre, max_all = List.fold_left (fun (accl, accp, acca) (q, s, f) -> + let s1 = State.print _str_fmt q; _flush_str_fmt () in + let s2 = QNameSet.print _str_fmt s; _flush_str_fmt () in + let s3 = SFormula.print _str_fmt f; _flush_str_fmt () in + let pre = Pretty.length s1 + Pretty.length s2 in + let all = Pretty.length s3 in + ( (q, s1, s2, s3) :: accl, max accp pre, max acca all) + ) ([], 0, 0) sorted_trs in - List.iter (fun (s1, s2, s3) -> - fprintf fmt "%s, %s" s1 s2; - fprintf fmt "%s" (Pretty.padding (maxs - String.length s1 - String.length s2 - 2)); - fprintf fmt "%s %s@\n" Pretty.right_arrow s3) strs_strings + let line = Pretty.line (max_all + max_pre + 6) in + let prev_q = ref State.dummy in + List.iter (fun (q, s1, s2, s3) -> + if !prev_q != q && !prev_q != State.dummy then fprintf fmt " %s\n%!" line; + prev_q := q; + fprintf fmt " %s, %s" s1 s2; + fprintf fmt "%s" (Pretty.padding (max_pre - Pretty.length s1 - Pretty.length s2)); + fprintf fmt " %s %s@\n%!" Pretty.right_arrow s3; + ) strs_strings; + fprintf fmt " %s\n%!" line (* [complete transitions a] ensures that for each state q -- 2.17.1