This update uses XML for client-server communication. For unknown reasons, this

doesn't seem to work well with Firefox (but works ok on Chrome).

We reverted to a single process http daemon because of an annoying bug in
Ocaml Http, causing the daemon to terminate randomly.

diff --git a/matitaB/matita/matitadaemon.ml b/matitaB/matita/matitadaemon.ml
index 6601400ed5a11cf3c1d0996827449a6b97af8b72..18caa7426cc9d02b06855560b70712d452456f33 100644 (file)
--- a/matitaB/matita/matitadaemon.ml
+++ b/matitaB/matita/matitadaemon.ml
@@ -44,9 +44,14 @@ let history = ref [!status];;
 
 let include_paths = ["/home/barolo/matitaB/matita/lib"];;
 
-(* lista [meta n., goal; meta n., goal; ... ] *)
-(* "item1#item2#...#" *)
-
+(* <metasenv>
+ *   <meta number="...">
+ *     <metaname>...</metaname>
+ *     <goal>...</goal>
+ *   </meta>
+ *
+ *   ...
+ * </metasenv> *)
 let output_status s =
   let _,_,metasenv,subst,_ = s#obj in
   let render_switch = function 
@@ -68,7 +73,7 @@ let output_status s =
     let markup = 
       if is_loc then
         (match depth, pos with
-         | 0, 0 -> "<B>" ^ (render_switch sw) ^ "</B> "
+         | 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 ->
@@ -76,13 +81,23 @@ let output_status s =
          | _ -> 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)
+    let markup = 
+      Netencoding.Html.encode ~in_enc:`Enc_utf8 ~prefer_name:false () markup in
+    let markup = "<metaname>" ^ markup ^ "</metaname>" in
+    let sequent =
+      Netencoding.Html.encode ~in_enc:`Enc_utf8 ~prefer_name:false () (sequent sw)
+    in      
+    let txt0 = "<goal>" ^ sequent ^ "</goal>" in
+    "<meta number=\"" ^ (string_of_int metano) ^ "\">" ^ markup ^
+    txt0 ^ "</meta>" ^ acc
   in
-  Stack.fold 
-    ~env:(render_sequent true) ~cont:(render_sequent false) 
-    ~todo:(render_sequent false) "" s#stack
+  let res = "<metasenv>" ^
+    (Stack.fold 
+      ~env:(render_sequent true) ~cont:(render_sequent false) 
+      ~todo:(render_sequent false) "" s#stack) ^
+    "</metasenv>"
+  in 
+  prerr_endline ("sending metasenv:\n" ^ res); res
 ;;
 
 (* let html_of_status s =
@@ -226,7 +241,11 @@ let callback req outchan =
       prerr_endline "getting 'file' argument";
       let filename = List.assoc "file" req#params_GET in
       prerr_endline ("reading file " ^ filename);
-      let body = read_file filename in
+      let body = 
+       Netencoding.Html.encode ~in_enc:`Enc_utf8 ~prefer_name:false () 
+         (read_file filename) in
+      prerr_endline ("sending:\nBEGIN\n" ^ body ^ "\nEND");
+      let body = "<file>" ^ body ^ "</file>" in
       let _,baseuri,_,_ = 
         Librarian.baseuri_of_script ~include_paths:[] filename
       in
@@ -250,8 +269,11 @@ let callback req outchan =
                 (0,"",txt), Printexc.to_string e, `Code 500)
       in
       (* prerr_endline ("server response:\n" ^ txt); *)
-      let body = (string_of_int parsed_len) ^ "@" ^ txt in
-      Http_daemon.respond ~code ~body outchan
+      let body = 
+        "<response><parsed length=\"" ^ (string_of_int parsed_len) ^ "\" />" ^ txt 
+        ^ "</response>"
+      in (prerr_endline ("sending advance response:\n" ^ body);
+         Http_daemon.respond ~code ~body outchan)
   | "/bottom" ->
       let script = req#body in
       prerr_endline ("body length = " ^ (string_of_int (String.length script)));
@@ -270,8 +292,9 @@ let callback req outchan =
                 (0,txt), Printexc.to_string e, `Code 500)
       in
       (* prerr_endline ("server response:\n" ^ txt); *)
-      let body = (string_of_int parsed_len) ^ "@" ^ txt in
-      Http_daemon.respond ~code ~body outchan
+      let body = 
+        "<parsed length=\"" ^ (string_of_int parsed_len) ^ "\" />" ^ txt
+      in Http_daemon.respond ~code ~body outchan
   | "/retract" ->
       (try
         let body = retract () in
@@ -291,7 +314,7 @@ let spec =
   { Http_daemon.default_spec with
       callback = callback;
       port = 9999;
-      mode = `Thread;
+      mode = `Single (*`Thread *) ;
   }
 ;;
 

