From: matitaweb <claudio.sacerdoticoen@unibo.it>
Date: Tue, 18 Oct 2011 15:41:04 +0000 (+0000)
Subject: Localization of errors.
X-Git-Tag: make_still_working~2176
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=a7b54fb6f31e5ac626853890686ee54033dc7b24;p=helm.git

Localization of errors.
---

diff --git a/matitaB/matita/matitadaemon.ml b/matitaB/matita/matitadaemon.ml
index 606ccea4a..c92811c4e 100644
--- a/matitaB/matita/matitadaemon.ml
+++ b/matitaB/matita/matitadaemon.ml
@@ -1,6 +1,8 @@
 open Printf;;
 open Http_types;;
 
+exception Emphasized_error of string
+
 module Stack = Continuationals.Stack
 
 let rt_path () = Helm_registry.get "matita.rt_base_dir" 
@@ -29,9 +31,13 @@ let do_global_commit () =
        let ft = MatitaAuthentication.read_ft u in
 
        (* first we add new files/dirs to the repository *)
-       let to_be_added = List.map fst  
-         (List.filter (fun (_,flag) -> flag = MatitaFilesystem.MAdd) ft)
+       (* must take the reverse because svn requires the add to be performed in
+          the correct order
+          (otherwise run with --parents option) *)
+       let to_be_added = List.rev (List.map fst  
+         (List.filter (fun (_,flag) -> flag = MatitaFilesystem.MAdd) ft))
        in
+       prerr_endline ("@@@ ADDING files: " ^ String.concat ", " to_be_added);
        let out = 
          try
            let newout = MatitaFilesystem.add_files u to_be_added in
@@ -120,7 +126,10 @@ let do_global_commit () =
          (String.concat ", " not_added)
          (String.concat ", " not_committed) (String.concat ", " conflicts)))
 
-  "" (List.rev !to_be_committed)
+  (* XXX: at the moment, we don't keep track of the order in which users have 
+     scheduled their commits, but we should, otherwise we will get a 
+     "first come, random served" policy *)
+  "" (* (List.rev !to_be_committed) *) (MatitaAuthentication.get_users ())
 ;;
 
 (*** from matitaScript.ml ***)
@@ -337,12 +346,24 @@ let advance0 sid text =
   let status = MatitaAuthentication.get_status sid in
   let status = status#reset_disambiguate_db () in
   let (st,new_statements,new_unparsed),(* newtext TODO *) _,parsed_len =
-       try
-         eval_statement !include_paths (*buffer*) status (`Raw text)
-        with 
-        | HExtlib.Localized (_,e) -> raise e
-        (*| End_of_file -> raise Margin *)
-     in
+    try
+    eval_statement !include_paths (*buffer*) status (`Raw text)
+    with
+    | HExtlib.Localized (floc,e) as exn ->
+      let x, y = HExtlib.loc_of_floc floc in
+      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 = MatitaExcPp.to_string exn 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
   let stringbuf = Ulexing.from_utf8_string new_statements in
   let interpr = GrafiteDisambiguate.get_interpr st#disambiguate_db in
   let outstr = ref "" in
