]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/http_getter/http_getter_debugger.ml
split into two major parts:
[helm.git] / helm / http_getter / http_getter_debugger.ml
index b6d1e504215ae420eb4bb5780765a3a8cb0af76c..3f9afd78c1e93ba5dbf2b50e4c431a13e1e70ac3 100644 (file)
@@ -1,5 +1,5 @@
 (*
- * Copyright (C) 2003:
+ * Copyright (C) 2003-2004:
  *    Stefano Zacchiroli <zack@cs.unibo.it>
  *    for the HELM Team http://helm.cs.unibo.it/
  *
  *  http://helm.cs.unibo.it/
  *)
 
- (* debugging settings *)
-let debug = true;;
-let debug_print s = if debug then prerr_endline ("[HTTP-Getter] " ^ s);;
+let debug = ref true
+
+(* invariant: if logfile is set, then logchan is set too *)
+let logfile = ref None
+let logchan = ref None
+
+let set_logfile f =
+  (match !logchan with None -> () | Some oc -> close_out oc);
+  match f with
+  | Some f ->
+      logfile := Some f;
+      logchan := Some (open_out f)
+  | None ->
+      logfile := None;
+      logchan := None
+
+let get_logfile () = !logfile
+
+let close_logfile () = set_logfile None
+
+let debug_print s =
+  let msg = "[HTTP-Getter] " ^ s in
+  if !debug then
+    match (!logfile, !logchan) with
+    | None, _ -> prerr_endline msg
+    | Some fname, Some oc ->
+        output_string oc msg;
+        flush oc
+    | Some _, None -> assert false