From 1c57abfd96b2a0d027881a7c81d2ae9751f7be56 Mon Sep 17 00:00:00 2001
From: Wilmer Ricciotti <ricciott@cs.unibo.it>
Date: Thu, 20 Oct 2011 10:45:34 +0000
Subject: [PATCH] Matitaweb: added preliminary support for interactive
 disambiguation. Ambiguous expressions are reported to the client and
 highlighted. The possible interpretations are shown in stderr.

---
 matitaB/matita/matitaGui.ml    |  4 ++--
 matitaB/matita/matitadaemon.ml | 22 +++++++++++++++++++++-
 matitaB/matita/matitaweb.js    |  2 +-
 3 files changed, 24 insertions(+), 4 deletions(-)

diff --git a/matitaB/matita/matitaGui.ml b/matitaB/matita/matitaGui.ml
index 7a05e13ff..759ffa5ff 100644
--- a/matitaB/matita/matitaGui.ml
+++ b/matitaB/matita/matitaGui.ml
@@ -1273,11 +1273,11 @@ let interactive_ast_choice () ts =
 
 let _ =
   (* disambiguator callbacks *)
-  Disambiguate.set_choose_uris_callback
+  (* Disambiguate.set_choose_uris_callback
    (fun ~selection_mode ?ok ?(enable_button_for_non_vars=false) ~title ~msg ->
      interactive_uri_choice ~selection_mode ?ok_label:ok ~title ~msg ());
   Disambiguate.set_choose_interp_callback (interactive_interp_choice ());
-  Disambiguate.set_choose_disamb_callback (interactive_ast_choice ());
+  Disambiguate.set_choose_disamb_callback (interactive_ast_choice ());*)
   (* gtk initialization *)
   GtkMain.Rc.add_default_file BuildTimeConf.gtkrc_file; (* loads gtk rc *)
   ignore (GMain.Main.init ())
diff --git a/matitaB/matita/matitadaemon.ml b/matitaB/matita/matitadaemon.ml
index c92811c4e..c2a586120 100644
--- a/matitaB/matita/matitadaemon.ml
+++ b/matitaB/matita/matitadaemon.ml
@@ -362,8 +362,28 @@ 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."
+          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 
+         (Netconversion.ustring_length `Enc_utf8 text - y) text in
+      let title = "Disambiguation Error" in
+      (* let title = "" in *)
+      let marked = 
+	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) 
    (* | End_of_file -> ...          *)
-   in
+  in
   let stringbuf = Ulexing.from_utf8_string new_statements in
   let interpr = GrafiteDisambiguate.get_interpr st#disambiguate_db in
   let outstr = ref "" in
diff --git a/matitaB/matita/matitaweb.js b/matitaB/matita/matitaweb.js
index fedaaf7fb..ccb2f3744 100644
--- a/matitaB/matita/matitaweb.js
+++ b/matitaB/matita/matitaweb.js
@@ -233,7 +233,7 @@ function debug(txt)
 	// but google chrome's innerText is, in a sense, "write only"
 	// what should we do?
         // logarea.innerText = txt + "\n" + logarea.innerText;
-        logtxt = logtxt + "\n" + txt;
+        logtxt = /* logtxt + "\n" +*/ txt;
 }
 
 function showLog() {
-- 
2.39.2