@@ -480,8 +501,6 @@ let save (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
         (* prerr_endline ("serializing proof objects..."); *)
         GrafiteTypes.Serializer.serialize 
           ~baseuri:(NUri.uri_of_string status#baseuri) status;
-        (* prerr_endline ("adding to the commit queue..."); *)
-        add_user_for_commit uid;
         (* prerr_endline ("done."); *)
        end;
      end;
@@ -613,7 +632,15 @@ let advance (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
       ~content_type:"text/xml; charset=\"utf-8\""
       ();
     cgi#out_channel#output_string body
-  with
+   with
+  | Emphasized_error text ->
+(* | MultiPassDisambiguator.DisambiguationError (offset,errorll) -> *)
+    let body = "<response><error>" ^ text ^ "</error> </response>" in 
+    cgi # set_header 
+      ~cache:`No_cache 
+      ~content_type:"text/xml; charset=\"utf-8\""
+      ();
+    cgi#out_channel#output_string body
   | Not_found _ -> 
     cgi # set_header
       ~status:`Internal_server_error
diff --git a/matitaB/matita/matitaweb.css b/matitaB/matita/matitaweb.css
index 03af7f6bb..9f0da2884 100644
--- a/matitaB/matita/matitaweb.css
+++ b/matitaB/matita/matitaweb.css
@@ -204,6 +204,12 @@ span.activegoal {
 	font-weight: bold;
 }
 
+span.error {
+        color:red;
+        text-decoration: none;
+        border-bottom: 2px dashed;
+}
+
 span.passivegoal {
 	color: blue;
 }
diff --git a/matitaB/matita/matitaweb.js b/matitaB/matita/matitaweb.js
index f05639282..fedaaf7fb 100644
--- a/matitaB/matita/matitaweb.js
+++ b/matitaB/matita/matitaweb.js
@@ -33,6 +33,16 @@ function unescape_html(s)
   return text_of_html(u)
 }
 
+function filterByClass (elements,class){
+  var itemsfound = new Array;
+  for(var i=0;i<elements.length;i++){
+    if(elements[i].className == class){
+      itemsfound.push(elements[i]);
+    }
+  }
+  return itemsfound;
+}
+
 function initialize()
 {
   if (readCookie("session") == null) {
@@ -161,12 +171,25 @@ function lookup_tex(texmacro)
   texmacro = texmacro.substring(1);
   return unescape(macro2utf8[texmacro]);
 }
+
+function strip_errors() 
+{
+    errors = filterByClass(unlocked.getElementsByTagName("span"),"error");
+    for (i = 0; i < errors.length; i++) {
+        children = errors[i].childNodes;
+        for (j = 0; j < children.length; j++) {
+            unlocked.insertBefore(children[j],errors[i]);
+	}
+        unlocked.removeChild(errors[i]);
+    }
+}
  
 function keypress(e)
 {
    if (!e) e= event;
    pressmesg('keypress',e);
    var s = string_of_key(e.charCode);
+   strip_errors();
    if (s == " ") {
 	j = getCursorPos();
 	i = unlocked.innerHTML.lastIndexOf('\\',j);
@@ -512,24 +535,31 @@ function advanceForm1()
 {
 	processor = function(xml) {
 		if (is_defined(xml)) {
+                        parsed = xml.getElementsByTagName("parsed")[0];
+                        if (is_defined(parsed)) {
 			// debug("advance: received response\nBEGIN\n" + req.responseText + "\nEND");
-			parsed = xml.getElementsByTagName("parsed")[0];
-			len = parseInt(parsed.getAttribute("length"));
-	                // len0 = unlocked.innerHTML.length;
-			unescaped = unlocked.innerHTML.html_to_matita();
-			parsedtxt = parsed.childNodes[0].nodeValue;
-			//parsedtxt = unescaped.substr(0,len); 
-			unparsedtxt = unescaped.substr(len);
-			lockedbackup += parsedtxt;
-			locked.innerHTML = lockedbackup;
-			unlocked.innerHTML = unparsedtxt.matita_to_html();
-			// len1 = unlocked.innerHTML.length;
-			// len2 = len0 - len1;
-			len2 = parsedtxt.length;
-			metasenv = xml.getElementsByTagName("meta");
-	                populate_goalarray(metasenv);
-			statements = listcons(len2,statements);
-			unlocked.scrollIntoView(true);
+			    len = parseInt(parsed.getAttribute("length"));
+	                    // len0 = unlocked.innerHTML.length;
+			    unescaped = unlocked.innerHTML.html_to_matita();
+			    parsedtxt = parsed.childNodes[0].nodeValue;
+			    //parsedtxt = unescaped.substr(0,len); 
+			    unparsedtxt = unescaped.substr(len);
+			    lockedbackup += parsedtxt;
+			    locked.innerHTML = lockedbackup;
+			    unlocked.innerHTML = unparsedtxt.matita_to_html();
+			    // len1 = unlocked.innerHTML.length;
+			    // len2 = len0 - len1;
+			    len2 = parsedtxt.length;
+			    metasenv = xml.getElementsByTagName("meta");
+	                    populate_goalarray(metasenv);
+			    statements = listcons(len2,statements);
+			    unlocked.scrollIntoView(true);
+			}
+		        else {
+                            error = xml.getElementsByTagName("error")[0]; 
+			    unlocked.innerHTML = error.childNodes[0].nodeValue;
+			    // debug(xml.childNodes[0].nodeValue);
+			}
 		} else {
 			debug("advance failed");
 		}