]> matita.cs.unibo.it Git - helm.git/commitdiff
projects / helm.git / commitdiff
? search:
summary | shortlog | log | commit | commitdiff | tree
raw | patch | inline | side by side (parent: c3bcf78)
drawGraph ported to Helm_registry.
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Mon, 16 Feb 2004 22:59:21 +0000 (22:59 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Mon, 16 Feb 2004 22:59:21 +0000 (22:59 +0000)
helm/graphs/tools/drawGraph.conf.xml.sample [new file with mode: 0644] patch | blob
helm/graphs/tools/drawGraph.ml patch | blob | history

diff --git a/helm/graphs/tools/drawGraph.conf.xml.sample b/helm/graphs/tools/drawGraph.conf.xml.sample
new file mode 100644 (file)
index 0000000..a26b4b9
--- /dev/null
+++ b/helm/graphs/tools/drawGraph.conf.xml.sample
@@ -0,0 +1,7 @@
+<?xml version="1.0" encoding="utf-8"?>
+<helm_registry>
+  <section name="draw_graph">
+    <key name="port">58083</key>
+    <key name="dir">/projects/helm/daemons/graphs/tools</key>
+  </section>
+</helm_registry>
diff --git a/helm/graphs/tools/drawGraph.ml b/helm/graphs/tools/drawGraph.ml
index dd0e6cf5c00b2bb93318a4f708333137c261112d..1a980fede0d3559e1b0625e28539e4093584ad04 100644 (file)
--- 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
 "<html>
@@ -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;
Unnamed repository; edit this file 'description' to name the repository.