Improved rendering of sequents in matitaweb, including handling of multiple

goals.

diff --git a/matitaB/matita/matitadaemon.ml b/matitaB/matita/matitadaemon.ml
index b8b3a1eb2111882740d602f527704714ee34c2e7..934e2ab1e564fb8ddee5ec73a128c90a05f78662 100644 (file)
--- a/matitaB/matita/matitadaemon.ml
+++ b/matitaB/matita/matitadaemon.ml
@@ -1,6 +1,8 @@
 open Printf;;
 open Http_types;;
 
+module Stack = Continuationals.Stack
+
 (*** from matitaScript.ml ***)
 (* let only_dust_RE = Pcre.regexp "^(\\s|\n|%%[^\n]*\n)*$" *)
 
@@ -42,16 +44,40 @@ let include_paths = ["/home/barolo/matitaB/matita/lib"];;
 
 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 render_switch = function 
+  | Stack.Open i -> "?" ^ (string_of_int i) 
+  | Stack.Closed i -> "<S>?" ^ (string_of_int i) ^ "</S>"
+  in
+  let int_of_switch = function
+  | Stack.Open i | Stack.Closed i -> i
+  in
+  let sequent = function
+  | Stack.Open i ->
+      let meta = List.assoc i metasenv in
+      snd (ApplyTransformation.ntxt_of_cic_sequent 
+        ~metasenv ~subst ~map_unicode_to_tex:false 80 s (i,meta))
+  | Stack.Closed _ -> "This goal has already been closed."
+  in
+  let render_sequent is_loc acc depth tag (pos,sw) =
+    let metano = int_of_switch sw in
+    let markup = 
+      if is_loc then
+        (match depth, pos with
+         | 0, 0 -> "<B>" ^ (render_switch sw) ^ "</B> "
+         | 0, _ -> 
+            Printf.sprintf "<B>|<SUB>%d</SUB>: %s</B>" pos (render_switch sw)
+         | 1, pos when Stack.head_tag s#stack = `BranchTag ->
+             Printf.sprintf "|<SUB>%d</SUB> : %s" pos (render_switch sw)
+         | _ -> render_switch sw)
+      else render_switch sw
+    in
+    let markup = Netencoding.Url.encode ~plus:false markup in
+    let txt0 = Netencoding.Url.encode ~plus:false (sequent sw) in
+    (string_of_int metano ^ "|" ^ markup ^ "|" ^ txt0 ^ "#" ^ acc)
+  in
+  Stack.fold 
+    ~env:(render_sequent true) ~cont:(render_sequent false) 
+    ~todo:(render_sequent false) "" s#stack
 ;;
 
 (* let html_of_status s =