diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/explore.ml | 18 | ||||
| -rw-r--r-- | lib/explore.mli | 2 | ||||
| -rw-r--r-- | lib/pp.ml4 | 19 | ||||
| -rw-r--r-- | lib/pp.mli | 3 |
4 files changed, 23 insertions, 19 deletions
diff --git a/lib/explore.ml b/lib/explore.ml index 407bf1e91c..e353c90706 100644 --- a/lib/explore.ml +++ b/lib/explore.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Format +open Pp (*s Definition of a search problem. *) @@ -14,20 +14,20 @@ module type SearchProblem = sig type state val branching : state -> state list val success : state -> bool - val pp : state -> unit + val pp : state -> std_ppcmds end module Make = functor(S : SearchProblem) -> struct type position = int list - let pp_position p = + let msg_with_position p pp = let rec pp_rec = function - | [] -> () - | [i] -> printf "%d" i - | i :: l -> pp_rec l; printf ".%d" i + | [] -> mt () + | [i] -> int i + | i :: l -> pp_rec l ++ str "." ++ int i in - open_hbox (); pp_rec p; close_box () + msg_debug (h 0 (pp_rec p) ++ pp) (*s Depth first search. *) @@ -40,7 +40,7 @@ module Make = functor(S : SearchProblem) -> struct let debug_depth_first s = let rec explore p s = - pp_position p; S.pp s; + msg_with_position p (S.pp s); if S.success s then s else explore_many 1 p (S.branching s) and explore_many i p = function | [] -> raise Not_found @@ -83,7 +83,7 @@ module Make = functor(S : SearchProblem) -> struct explore q | s :: l -> let ps = i::p in - pp_position ps; S.pp s; + msg_with_position ps (S.pp s); if S.success s then s else enqueue (succ i) p (push (ps,s) q) l in enqueue 1 [] empty [s] diff --git a/lib/explore.mli b/lib/explore.mli index e64459f106..a292fd83ea 100644 --- a/lib/explore.mli +++ b/lib/explore.mli @@ -27,7 +27,7 @@ module type SearchProblem = sig val success : state -> bool - val pp : state -> unit + val pp : state -> Pp.std_ppcmds end diff --git a/lib/pp.ml4 b/lib/pp.ml4 index 4fc53270cb..ff1973846a 100644 --- a/lib/pp.ml4 +++ b/lib/pp.ml4 @@ -275,17 +275,15 @@ let pp_dirs ft = (* pretty print on stdout and stderr *) (* Special chars for emacs, to detect warnings inside goal output *) -let emacs_warning_start_string = String.make 1 (Char.chr 254) -let emacs_warning_end_string = String.make 1 (Char.chr 255) +let emacs_quote_start = String.make 1 (Char.chr 254) +let emacs_quote_end = String.make 1 (Char.chr 255) -let warnstart() = - if not !print_emacs then mt() else str emacs_warning_start_string +let emacs_quote strm = + if !print_emacs then + [< str emacs_quote_start; hov 0 strm; str emacs_quote_end >] + else hov 0 strm -let warnend() = - if not !print_emacs then mt() else str emacs_warning_end_string - -let warnbody strm = - [< warnstart() ; hov 0 (str "Warning: " ++ strm) ; warnend() >] +let warnbody strm = emacs_quote (str "Warning: " ++ strm) (* pretty printing functions WITHOUT FLUSH *) let pp_with ft strm = @@ -334,6 +332,9 @@ let msgerr x = msg_with !err_ft x let msgerrnl x = msgnl_with !err_ft x let msg_warning x = msg_warning_with !err_ft x +(* Same specific display in emacs as warning, but without the "Warning:" *) +let msg_debug x = msgnl (emacs_quote x) + let string_of_ppcmds c = msg_with Format.str_formatter c; Format.flush_str_formatter () diff --git a/lib/pp.mli b/lib/pp.mli index 2fd62d55ae..112d976552 100644 --- a/lib/pp.mli +++ b/lib/pp.mli @@ -114,6 +114,9 @@ val msgerr : std_ppcmds -> unit val msgerrnl : std_ppcmds -> unit val msg_warning : std_ppcmds -> unit +(** Same specific display in emacs as warning, but without the "Warning:" **) +val msg_debug : std_ppcmds -> unit + val string_of_ppcmds : std_ppcmds -> string (** {6 Location management. } *) |