(* $Id$
|
(* $Id: util.sml 7 2007-10-31 05:39:12Z tbourke $
|
*)
|
*)
|
|
|
structure Util :
|
structure Util :
|
sig
|
sig
|
val warn : string list -> unit
|
val warn : string list -> unit
|
val abort : string list -> 'a
|
val abort : string list -> 'a
|
|
|
val debug : (Settings.debug_priority * (unit -> string list)) -> unit
|
val debug : (Settings.debug_priority * (unit -> string list)) -> unit
|
|
|
val debugAll : (unit -> string list) -> unit
|
val debugAll : (unit -> string list) -> unit
|
val debugVeryDetailed : (unit -> string list) -> unit
|
val debugVeryDetailed : (unit -> string list) -> unit
|
val debugDetailed : (unit -> string list) -> unit
|
val debugDetailed : (unit -> string list) -> unit
|
val debugOutline : (unit -> string list) -> unit
|
val debugOutline : (unit -> string list) -> unit
|
|
|
(* show borders *)
|
(* show borders *)
|
val debugSect : (Settings.debug_priority * (unit -> string list)) -> unit
|
val debugSect : (Settings.debug_priority * (unit -> string list)) -> unit
|
val debugSubsect : (Settings.debug_priority * (unit -> string list)) -> unit
|
val debugSubsect : (Settings.debug_priority * (unit -> string list)) -> unit
|
|
|
val debugIndent : (Settings.debug_priority * (unit -> string list)) -> unit
|
val debugIndent : (Settings.debug_priority * (unit -> string list)) -> unit
|
val debugOutdent : (Settings.debug_priority * (unit -> string list)) -> unit
|
val debugOutdent : (Settings.debug_priority * (unit -> string list)) -> unit
|
|
|
end
|
end
|
=
|
=
|
let structure TIO = TextIO
|
let structure TIO = TextIO
|
in
|
in
|
struct
|
struct
|
val indent = ref 0
|
val indent = ref 0
|
val indentAmount = 3;
|
val indentAmount = 3;
|
|
|
val sect = StringCvt.padLeft #"*" 71 "\n"
|
val sect = StringCvt.padLeft #"*" 71 "\n"
|
val subsect = StringCvt.padLeft #"-" 71 "\n"
|
val subsect = StringCvt.padLeft #"-" 71 "\n"
|
|
|
fun warn msg = (TIO.output (TIO.stdErr,
|
fun warn msg = (TIO.output (TIO.stdErr,
|
String.concat (Settings.progName::":"::msg));
|
String.concat (Settings.progName::":"::msg));
|
TIO.output (TIO.stdErr, "\n"))
|
TIO.output (TIO.stdErr, "\n"))
|
|
|
fun abort msg = (TIO.output (TIO.stdErr,
|
fun abort msg = (TIO.output (TIO.stdErr,
|
String.concat (Settings.progName::":"::msg));
|
String.concat (Settings.progName::":"::msg));
|
TIO.output (TIO.stdErr, "\n");
|
TIO.output (TIO.stdErr, "\n");
|
OS.Process.exit (OS.Process.failure))
|
OS.Process.exit (OS.Process.failure))
|
|
|
fun print (indent, lazystrs) = case lazystrs ()
|
fun print (indent, lazystrs) = case lazystrs ()
|
of [] => ()
|
of [] => ()
|
| strs => (TIO.output (TIO.stdErr, StringCvt.padLeft #" " indent "");
|
| strs => (TIO.output (TIO.stdErr, StringCvt.padLeft #" " indent "");
|
app (fn s=> TIO.output (TIO.stdErr, s)) strs;
|
app (fn s=> TIO.output (TIO.stdErr, s)) strs;
|
TIO.output (TIO.stdErr, "\n"))
|
TIO.output (TIO.stdErr, "\n"))
|
|
|
fun debug (priority, lazystrs) =
|
fun debug (priority, lazystrs) =
|
if Settings.showDebug (priority)
|
if Settings.showDebug (priority)
|
then print (!indent, lazystrs) else ()
|
then print (!indent, lazystrs) else ()
|
|
|
fun debugSect (priority, lazystrs) =
|
fun debugSect (priority, lazystrs) =
|
if Settings.showDebug (priority)
|
if Settings.showDebug (priority)
|
then (TIO.output (TIO.stdErr, sect);
|
then (TIO.output (TIO.stdErr, sect);
|
print (!indent, lazystrs))
|
print (!indent, lazystrs))
|
else ()
|
else ()
|
|
|
fun debugSubsect (priority, lazystrs) =
|
fun debugSubsect (priority, lazystrs) =
|
if Settings.showDebug (priority)
|
if Settings.showDebug (priority)
|
then (TIO.output (TIO.stdErr, subsect);
|
then (TIO.output (TIO.stdErr, subsect);
|
print (!indent, lazystrs))
|
print (!indent, lazystrs))
|
else ()
|
else ()
|
|
|
fun debugIndent (priority, lazystrs) =
|
fun debugIndent (priority, lazystrs) =
|
if Settings.showDebug (priority)
|
if Settings.showDebug (priority)
|
then (print (!indent, lazystrs);
|
then (print (!indent, lazystrs);
|
indent := (!indent) + indentAmount)
|
indent := (!indent) + indentAmount)
|
else ()
|
else ()
|
|
|
fun debugOutdent (priority, lazystrs) =
|
fun debugOutdent (priority, lazystrs) =
|
if Settings.showDebug (priority)
|
if Settings.showDebug (priority)
|
then (indent := (!indent) - indentAmount;
|
then (indent := (!indent) - indentAmount;
|
print (!indent, lazystrs))
|
print (!indent, lazystrs))
|
else ()
|
else ()
|
|
|
fun debugAll ls = debug (Settings.All, ls)
|
fun debugAll ls = debug (Settings.All, ls)
|
fun debugVeryDetailed ls = debug (Settings.VeryDetailed, ls)
|
fun debugVeryDetailed ls = debug (Settings.VeryDetailed, ls)
|
fun debugDetailed ls = debug (Settings.Detailed, ls)
|
fun debugDetailed ls = debug (Settings.Detailed, ls)
|
fun debugOutline ls = debug (Settings.Outline, ls)
|
fun debugOutline ls = debug (Settings.Outline, ls)
|
end
|
end
|
end
|
end
|
|
|
|
|