From: Claudio Sacerdoti Coen Date: Mon, 16 Feb 2004 22:59:21 +0000 (+0000) Subject: drawGraph ported to Helm_registry. X-Git-Tag: v0_0_4~181 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=ebc70db9d8720a6f776e7d7c09c7833e500b9eb3;p=helm.git drawGraph ported to Helm_registry. --- diff --git a/helm/graphs/tools/drawGraph.conf.xml.sample b/helm/graphs/tools/drawGraph.conf.xml.sample new file mode 100644 index 000000000..a26b4b990 --- /dev/null +++ b/helm/graphs/tools/drawGraph.conf.xml.sample @@ -0,0 +1,7 @@ + + +
+ 58083 + /projects/helm/daemons/graphs/tools +
+ diff --git a/helm/graphs/tools/drawGraph.ml b/helm/graphs/tools/drawGraph.ml index dd0e6cf5c..1a980fede 100644 --- a/helm/graphs/tools/drawGraph.ml +++ b/helm/graphs/tools/drawGraph.ml @@ -28,11 +28,9 @@ open Printf;; let debug = true;; let debug_print s = if debug then prerr_endline s;; +let configuration_file = "/projects/helm/etc/drawGraph.conf.xml";; + let daemon_name = "Draw Graph";; -let default_port = 48083;; -let default_dir = "/projects/helm/graphs/tools";; -let port_env_var = "DRAW_GRAPH_PORT";; -let dir_env_var = "DRAW_GRAPH_DIR";; let wget url fname = prerr_endline (sprintf "DEBUG: wgetting url '%s'" url); @@ -41,16 +39,6 @@ let wget url fname = close_out oc ;; -let port = - try - int_of_string (Sys.getenv port_env_var) - with - | Not_found -> default_port - | Failure "int_of_string" -> - prerr_endline "Warning: invalid port, reverting to default"; - default_port -in -let dir = try Sys.getenv dir_env_var with Not_found -> default_dir in let errmsg = sprintf " @@ -102,7 +90,9 @@ let callback (req: Http_types.request) outchan = ~body:(sprintf "Parameter '%s' is missing" attr_name) outchan in -Sys.chdir dir; +Helm_registry.load_from configuration_file; +let port = Helm_registry.get_int "draw_graph.port" in +Sys.chdir (Helm_registry.get "draw_graph.dir"); printf "%s started and listening on port %d\n" daemon_name port; printf "current directory is %s\n" (Sys.getcwd ()); flush stdout;