Added support for hyperlinks in the goal view of the web interface.

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

diff --git a/matitaB/matita/matitadaemon.ml b/matitaB/matita/matitadaemon.ml
index 5c58db3713ab38f73bf7ccc5689dd89662ace5bc..d1a7e207226d759d1992adee1ec80c0fe21a752f 100644 (file)
--- a/matitaB/matita/matitadaemon.ml
+++ b/matitaB/matita/matitadaemon.ml
@@ -50,9 +50,10 @@ let advance text (* (?bos=false) *) =
      let _,_,metasenv,subst,_ = !status#obj in
      let txt = List.fold_left 
        (fun acc (nmeta,_ as meta) ->
-         let txt0 = Netencoding.Html.encode ~in_enc:`Enc_utf8 ()
-           (snd (ApplyTransformation.ntxt_of_cic_sequent 
-            ~metasenv ~subst ~map_unicode_to_tex:false 80 !status meta)) in
+          let txt0 = snd (ApplyTransformation.ntxt_of_cic_sequent 
+            ~metasenv ~subst ~map_unicode_to_tex:false 80 !status
+           meta) in
+          prerr_endline ("### txt0 = " ^ txt0);
          ("<B>Goal ?" ^ (string_of_int nmeta) ^ "</B>\n" ^ txt0)::acc)
        [] metasenv
      in
@@ -171,9 +172,10 @@ let callback req outchan =
                 let _,_,metasenv,subst,_ = !status#obj in
                 let txt = List.fold_left 
                   (fun acc (nmeta,_ as meta) ->
-                    let txt0 = Netencoding.Html.encode ~in_enc:`Enc_utf8 ()
-                      (snd (ApplyTransformation.ntxt_of_cic_sequent 
-                       ~metasenv ~subst ~map_unicode_to_tex:false 80 !status meta)) in
+                     let txt0 = snd (ApplyTransformation.ntxt_of_cic_sequent 
+                       ~metasenv ~subst ~map_unicode_to_tex:false 80 !status
+                      meta) in
+                     prerr_endline ("### txt0 = " ^ txt0);
                     ("<B>Goal ?" ^ (string_of_int nmeta) ^ "</B>\n" ^ txt0)::acc)
                   [] metasenv
                 in