1) removed many debug prints

[helm.git] / matitaB / matita / matitadaemon.ml

diff --git a/matitaB/matita/matitadaemon.ml b/matitaB/matita/matitadaemon.ml
index 06b465b13687243cd726888c238c8353069128b8..e9e03b0b2098b7da22d0f464a668632bb111dba3 100644 (file)
--- a/matitaB/matita/matitadaemon.ml
+++ b/matitaB/matita/matitadaemon.ml
@@ -107,12 +107,11 @@ let output_status s =
     "<meta number=\"" ^ (string_of_int metano) ^ "\">" ^ markup ^
     txt0 ^ "</meta>" ^ acc
   in
-  let res = "<metasenv>" ^
+  "<metasenv>" ^
     (Stack.fold 
       ~env:(render_sequent true) ~cont:(render_sequent false) 
       ~todo:(render_sequent false) "" s#stack) ^
     "</metasenv>"
-  in 
   (* prerr_endline ("sending metasenv:\n" ^ res); res *)
 ;;
 
@@ -508,6 +507,41 @@ let gotoBottom (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
   cgi#out_channel#commit_work() 
 ;;
 
+let gotoTop (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
+  let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in
+  let env = cgi#environment in
+  prerr_endline "executing goto Top";
+  (try 
+    let sid = Uuidm.of_string (Netcgi.Cookie.value (env#cookie "session")) in
+    let sid = HExtlib.unopt sid in
+    (*
+    cgi # set_header 
+      ~cache:`No_cache 
+      ~content_type:"text/xml; charset=\"utf-8\""
+      ();
+    *)
+    let status = MatitaAuthentication.get_status sid in
+    let uid = MatitaAuthentication.user_of_session sid in
+    let baseuri = status#baseuri in
+    let new_status = new MatitaEngine.status (Some uid) baseuri in
+    NCicLibrary.time_travel new_status;
+    let new_history = [new_status] in 
+    MatitaAuthentication.set_history sid new_history;
+    MatitaAuthentication.set_status sid new_status;
+    NCicLibrary.time_travel new_status;
+    cgi # set_header 
+      ~cache:`No_cache 
+      ~content_type:"text/xml; charset=\"utf-8\""
+      ();
+    cgi#out_channel#output_string "<response>ok</response>"
+   with _ -> 
+     (cgi#set_header ~status:`Internal_server_error 
+      ~cache:`No_cache 
+      ~content_type:"text/xml; charset=\"utf-8\"" ();
+      cgi#out_channel#output_string "<response>ok</response>");
+  cgi#out_channel#commit_work()) 
+;;
+
 let retract (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
   let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in
   let env = cgi#environment in
@@ -644,6 +678,13 @@ let start() =
       dyn_translator = (fun _ -> ""); (* not needed *)
       dyn_accept_all_conditionals = false;
     } in
+  let goto_top =
+    { Nethttpd_services.dyn_handler = (fun _ -> gotoTop);
+      dyn_activation = Nethttpd_services.std_activation `Std_activation_buffered;
+      dyn_uri = None;                 (* not needed *)
+      dyn_translator = (fun _ -> ""); (* not needed *)
+      dyn_accept_all_conditionals = false;
+    } in
   let retrieve =
     { Nethttpd_services.dyn_handler = (fun _ -> retrieve);
       dyn_activation = Nethttpd_services.std_activation `Std_activation_buffered;
@@ -706,6 +747,7 @@ let start() =
       ~handlers:[ "advance", do_advance
                 ; "retract", do_retract
                 ; "bottom", goto_bottom
+                ; "top", goto_top
                 ; "open", retrieve 
                 ; "register", do_register
                 ; "login", do_login