diff --git a/matitaB/matita/matitaweb.js b/matitaB/matita/matitaweb.js
index 588643861f3c7b178e2019c05fc378febb63060c..e87a19f520d3171f259a7428ad58d44dff52de01 100644 (file)
--- a/matitaB/matita/matitaweb.js
+++ b/matitaB/matita/matitaweb.js
@@ -149,31 +149,29 @@ function p33 (p)
   return (tripletmap (function (a,b,c) { return (c); }, p));
 }
 
-function populate_goalarray(txt)
+function populate_goalarray(menv)
 {
-  if (txt == "") {
+  debug("metasenv.length = " + menv.length);
+  if (menv.length == 0) {
       try {
           hideSequent();
       } catch (err) { };
   } else {
       showSequent();
-      debug("populate with '" + txt + "'");
       goalarray = new Array();
       metalist = listnil();
       var tmp_goallist = "";
-      listiter (function(item)
-        {
-         debug ("item is '" + item + "'");
-         tripletmap (function(a,ahtml,b) {   
-          debug ("found meta n. " + a);
-          debug ("found goal\nBEGIN" + unescape(b) + "\nEND");
-          goalarray[a] = unescape(b);
-          tmp_goallist = " <A href=\"javascript:switch_goal(" + a + ")\">" + unescape(ahtml) + "</A>" + tmp_goallist;
-          metalist = listcons(a,metalist);
-          debug ("goalarray[\"" + a + "\"] = " + goalarray[a]); 
-         },item);
-        }, txt);
-      // metalist = listmap (p13,txt);
+      for (i = 0; i < menv.length; i++) {
+        metano = menv[i].getAttribute("number");
+       metaname = menv[i].childNodes[0].childNodes[0].data;
+       goal = menv[i].childNodes[1].childNodes[0].data;
+        debug ("found meta n. " + metano);
+        debug ("found goal\nBEGIN" + goal + "\nEND");
+        goalarray[metano] = goal;
+        tmp_goallist = " <A href=\"javascript:switch_goal(" + metano + ")\">" + metaname + "</A>" + tmp_goallist;
+        metalist = listcons(metano,metalist);
+        debug ("goalarray[\"" + metano + "\"] = " + goalarray[metano]); 
+      }
       goals.innerHTML = tmp_goallist;
       debug("new metalist is '" + metalist + "'");
       if (is_nil(metalist)) {
@@ -263,12 +261,22 @@ function callServer(servicename,processResponse,reqbody)
                        stat = req.status;
                        stxt = req.statusText;
                        if(stat == 200)
-                       {       
-                               processResponse(req.responseText);
+                       {
+                         debug(req.responseText);
+                         if (window.DOMParser) {
+                            parser=new DOMParser();
+                            xmlDoc=parser.parseFromString(req.responseText,"text/xml");
+                          }
+                         else // Internet Explorer
+                          {
+                            xmlDoc=new ActiveXObject("Microsoft.XMLDOM");
+                            xmlDoc.async="false";
+                            xmlDoc.loadXML(req.responseText);
+                          }    
+                         processResponse(xmlDoc);
                        } else {
-                               processResponse();
+                         processResponse();
                        }
-                       // resume();
                } 
        };
        req.open("POST", servicename); // + escape(unlocked.innerHTML), true); 
@@ -282,11 +290,10 @@ function callServer(servicename,processResponse,reqbody)
 
 function advanceForm1()
 {
-       processor = function(responseText) {
-               if (is_defined(responseText)) {
+       processor = function(xml) {
+               if (is_defined(xml)) {
                        // debug("advance: received response\nBEGIN\n" + req.responseText + "\nEND");
-                       response = responseText.split("@");
-                       len = parseInt(response[0]);
+                       len = parseInt(xml.getElementsByTagName("parsed")[0].getAttribute("length"));
                        len0 = unlocked.innerHTML.length;
                        unescaped = unlocked.innerHTML.unescapeHTML();
                        parsedtxt = unescaped.substr(0,len); 
@@ -295,8 +302,8 @@ function advanceForm1()
                        unlocked.innerHTML = unparsedtxt;
                        len1 = unlocked.innerHTML.length;
                        len2 = len0 - len1;
-                       metasenv = response[1];
-                       populate_goalarray(response[1]);
+                       metasenv = xml.getElementsByTagName("meta");
+                       populate_goalarray(metasenv);
                        statements = listcons(len2,statements);
                        unlocked.scrollIntoView(true);
                } else {
@@ -311,22 +318,22 @@ function advanceForm1()
 
 function gotoBottom()
 {
-       processor = function(responseText) {
-               if (is_defined(responseText)) {
+       processor = function(xml) {
+               if (is_defined(xml)) {
                        // debug("goto bottom: received response\nBEGIN\n" + req.responseText + "\nEND");
-                       response = responseText.split("@");
-                       len = parseInt(response[0]);
-                        len0 = unlocked.innerHTML.length;
+                       len = parseInt(xml.getElementsByTagName("parsed")[0].getAttribute("length"));
+                       len0 = unlocked.innerHTML.length;
                        unescaped = unlocked.innerHTML.unescapeHTML();
                        parsedtxt = unescaped.substr(0,len); 
                        unparsedtxt = unescaped.substr(len);
                        locked.innerHTML = locked.innerHTML + parsedtxt;
                        unlocked.innerHTML = unparsedtxt;
                        len1 = unlocked.innerHTML.length;
-                       len = len0 - len1;
-                        populate_goalarray(response[1]);
-                       statements = listcons(len,statements);
-                        unlocked.scrollIntoView(true);
+                       len2 = len0 - len1;
+                       metasenv = xml.getElementsByTagName("meta");
+                       populate_goalarray(metasenv);
+                       statements = listcons(len2,statements);
+                       unlocked.scrollIntoView(true);
                } else {
                        debug("goto bottom failed");
                } 
@@ -343,11 +350,10 @@ function gotoPos(offset)
         if (!is_defined(offset)) {
                offset = getCursorPos();
         }
-       processor = function(responseText) {
-               if (is_defined(responseText)) {
-                       // debug("advance: received response\nBEGIN\n" + req.responseText + "\nEND");
-                       response = responseText.split("@");
-                       len = parseInt(response[0]);
+       processor = function(xml) {
+               if (is_defined(xml)) {
+                       // debug("goto pos: received response\nBEGIN\n" + req.responseText + "\nEND");
+                       len = parseInt(xml.getElementsByTagName("parsed")[0].getAttribute("length"));
                        len0 = unlocked.innerHTML.length;
                        unescaped = unlocked.innerHTML.unescapeHTML();
                        parsedtxt = unescaped.substr(0,len); 
@@ -356,11 +362,13 @@ function gotoPos(offset)
                        unlocked.innerHTML = unparsedtxt;
                        len1 = unlocked.innerHTML.length;
                        len2 = len0 - len1;
+                       metasenv = xml.getElementsByTagName("meta");
+                       // populate_goalarray(metasenv);
                        statements = listcons(len2,statements);
-                       metasenv = response[1];
+                       unlocked.scrollIntoView(true);
                        // la populate non andrebbe fatta a ogni passo
                        if (offset <= len) {
-                               populate_goalarray(response[1]);
+                               populate_goalarray(metasenv);
                                resume();
                        } else {
                                gotoPos(offset - len);
@@ -377,16 +385,17 @@ function gotoPos(offset)
 
 function retract()
 {
-       processor = function(responseText) {
-               if (typeof responseText != "undefined") {
-                debug("retract: received response\nBEGIN\n" + responseText + "\nEND");
+       processor = function(xml) {
+               if (typeof xml != "undefined") {
+                       // debug("advance: received response\nBEGIN\n" + req.responseText + "\nEND");
                        statementlen = parseInt(listhd(statements));
                         statements = listtl(statements);
                         lockedlen = locked.innerHTML.length - statementlen;
                        statement = locked.innerHTML.substr(lockedlen, statementlen);
                         locked.innerHTML = locked.innerHTML.substr(0,lockedlen);
                        unlocked.innerHTML = statement + unlocked.innerHTML;
-                        populate_goalarray(responseText);
+                       metasenv = xml.getElementsByTagName("meta");
+                        populate_goalarray(metasenv);
                         unlocked.scrollIntoView(true);
                } else {
                        debug("retract failed");
@@ -401,11 +410,11 @@ function retract()
 
 function openFile()
 { 
-       processor = function(responseText)
+       processor = function(xml)
        {
-               if (responseText) {     
+               if (is_defined(xml)) {  
                        locked.innerHTML = "";
-                       unlocked.innerHTML = responseText;
+                       unlocked.innerHTML = xml.documentElement.firstChild.data;
                } else {
                        debug("file open failed");
                }