Matitaweb:

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

diff --git a/matitaB/matita/matitadaemon.ml b/matitaB/matita/matitadaemon.ml
index 14bcf1db6d9b757d34c50263f8fd26194cef33e3..6d71ec6bc4f63c7b89d438da264f3b40e2ca3811 100644 (file)
--- a/matitaB/matita/matitadaemon.ml
+++ b/matitaB/matita/matitadaemon.ml
@@ -2,7 +2,7 @@ open Printf;;
 open Http_types;;
 
 exception Emphasized_error of string
-exception Ambiguous of string
+exception Disamb_error of string
 
 module Stack = Continuationals.Stack
 
@@ -401,6 +401,45 @@ let retrieve (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
   cgi#out_channel#commit_work()
 ;;
 
+let xml_of_disamb_error l =
+  let mk_alias = function
+  | GrafiteAst.Ident_alias (_,uri) -> "href=\"" ^ uri ^ "\""
+  | GrafiteAst.Symbol_alias (_,uri,desc) 
+  | GrafiteAst.Number_alias (uri,desc) -> 
+      let uri = try HExtlib.unopt uri with _ -> "cic:/fakeuri.def(1)" in
+        "href=\"" ^ uri ^ "\" title=\"" ^ 
+        (Netencoding.Html.encode ~in_enc:`Enc_utf8 ~prefer_name:false () desc)
+        ^ "\""
+  in
+
+  let mk_interpr (loc,a) =
+    let x,y = HExtlib.loc_of_floc loc in
+    Printf.sprintf "<interpretation start=\"%d\" stop=\"%d\" %s />"
+      x y (mk_alias a)
+  in
+
+  let mk_failure (il,loc,msg) =
+    let x,y = HExtlib.loc_of_floc loc in
+    Printf.sprintf "<failure start=\"%d\" stop=\"%d\" title=\"%s\">%s</failure>"
+      x y (Netencoding.Html.encode ~in_enc:`Enc_utf8 ~prefer_name:false () msg)
+      (String.concat "" (List.map mk_interpr il))
+  in
+
+  let mk_choice (a,fl) = 
+    let fl' = String.concat "" (List.map mk_failure fl) in
+    match a with
+    | None -> "<choice>" ^ fl' ^ "</choice>"
+    | Some a -> Printf.sprintf "<choice %s>%s</choice>" (mk_alias a) fl'
+  in
+
+  let mk_located (loc,cl) =
+    let x,y = HExtlib.loc_of_floc loc in
+    Printf.sprintf "<choicepoint start=\"%d\" stop=\"%d\">%s</choicepoint>"
+      x y (String.concat "" (List.map mk_choice cl))
+  in
+  "<disamberror>" ^ (String.concat "" (List.map mk_located l)) ^ "</disamberror>"
+;;
+
 let advance0 sid text =
   let status = MatitaAuthentication.get_status sid in
   let history = MatitaAuthentication.get_history sid in
@@ -473,7 +512,8 @@ let advance0 sid text =
       *)
       let strchoices = Printf.sprintf
         "<ambiguity start=\"%d\" stop=\"%d\">%s</ambiguity>" x y strchoices
-      in raise (Ambiguous strchoices) 
+      in raise (Disamb_error strchoices)
+   | GrafiteDisambiguate.Error l -> raise (Disamb_error (xml_of_disamb_error l))
    (* | End_of_file -> ...          *)
   in
   MatitaAuthentication.set_status sid st;
@@ -746,7 +786,7 @@ let advance (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
       ~content_type:"text/xml; charset=\"utf-8\""
       ();
     cgi#out_channel#output_string body
-  | Ambiguous text ->
+  | Disamb_error text -> 
     let body = "<response>" ^ text ^ "</response>" in 
     cgi # set_header 
       ~cache:`No_cache 
@@ -773,7 +813,7 @@ let gotoBottom (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
 
     let error_msg = function
       | Emphasized_error text -> "<localized>" ^ text ^ "</localized>" 
-      | Ambiguous text -> (* <ambiguity> *) text
+      | Disamb_error text -> text
       | End_of_file _ -> (* not an error *) ""
       | e -> (* unmanaged error *)
           "<error>" ^