Matitaweb: Fixed a bug in matitaweb.js concerning disambiguation and escaping.

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

diff --git a/matitaB/matita/matitadaemon.ml b/matitaB/matita/matitadaemon.ml
index 9fc2b1bbcf05b30e9cc327f39ba847dc0d29b5d4..a53d24f676ae3c3ec9a86e8182700e1a4aa9942c 100644 (file)
--- a/matitaB/matita/matitadaemon.ml
+++ b/matitaB/matita/matitadaemon.ml
@@ -363,6 +363,14 @@ let advance0 sid text =
       let marked = Netencoding.Html.encode ~in_enc:`Enc_utf8 ~prefer_name:false 
       () (html_of_matita marked) in
       raise (Emphasized_error marked) 
+    | NTacStatus.Error (s,None) as e ->
+        prerr_endline 
+          ("NTacStatus.Error " ^ (Lazy.force s));
+        raise e
+    | NTacStatus.Error (s,Some exc) as e ->
+        prerr_endline 
+          ("NTacStatus.Error " ^ Lazy.force s ^ " -- " ^ (Printexc.to_string exc));
+        raise e
     | GrafiteDisambiguate.Ambiguous_input (loc,choices) ->
       let x,y = HExtlib.loc_of_floc loc in
       let choice_of_alias = function