Preliminary version of matitaweb handling multiple goals in the sequent view.

diff --git a/matitaB/matita/matitadaemon.ml b/matitaB/matita/matitadaemon.ml
index 3e37febbd0d759a59e08c29d2e484fdcafd50cdb..b8b3a1eb2111882740d602f527704714ee34c2e7 100644 (file)
--- a/matitaB/matita/matitadaemon.ml
+++ b/matitaB/matita/matitadaemon.ml
@@ -37,7 +37,24 @@ let history = ref [!status];;
 
 let include_paths = ["/home/barolo/matitaB/matita/lib"];;
 
-let html_of_status s =
+(* lista [meta n., goal; meta n., goal; ... ] *)
+(* "item1#item2#...#" *)
+
+let output_status s =
+  let _,_,metasenv,subst,_ = s#obj in
+  List.fold_left
+    (fun acc (nmeta,_ as meta) -> 
+       let txt0 = snd (ApplyTransformation.ntxt_of_cic_sequent 
+         ~metasenv ~subst ~map_unicode_to_tex:false 80 s meta)
+       in
+       (*let txt0 = Netencoding.Html.encode ~in_enc:`Enc_utf8 () txt0 in*)
+       prerr_endline ("prima dell'encoding: BEGIN\n" ^ txt0 ^ "\nEND");
+       let txt0 = Netencoding.Url.encode ~plus:false txt0 in
+       (string_of_int nmeta) ^ "|" ^ txt0 ^ "#" ^ acc)
+    "" metasenv
+;;
+
+(* let html_of_status s =
   let _,_,metasenv,subst,_ = s#obj in
   let txt = List.fold_left 
     (fun acc (nmeta,_ as meta) ->
@@ -49,7 +66,7 @@ let html_of_status s =
     [] metasenv
   in
   String.concat "\n\n" txt
-;;
+;; *)
 
 let advance text (* (?bos=false) *) =
      let (st,new_statements),(* newtext TODO *) _,parsed_len =
@@ -59,7 +76,7 @@ let advance text (* (?bos=false) *) =
      in
      status := st;
      history := st :: !history;
-     let txt = html_of_status !status in
+     let txt = output_status !status in
      parsed_len, txt
 ;;
 
@@ -73,7 +90,7 @@ let retract () =
   NCicLibrary.time_travel !status;
   history := new_history;
   status := new_status;
-  html_of_status !status
+  output_status !status
 ;;
 
 let read_file fname =
@@ -162,16 +179,16 @@ let callback req outchan =
                 with e -> prerr_endline ("inner exception: " ^
                   Printexc.to_string e));
                 prerr_endline "end status";
-                let txt = html_of_status !status in
+                let txt = output_status !status in
                 (0,txt), Printexc.to_string e, `Code 500)
       in
-      let txt = Netencoding.Url.encode ~plus:false txt in
-      let body = (string_of_int parsed_len) ^ "#" ^ txt in
+      prerr_endline ("server response:\n" ^ txt);
+      let body = (string_of_int parsed_len) ^ "@" ^ txt in
       Http_daemon.respond ~code ~body outchan
   | "/retract" ->
       (try
-        let txt = retract () in
-        Http_daemon.respond ~code:(`Code 200) ~body:txt outchan
+        let body = retract () in
+        Http_daemon.respond ~code:(`Code 200) ~body outchan
        with e -> 
         (prerr_endline (Printexc.to_string e);
          Http_daemon.respond ~code:(`Code 500) outchan))
@@ -179,8 +196,6 @@ let callback req outchan =
 
 ;;
 
-
-
 let spec =
   { Http_daemon.default_spec with
       callback = callback;