X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fmatita%2Fmatitadaemon.ml;h=fc8c9684e87534819f855ba1786723c347738e2a;hb=84b38ac86f1f92b91ae8913cd0dbcb5c3485dc3a;hp=eba76597e9e896805d30cd92f511ee9b9d67bbd7;hpb=92fc70ae76ae4376b7976d1dff5c9b57d1b96056;p=helm.git
diff --git a/matitaB/matita/matitadaemon.ml b/matitaB/matita/matitadaemon.ml
index eba76597e..fc8c9684e 100644
--- a/matitaB/matita/matitadaemon.ml
+++ b/matitaB/matita/matitadaemon.ml
@@ -3,6 +3,7 @@ open Http_types;;
exception Emphasized_error of string
exception Disamb_error of string
+exception Generic_error of string
module Stack = Continuationals.Stack
@@ -482,6 +483,8 @@ let advance0 sid text =
let status = status#reset_disambiguate_db () in
let (st,new_statements,new_unparsed),parsed_len =
let rec do_exc = function
+ | MatitaEngine.EnrichedWithStatus (e,_) -> do_exc e
+ | NCicTypeChecker.TypeCheckerFailure s -> raise (Generic_error (Lazy.force s))
| HExtlib.Localized (floc,e) ->
let x, y = HExtlib.loc_of_floc floc in
let pre = Netconversion.ustring_sub `Enc_utf8 0 x text in
@@ -573,7 +576,8 @@ let advance0 sid text =
| GrafiteDisambiguate.Error l -> raise (Disamb_error (xml_of_disamb_error l))
(* | End_of_file -> ... *)
| e ->
- prerr_endline ("matitadaemon *** Unhandled exception " ^ Printexc.to_string e);
+ (* prerr_endline ("matitadaemon *** Unhandled exception " ^ Printexc.to_string e); *)
+ prerr_endline ("matitadaemon *** Unhandled exception " ^ snd (MatitaExcPp.to_string e));
raise e
in
@@ -596,7 +600,7 @@ let advance0 sid text =
Netencoding.Html.encode ~in_enc:`Enc_utf8 ~prefer_name:false
() (html_of_matita new_statements), new_unparsed, st
-let register (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
+let register (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in
let _env = cgi#environment in
@@ -629,7 +633,7 @@ let register (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
cgi#out_channel#commit_work()
;;
-let login (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
+let login (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in
let env = cgi#environment in
@@ -660,7 +664,7 @@ let login (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
cgi#out_channel#commit_work()
;;
-let logout (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
+let logout (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in
let env = cgi#environment in
(try
@@ -685,7 +689,7 @@ let logout (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
exception File_already_exists;;
-let save (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
+let save (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in
let env = cgi#environment in
(try
@@ -794,7 +798,7 @@ let initiate_commit (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
cgi#out_channel#commit_work()
;;
-let svn_update (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
+let svn_update (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in
let env = cgi#environment in
let sid = Uuidm.of_string (Netcgi.Cookie.value (env#cookie "session")) in
@@ -875,9 +879,16 @@ let advance (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
();
cgi#out_channel#output_string body
with
+ | Generic_error text ->
+ let body = "" ^ text ^ "" in
+ cgi # set_header
+ ~cache:`No_cache
+ ~content_type:"text/xml; charset=\"utf-8\""
+ ();
+ cgi#out_channel#output_string body
| Emphasized_error text ->
(* | MultiPassDisambiguator.DisambiguationError (offset,errorll) -> *)
- let body = "" ^ text ^ "" in
+ let body = "" ^ text ^ "" in
cgi # set_header
~cache:`No_cache
~content_type:"text/xml; charset=\"utf-8\""
@@ -907,7 +918,7 @@ let advance (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
cgi#out_channel#commit_work()
;;
-let gotoBottom (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
+let gotoBottom (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in
let env = cgi#environment in
(* (try *)
@@ -968,7 +979,7 @@ let gotoBottom (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
cgi#out_channel#commit_work()
;;
-let gotoTop (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
+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";
@@ -1005,7 +1016,7 @@ let gotoTop (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
cgi#out_channel#commit_work()
;;
-let retract (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
+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
(try
@@ -1050,7 +1061,7 @@ let retract (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
;;
-let viewLib (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
+let viewLib (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in
let env = cgi#environment in
@@ -1090,7 +1101,7 @@ let viewLib (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
;;
-let resetLib (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
+let resetLib (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in
MatitaAuthentication.reset ();
cgi # set_header