Matitaweb: first attempt at web UI for disambiguation.

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

diff --git a/matitaB/matita/matitadaemon.ml b/matitaB/matita/matitadaemon.ml
index c2a586120227bd3fcbc11b2aa7103b039c8580f1..9fc2b1bbcf05b30e9cc327f39ba847dc0d29b5d4 100644 (file)
--- a/matitaB/matita/matitadaemon.ml
+++ b/matitaB/matita/matitadaemon.ml
@@ -2,6 +2,7 @@ open Printf;;
 open Http_types;;
 
 exception Emphasized_error of string
+exception Ambiguous of string
 
 module Stack = Continuationals.Stack
 
@@ -362,15 +363,33 @@ 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) 
-    | GrafiteDisambiguate.Ambiguous_input (loc,choices) -> 
-        let strchoices = 
-          String.concat "\n" (List.map
-            GrafiteAst.description_of_alias choices)
-        in
-        let x,y = HExtlib.loc_of_floc loc in
-        prerr_endline (Printf.sprintf
-          "@@@ Ambiguous input at (%d,%d). Possible choices:\n\n%s\n\n@@@ End."
+    | GrafiteDisambiguate.Ambiguous_input (loc,choices) ->
+      let x,y = HExtlib.loc_of_floc loc in
+      let choice_of_alias = function
+       | GrafiteAst.Ident_alias (_,uri) -> uri, None, uri
+       | GrafiteAst.Number_alias (None,desc)
+       | GrafiteAst.Symbol_alias (_,None,desc) -> "cic:/fakeuri.def(1)", Some desc, desc
+       | GrafiteAst.Number_alias (Some uri,desc)
+       | GrafiteAst.Symbol_alias (_,Some uri,desc) -> uri, Some desc, desc
+      in
+      let tag_of_choice (uri,title,desc) =
+        match title with
+        | None -> Printf.sprintf "<choice href=\"%s\">%s</choice>"
+            uri 
+            (Netencoding.Html.encode ~in_enc:`Enc_utf8 ~prefer_name:false () desc)
+        | Some t -> Printf.sprintf "<choice href=\"%s\" title=\"%s\">%s</choice>"
+            uri 
+            (Netencoding.Html.encode ~in_enc:`Enc_utf8 ~prefer_name:false () t)
+            (Netencoding.Html.encode ~in_enc:`Enc_utf8 ~prefer_name:false () desc)
+      in
+      let strchoices = 
+        String.concat "\n" 
+          (List.map (fun x -> tag_of_choice (choice_of_alias x)) choices)
+      in
+      prerr_endline (Printf.sprintf
+        "@@@ Ambiguous input at (%d,%d). Possible choices:\n\n%s\n\n@@@ End."
           x y strchoices);
+      (*
       let pre = Netconversion.ustring_sub `Enc_utf8  0 x text in
       let err = Netconversion.ustring_sub `Enc_utf8  x (y-x) text in
       let post = Netconversion.ustring_sub `Enc_utf8 y 
@@ -381,7 +400,10 @@ let advance0 sid text =
        pre ^ "\005span class=\"error\" title=\"" ^ title ^ "\"\006" ^ err ^ "\005/span\006" ^ post in
       let marked = Netencoding.Html.encode ~in_enc:`Enc_utf8 ~prefer_name:false 
       () (html_of_matita marked) in
-      raise (Emphasized_error marked) 
+      *)
+      let strchoices = Printf.sprintf
+        "<ambiguity start=\"%d\" stop=\"%d\">%s</ambiguity>" x y strchoices
+      in raise (Ambiguous strchoices) 
    (* | End_of_file -> ...          *)
   in
   let stringbuf = Ulexing.from_utf8_string new_statements in
@@ -655,7 +677,14 @@ let advance (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
    with
   | Emphasized_error text ->
 (* | MultiPassDisambiguator.DisambiguationError (offset,errorll) -> *)
-    let body = "<response><error>" ^ text ^ "</error> </response>" in 
+    let body = "<response><error>" ^ text ^ "</error></response>" in 
+    cgi # set_header 
+      ~cache:`No_cache 
+      ~content_type:"text/xml; charset=\"utf-8\""
+      ();
+    cgi#out_channel#output_string body
+  | Ambiguous text ->
+    let body = "<response>" ^ text ^ "</response>" in 
     cgi # set_header 
       ~cache:`No_cache 
       ~content_type:"text/xml; charset=\"utf-8\""