From: Wilmer Ricciotti <ricciott@cs.unibo.it>
Date: Tue, 7 Jun 2011 15:12:00 +0000 (+0000)
Subject: Removed hardcoded include paths from matitadaemon.
X-Git-Tag: make_still_working~2453
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=5a0bffcc89e1215ed051b515dc276f6b8111fc9d;p=helm.git

Removed hardcoded include paths from matitadaemon.
---

diff --git a/matitaB/matita/matitadaemon.ml b/matitaB/matita/matitadaemon.ml
index 65ddaf2cc..3d9b9d09c 100644
--- a/matitaB/matita/matitadaemon.ml
+++ b/matitaB/matita/matitadaemon.ml
@@ -45,7 +45,7 @@ let eval_statement include_paths (* (buffer : GText.buffer) *) status (* script
 let status = ref (new MatitaEngine.status "cic:/matita");;
 let history = ref [!status];;
 
-let include_paths = ["/home/barolo/matitaB/matita/lib"];;
+let include_paths = ref [];;
 
 (* <metasenv>
  *   <meta number="...">
@@ -155,20 +155,6 @@ let load_doc filename outchan =
   Http_daemon.respond ~headers:["Content-Type", contenttype] ~code:(`Code 200) ~body:s outchan
 ;;
 
-let call_service outchan =
-  try 
-   (ignore(MatitaEngine.assert_ng 
-     ~include_paths:["/home/barolo/matitaB/matita/lib"] (* ~outch:outchan *)
-    "/home/barolo/matitaB/matita/lib/basics/pts.ma");
-    prerr_endline "fatto";
-    let s = read_file "/home/barolo/matitaB/matita/lib/basics/pts.ma.mad"
-    in
-    Http_daemon.respond ~headers:["Content-Type", "text/html"] ~code:(`Code 200) ~body:s outchan
-   )
-  with
-  e -> Http_daemon.respond ~code:(`Code 500) outchan
-;;
-
 let retrieve (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
   let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in
   cgi # set_header 
@@ -182,9 +168,21 @@ let retrieve (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
       (read_file filename) in
   prerr_endline ("sending:\nBEGIN\n" ^ body ^ "\nEND");
   let body = "<file>" ^ body ^ "</file>" in
-  let _,baseuri,_,_ = 
-    Librarian.baseuri_of_script ~include_paths:[] filename
-  in
+  let baseuri, incpaths = 
+    try 
+      let root, baseuri, _fname, _tgt = 
+        Librarian.baseuri_of_script ~include_paths:[] filename in 
+      let includes =
+       try
+        Str.split (Str.regexp " ") 
+         (List.assoc "include_paths" (Librarian.load_root_file (root^"/root")))
+       with Not_found -> []
+      in
+      let rc = root :: includes in
+       List.iter (HLog.debug) rc; baseuri, rc
+     with 
+       Librarian.NoRootFor _ | Librarian.FileNotFound _ -> "",[] in
+  include_paths := incpaths;
   status := (!status)#set_baseuri baseuri;
   cgi#out_channel#output_string body;
   cgi#out_channel#commit_work()
@@ -193,7 +191,7 @@ let retrieve (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
 let advance0 text =
   let (st,new_statements,new_unparsed),(* newtext TODO *) _,parsed_len =
        (* try *)
-         eval_statement include_paths (*buffer*) !status (`Raw text)
+         eval_statement !include_paths (*buffer*) !status (`Raw text)
        (* with End_of_file -> raise Margin *)
      in
   status := st;