From: matitaweb <claudio.sacerdoticoen@unibo.it>
Date: Fri, 30 Sep 2011 11:11:22 +0000 (+0000)
Subject: Matitaweb:
X-Git-Tag: make_still_working~2261
X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=54f0752c831479f87d61afcdfdafd2a35edb4053

Matitaweb:
1) Added experimental update functionality
2) Flagged library files -synchronized, modified, conflicted, unmanaged-
   (partial implementation)
3) Various cosmetic changes
---

diff --git a/matitaB/matita/index.html b/matitaB/matita/index.html
index c7be10ff1..a1099ad7f 100644
--- a/matitaB/matita/index.html
+++ b/matitaB/matita/index.html
@@ -33,15 +33,27 @@
 						  id="bottom" alt="Bottom" title="Execute the whole script."></A>
 </div>
 <div class="toolbar">
+  <table>
+  <tr>
+    <td>
 	   <INPUT type="BUTTON" value="New" id="newbutton" ONCLICK="newDialog()">
 	   <INPUT type="BUTTON" value="Open" id="showdialog" ONCLICK="openDialog()">
 	   <INPUT type="BUTTON" value="Save" id="savebutton" ONCLICK="saveFile()">
 	   <INPUT type="BUTTON" value="Save as" id="saveasbutton" ONCLICK="saveDialog()">
+    </td>
+  </tr>
+  <tr>
+    <td>
  	   <INPUT type="BUTTON" value="Upload" id="uploadbutton" ONCLICK="uploadDialog()">
            <INPUT type="BUTTON" value="Commit" id="commitbutton" ONCLICK="commitAll()">
+           <INPUT type="BUTTON" value="Update" id="updatebutton" ONCLICK="updateAll()">
+           <INPUT type="BUTTON" value="Log" id="logbutton" ONCLICK="showLog()">
 <!--	   <INPUT type="BUTTON" value="show sequent" id="showseq" ONCLICK="showSequent()">
 	   <INPUT type="BUTTON" value="hide sequent" id="hideseq" ONCLICK="hideSequent()">
 	   <INPUT type="BUTTON" value="selection test" id="hideseq" ONCLICK="test()"> -->
+    </td>
+  </tr>
+  </table> 
 
 </div>
 <div class="caption"><p><img align="bottom" class="topimg" src="icons/matita-text.png"></p></div>
@@ -60,21 +72,22 @@
 </div>
 <div class="goalarea" id="goalcell">
   <div id="goals"></div>
-  <div contentEditable="true" style="border-style:solid; height:100%; width:100%; overflow:auto;">
+  <div contentEditable="true" style="border-style:solid; height:95%; width:100%; overflow:auto;">
   <pre id="goalview"></pre>
   </div>
 </div>
 </div>
 
-<div class="bottomarea">
+<!-- <div class="bottomarea">
 	<textarea id="logarea" style="width:100%; height:100%"></textarea>
-</div>
+</div> -->
 
 </div>
 
 <div class="dialog" id="dialogBox" style="display: none;">
   <div class="diaTitle" id="dialogTitle"></div>
   <div class="diaClose" id="dialogClose"><H2><A id="butClose" href="javascript:abortDialog()">X</A></H2></div>
+  <INPUT type="button" id="dialogNewdir" value="Create dir..." ONCLICK="createDir()" style="width:150px"><br/>
   <div class="scroll" id="dialogContent"></div>
   <INPUT class="diaFile" type="text" id="dialogFilename">
   <INPUT type="button" id="dialogSelect" value="OK" ONCLICK="dialogOK()" style="width:70px">
diff --git a/matitaB/matita/matitaAuthentication.ml b/matitaB/matita/matitaAuthentication.ml
index 77aeed15f..566965851 100644
--- a/matitaB/matita/matitaAuthentication.ml
+++ b/matitaB/matita/matitaAuthentication.ml
@@ -25,6 +25,8 @@
 
 type session_id = Uuidm.t
 
+type matita_file = MatitaFilesystem.matita_flag * string
+
 (* user table: user id, (password, optional session id) *)
 type user = string * (string * session_id option)
 
@@ -115,13 +117,47 @@ let deserialize () =
   session_tbl := [];
 ;;
 
+let write_ft uid ft =
+  let ft_ch = open_out (config_path () ^ "/ft_" ^ uid ^ ".dump") in
+  Marshal.to_channel ft_ch ft [];
+  close_out ft_ch;
+;;
+
+let read_ft uid =
+  try
+    let ft_ch = open_in (config_path () ^ "/ft_" ^ uid ^ ".dump") in
+    let ft = Marshal.from_channel ft_ch in
+    close_in ft_ch;
+    ft
+  with
+    | Sys_error _ -> 
+      (* this is an error, we should rebuild the table by a diff of
+         the directory listing and svn stat *) 
+      [] 
+;;
+
+let set_file_flag uid filename flag = 
+  let ft = read_ft uid in
+  let oldflag = 
+    try List.assoc filename ft
+    with Not_found -> MatitaFilesystem.MSynchronized
+  in
+  if oldflag <> MatitaFilesystem.MConflict 
+    then
+      let ft = (filename,flag)::
+        List.filter (fun (fn,_) -> fn <> filename) ft in
+      write_ft uid ft
+    else ()
+;;
+
 let add_user uid pw =
   try
     let _ = lookup_user uid in
     raise (UsernameCollision uid)
   with Not_found -> 
-    MatitaFilesystem.checkout uid;
+    let ft = MatitaFilesystem.checkout uid in
     user_tbl := (uid,(pw,None))::!user_tbl;
+    write_ft uid ft;
     serialize ()
 ;;
 
diff --git a/matitaB/matita/matitaAuthentication.mli b/matitaB/matita/matitaAuthentication.mli
index 41f0304af..8a832eb81 100644
--- a/matitaB/matita/matitaAuthentication.mli
+++ b/matitaB/matita/matitaAuthentication.mli
@@ -51,6 +51,12 @@ val serialize : unit -> unit
 
 val deserialize : unit -> unit
 
+val read_ft : string -> (string * MatitaFilesystem.matita_flag) list
+
+val write_ft : string -> (string * MatitaFilesystem.matita_flag) list -> unit
+
+val set_file_flag : string -> string -> MatitaFilesystem.matita_flag -> unit
+
 val add_user : string -> string -> unit
 
 val reset : unit -> unit
diff --git a/matitaB/matita/matitaFilesystem.ml b/matitaB/matita/matitaFilesystem.ml
index 2686fff42..b846c153c 100644
--- a/matitaB/matita/matitaFilesystem.ml
+++ b/matitaB/matita/matitaFilesystem.ml
@@ -46,25 +46,115 @@ let exec_process cmd =
      assert false
     with End_of_file -> 
      match (Unix.close_process_full chs) with
-     | Unix.WEXITED errno -> 
-        let output = "std out =\n" ^ String.concat "\n" (List.rev !outlines) in
-        let errors = "std err =\n" ^ String.concat "\n" (List.rev !errlines) in
-        errno, output ^ "\n\n" ^ errors
+     | Unix.WEXITED errno -> errno, !outlines, !errlines 
      | _ -> assert false))
 
-(* this should be executed only for a freshly created user
- * so no CS is needed *)
+let string_of_output outlines errlines =
+  let output = "std out =\n" ^ String.concat "\n" (List.rev outlines) in
+  let errors = "std err =\n" ^ String.concat "\n" (List.rev errlines) in
+  output ^ "\n\n" ^ errors
+
+type svn_flag = 
+| Add
+| Conflict
+| Modified
+| NotAdded
+| Delete
+| Update
+| Merge
+
+type matita_flag =
+| MUnversioned
+| MSynchronized
+| MAdd
+| MModified
+| MConflict
+
+let string_of_matita_flag = function
+| MUnversioned -> "unversioned"
+| MSynchronized -> "synchronized"
+| MAdd -> "new"
+| MModified -> "modified"
+| MConflict -> "conflict!"
+
+exception SvnAnomaly of string
+
+let stat_classify line =
+  let rec aux n acc =
+    match (line.[n], n) with
+    | _, n when n = 7 -> String.sub line 8 ((String.length line) - 8), acc
+    | ' ', _ -> aux (n+1) acc
+    | 'A',0 -> aux (n+1) (Add::acc)
+    | 'C',_ when n = 0 || n = 1 -> aux (n+1) (Conflict::acc)
+(*  | 'D',0 -> aux (n+1) (Delete::acc) *)
+(*  | 'I',0 -> aux (n+1) (Ignore::acc) *)
+    | 'M',_ when n = 0 || n = 1 -> aux (n+1) (Modified::acc)
+(*  | 'R',0 -> aux (n+1) (Replaced::acc) *)
+(*  | 'X',0 -> aux (n+1) (UnversionedDir::acc) *)
+    | '?',0 -> aux (n+1) (NotAdded::acc)
+(*  | '!',0 -> aux (n+1) (Missing::acc) *)
+(*  | '~',0 -> aux (n+1) (Obstructed::acc) *)
+(*  | 'L',2 -> aux (n+1) (Lock::acc) *)
+(*  | '+',3 -> aux (n+1) (History::acc) *)
+(*  | 'S',4 -> aux (n+1) (SwitchedUrl::acc) *)
+(*  | 'X',4 -> aux (n+1) (External::acc) *)
+(*  | 'K',5 -> aux (n+1) (LockToken::acc) *)
+(*  | 'C',6 -> aux (n+1) (TreeConflict::acc) *)
+    | _ -> raise (SvnAnomaly line)
+  in aux 0 []
+
+let stat_user user =
+  let rt_dir = Helm_registry.get "matita.rt_base_dir" in
+  let repo = Helm_registry.get "matita.weblib" in
+
+  let errno, outlines, errlines = exec_process 
+    ("svn stat " ^ rt_dir ^ "/users/" ^ user ^ "/")
+  in
+  let files, anomalies = 
+    List.fold_left (fun (facc,eacc) line ->
+      try
+        (stat_classify line::facc), eacc
+      with
+      | SvnAnomaly l -> facc, l::eacc) ([],[]) outlines
+  in
+  if errno = 0 then files, anomalies
+  else raise (SvnError ("Anomalies: " ^ (String.concat "\n" anomalies) ^ "\n\n" ^ (string_of_output outlines errlines)))
+;;
+
+(* update and checkout *)
+let up_classify line =
+  let rec aux n acc =
+    match (line.[n], n) with
+    | _, n when n = 4 -> String.sub line 5 ((String.length line) - 5), acc
+    | ' ', _ -> aux (n+1) acc
+    | 'A',_ when n = 0 || n = 1 -> aux (n+1) (Add::acc)
+    | 'C',_ when n = 0 || n = 1 -> aux (n+1) (Conflict::acc)
+    | 'D',_ when n = 0 || n = 1 -> aux (n+1) (Delete::acc)
+    | 'U',_ when n = 0 || n = 1 -> aux (n+1) (Update::acc)
+    | 'G',_ when n = 0 || n = 1 -> aux (n+1) (Merge::acc)
+(*  | 'E',_ when n = 0 || n = 1 -> aux (n+1) (Exist::acc) *)
+    | _ -> raise (SvnAnomaly line)
+  in aux 0 []
+
+(* this should be executed only for a freshly created user so no CS is needed *)
 let checkout user =
   let rt_dir = Helm_registry.get "matita.rt_base_dir" in
   let repo = Helm_registry.get "matita.weblib" in
 
-  let errno, outstr = exec_process 
+  let errno, outlines, errlines = exec_process 
     ("svn co " ^ repo ^ " " ^ rt_dir ^ "/users/" ^ user ^ "/")
   in
-  if errno = 0 then ()
-  else raise (SvnError outstr)
+  let files, anomalies = 
+    List.fold_left (fun (facc,eacc) line ->
+      try
+        (up_classify line::facc), eacc
+      with
+      | SvnAnomaly l -> facc, l::eacc) ([],[]) outlines
+  in
+  if errno = 0 then List.map (fun (f,_) -> f,MSynchronized) files 
+  else raise (SvnError (string_of_output outlines errlines))
 
-let html_of_library uid =
+let html_of_library uid ft =
   let i = ref 0 in
   let newid () = incr i; ("node" ^ string_of_int !i) in
 
@@ -74,9 +164,19 @@ let html_of_library uid =
     let id = newid () in
     let name = Filename.basename lpath in
     let name = if name <> "." then name else "cic:/matita" in
+    let lpath =
+      try 
+        if String.sub lpath 0 2 <> "./" then lpath 
+        else String.sub lpath 2 (String.length lpath - 2)
+      with Invalid_argument _ -> lpath
+    in
+    let flag = 
+      try List.assoc lpath ft 
+      with Not_found -> MSynchronized in
+    let szflag = string_of_matita_flag flag in
     "<span class=\"trigger\" onClick=\"showBranch('" ^ id ^ "','" ^ lpath ^ "/')\">\n" ^
     "<img src=\"treeview/closed.gif\" id=\"I" ^ id ^ "\"/>\n" ^
-    name ^ "<br/></span>\n" ^
+    name ^ " " ^ szflag ^ "<br/></span>\n" ^
     "<span class=\"branch\" id=\"" ^ id ^ "\">\n" ^
     children ^ "\n</span>"
   in
@@ -129,6 +229,24 @@ let add_user uid =
   Mutex.unlock mutex;
 ;;
 
+let update_user user =
+  let rt_dir = Helm_registry.get "matita.rt_base_dir" in
+  let repo = Helm_registry.get "matita.weblib" in
+
+  let errno, outlines, errlines = exec_process 
+    ("svn up " ^ rt_dir ^ "/users/" ^ user ^ "/")
+  in
+  let files, anomalies = 
+    List.fold_left (fun (facc,eacc) line ->
+      try
+        (up_classify line::facc), eacc
+      with
+      | SvnAnomaly l -> facc, l::eacc) ([],[]) outlines
+  in
+  if errno = 0 then files, anomalies
+  else raise (SvnError (string_of_output outlines errlines))
+;;
+
 (* this function and the next one should only be called by the server itself (or
  * the admin) at a scheduled time, so no concurrent instances and no CS needed
  * also, svn should already be safe as far as concurrency is concerned *)
@@ -136,11 +254,12 @@ let commit user =
   let rt_dir = Helm_registry.get "matita.rt_base_dir" in
   let repo = Helm_registry.get "matita.weblib" in
 
-  let errno, outstr = exec_process 
+  let errno, outlines, errlines = exec_process 
     ("svn ci --message \"commit by user " ^ user ^ "\" " ^ rt_dir ^ "/users/" ^ user ^ "/")
   in
   if errno = 0 then ()
-  else raise (SvnError outstr)
+  else raise (SvnError (string_of_output outlines errlines))
+;;
 
 let do_global_commit () =
   prerr_endline ("to be committed: " ^ String.concat " " !to_be_committed);
diff --git a/matitaB/matita/matitaFilesystem.mli b/matitaB/matita/matitaFilesystem.mli
index ed840d230..f1906b1e8 100644
--- a/matitaB/matita/matitaFilesystem.mli
+++ b/matitaB/matita/matitaFilesystem.mli
@@ -1,8 +1,26 @@
 exception SvnError of string;;
 
-val checkout : string -> unit
+type svn_flag =
+| Add
+| Conflict
+| Modified
+| NotAdded
+| Delete
+| Update
+| Merge
 
-val html_of_library : string -> string
+type matita_flag =
+| MUnversioned
+| MSynchronized
+| MAdd
+| MModified
+| MConflict
+
+val string_of_matita_flag : matita_flag -> string
+
+val checkout : string -> (string * matita_flag) list
+
+val html_of_library : string -> (string * matita_flag) list ->  string
 
 val reset_lib : unit -> unit
 
@@ -11,3 +29,7 @@ val reset_lib : unit -> unit
 val add_user : string -> unit
 
 val do_global_commit : unit -> string list
+
+val update_user : string -> (string * svn_flag list) list * string list
+
+val stat_user : string -> (string * svn_flag list) list * string list
diff --git a/matitaB/matita/matitadaemon.ml b/matitaB/matita/matitadaemon.ml
index 9d0f94226..fb75e6579 100644
--- a/matitaB/matita/matitadaemon.ml
+++ b/matitaB/matita/matitadaemon.ml
@@ -89,11 +89,11 @@ let output_status s =
     let markup = 
       if is_loc then
         (match depth, pos with
-         | 0, 0 -> "<B>" ^ (render_switch sw) ^ "</B>"
+         | 0, 0 -> "<span class=\"activegoal\">" ^ (render_switch sw) ^ "</span>"
          | 0, _ -> 
-            Printf.sprintf "<B>|<SUB>%d</SUB>: %s</B>" pos (render_switch sw)
+            Printf.sprintf "<span class=\"activegoal\">|<SUB>%d</SUB>: %s</span>" pos (render_switch sw)
          | 1, pos when Stack.head_tag s#stack = `BranchTag ->
-             Printf.sprintf "|<SUB>%d</SUB> : %s" pos (render_switch sw)
+             Printf.sprintf "<span class=\"passivegoal\">|<SUB>%d</SUB> : %s</span>" pos (render_switch sw)
          | _ -> render_switch sw)
       else render_switch sw
     in
@@ -247,6 +247,7 @@ let advance0 sid text =
   let interpr = GrafiteDisambiguate.get_interpr st#disambiguate_db in
   let outstr = ref "" in
   ignore (SmallLexer.mk_small_printer interpr outstr stringbuf);
+  prerr_endline ("baseuri after advance = " ^ st#baseuri);
   (* prerr_endline ("parser output: " ^ !outstr); *)
   MatitaAuthentication.set_status sid st;
   parsed_len, 
@@ -296,7 +297,8 @@ let login (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
 
   if pw = userpw then
    begin
-    let _ = MatitaFilesystem.html_of_library uid in
+   let ft = MatitaAuthentication.read_ft uid in
+   let _ = MatitaFilesystem.html_of_library uid ft in
     let sid = MatitaAuthentication.create_session uid in
     (* let cookie = Netcgi.Cookie.make "session" (Uuidm.to_string sid) in
        cgi#set_header ~set_cookies:[cookie] (); *)
@@ -357,24 +359,32 @@ let save (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
     assert (cgi#arguments <> []);
     let locked = cgi#argument_value "locked" in
     let unlocked = cgi#argument_value "unlocked" in
-    let filename = libdir uid ^ "/" ^ (cgi # argument_value "file") in
+    let dir = cgi#argument_value "dir" in
+    let rel_filename = cgi # argument_value "file" in
+    let filename = libdir uid ^ "/" ^ rel_filename in
     let force = bool_of_string (cgi#argument_value "force") in
 
     if ((not force) && (Sys.file_exists filename)) then 
       raise File_already_exists;
 
-    let oc = open_out filename in
-    output_string oc (locked ^ unlocked);
-    close_out oc;
-    if MatitaEngine.eos status unlocked then
+    if dir = "true" then
+      Unix.mkdir filename 0o744
+    else 
      begin
-      (* prerr_endline ("serializing proof objects..."); *)
-      GrafiteTypes.Serializer.serialize 
-        ~baseuri:(NUri.uri_of_string status#baseuri) status;
-      (* prerr_endline ("adding to the commit queue..."); *)
-      MatitaFilesystem.add_user uid;
-      (* prerr_endline ("done."); *)
+      let oc = open_out filename in
+      output_string oc (locked ^ unlocked);
+      close_out oc;
+      if MatitaEngine.eos status unlocked then
+       begin
+        (* prerr_endline ("serializing proof objects..."); *)
+        GrafiteTypes.Serializer.serialize 
+          ~baseuri:(NUri.uri_of_string status#baseuri) status;
+        (* prerr_endline ("adding to the commit queue..."); *)
+        MatitaFilesystem.add_user uid;
+        (* prerr_endline ("done."); *)
+       end;
      end;
+    MatitaAuthentication.set_file_flag uid rel_filename MatitaFilesystem.MModified;
     cgi # set_header 
       ~cache:`No_cache 
       ~content_type:"text/xml; charset=\"utf-8\""
@@ -388,7 +398,10 @@ let save (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
       ~status:`Internal_server_error
       ~cache:`No_cache 
       ~content_type:"text/xml; charset=\"utf-8\""
-      ());
+      ()
+  | e ->
+      let estr = Printexc.to_string e in
+      cgi#out_channel#output_string ("<response>" ^ estr ^ "</response>"));
   cgi#out_channel#commit_work()
 ;;
 
@@ -413,6 +426,35 @@ let initiate_commit (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
   cgi#out_channel#commit_work()
 ;;
 
+let svn_update (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
+  let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in
+  let env = cgi#environment in
+  let sid = Uuidm.of_string (Netcgi.Cookie.value (env#cookie "session")) in
+  let sid = HExtlib.unopt sid in
+  let uid = MatitaAuthentication.user_of_session sid in
+  (try
+    let files,anomalies = MatitaFilesystem.update_user uid in
+    (* let changed = HExtlib.filter_map 
+        (fun (fl,n) -> if (List.mem MatitaFilesystem.Modified fl) then Some n else None) files
+      in
+      let changed = String.concat "\n" changed in
+      let anomalies = String.concat "\n" anomalies in
+      prerr_endline ("Changed:\n" ^ changed ^ "\n\nAnomalies:\n" ^ anomalies); *)
+    cgi # set_header 
+      ~cache:`No_cache 
+      ~content_type:"text/xml; charset=\"utf-8\""
+      ();
+    cgi#out_channel#output_string "<response>ok</response>"
+  with
+  | Not_found _ -> 
+    cgi # set_header
+      ~status:`Internal_server_error
+      ~cache:`No_cache 
+      ~content_type:"text/xml; charset=\"utf-8\""
+      ());
+  cgi#out_channel#commit_work()
+;;
+
 (* returns the length of the executed text and an html representation of the
  * current metasenv*)
 let advance (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
@@ -526,7 +568,9 @@ let gotoTop (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
     let uid = MatitaAuthentication.user_of_session sid in
     let baseuri = status#baseuri in
     let new_status = new MatitaEngine.status (Some uid) baseuri in
+    prerr_endline "gototop prima della time travel";
     NCicLibrary.time_travel new_status;
+    prerr_endline "gototop dopo della time travel";
     let new_history = [new_status] in 
     MatitaAuthentication.set_history sid new_history;
     MatitaAuthentication.set_status sid new_status;
@@ -540,8 +584,8 @@ let gotoTop (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
      (cgi#set_header ~status:`Internal_server_error 
       ~cache:`No_cache 
       ~content_type:"text/xml; charset=\"utf-8\"" ();
-      cgi#out_channel#output_string "<response>ok</response>");
-  cgi#out_channel#commit_work()) 
+      cgi#out_channel#output_string "<response>ok</response>"));
+  cgi#out_channel#commit_work() 
 ;;
 
 let retract (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
@@ -563,9 +607,12 @@ let retract (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
           history, status
       | [_] -> (prerr_endline "singleton";failwith "retract")
       | _ -> (prerr_endline "nil"; assert false) in
+    prerr_endline ("prima della time travel");
     NCicLibrary.time_travel new_status;
+    prerr_endline ("dopo della time travel");
     MatitaAuthentication.set_history sid new_history;
     MatitaAuthentication.set_status sid new_status;
+    prerr_endline ("baseuri after retract = " ^ new_status#baseuri);
     let body = output_status new_status in
     cgi # set_header 
       ~cache:`No_cache 
@@ -593,7 +640,8 @@ let viewLib (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
     *)
     let uid = MatitaAuthentication.user_of_session sid in
     
-    let html = MatitaFilesystem.html_of_library uid in
+    let ft = MatitaAuthentication.read_ft uid in
+    let html = MatitaFilesystem.html_of_library uid ft in
     cgi # set_header 
       ~cache:`No_cache 
       ~content_type:"text/html; charset=\"utf-8\""
@@ -606,6 +654,14 @@ let viewLib (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
        "<script src=\"treeview/xmlTree.js\" type=\"text/javascript\"></script>\n" ^
        "<body>\n" ^ *)
        html (* ^ "\n</body></html>" *) );
+    
+    let files,anomalies = MatitaFilesystem.stat_user uid in
+    let changed = HExtlib.filter_map 
+      (fun (n,fl) -> if (List.mem MatitaFilesystem.Modified fl) then Some n else None) files
+    in
+    let changed = String.concat "\n" changed in
+    let anomalies = String.concat "\n" anomalies in
+    prerr_endline ("Changed:\n" ^ changed ^ "\n\nAnomalies:\n" ^ anomalies);
   cgi#out_channel#commit_work()
   
 ;;
@@ -743,6 +799,14 @@ let start() =
       dyn_translator = (fun _ -> ""); (* not needed *)
       dyn_accept_all_conditionals = false;
     } in 
+  let do_update =
+    { Nethttpd_services.dyn_handler = (fun _ -> svn_update);
+      dyn_activation = Nethttpd_services.std_activation `Std_activation_buffered;
+      dyn_uri = None;                 (* not needed *)
+      dyn_translator = (fun _ -> ""); (* not needed *)
+      dyn_accept_all_conditionals = false;
+    } in 
+  
   
   let nethttpd_factory = 
     Nethttpd_plex.nethttpd_factory
@@ -757,7 +821,8 @@ let start() =
                 ; "reset", do_resetlib
                 ; "viewlib", do_viewlib
                 ; "save", do_save
-                ; "commit", do_commit]
+                ; "commit", do_commit
+		; "update", do_update]
       () in
   MatitaInit.initialize_all ();
   MatitaAuthentication.deserialize ();
diff --git a/matitaB/matita/matitaweb.css b/matitaB/matita/matitaweb.css
index aed752a8e..e481b4162 100644
--- a/matitaB/matita/matitaweb.css
+++ b/matitaB/matita/matitaweb.css
@@ -64,7 +64,7 @@ div.scroll {
 	margin-left: auto;
 	margin-right: auto;
 	border: 1px solid #ccc;
-	height:440px; 
+	height:415px; 
 	width:442px; 
 	overflow:auto;
 	background-color: white;
@@ -103,7 +103,7 @@ div.workarea {
 	display: block;
 	margin-left: auto;
 	margin-right: auto;
-	height:70%; 
+	height:88%; 
 	width:100%; 
 }
 
@@ -137,6 +137,7 @@ div.caption {
 
 img.topimg {
 	bottom:0px;
+        border:none;
 }
 
 div.scriptarea {
@@ -144,8 +145,9 @@ div.scriptarea {
 	margin-left: auto;
 	margin-right: auto;
 	height:100%; 
-	width:100%;
+	width:67%%;
         min-width:67%;
+        max-width:67%;
         float:left;
 }
 
@@ -155,10 +157,19 @@ div.goalarea {
 	margin-right: auto;
 	height:100%; 
 	width:33%;
-        min-width:33%; 
+        min-width:33%;
+        max-width:33%; 
         float:right;
 }
 
+span.activegoal {
+	color: red;
+	font-weight: bold;
+}
+
+span.passivegoal {
+	color: blue;
+}
 
 h2 {
 	border: 0px;
diff --git a/matitaB/matita/matitaweb.js b/matitaB/matita/matitaweb.js
index d9bd38aa8..3b37fc76b 100644
--- a/matitaB/matita/matitaweb.js
+++ b/matitaB/matita/matitaweb.js
@@ -17,6 +17,22 @@ var dialogContent;
 var metasenv = "";
 var lockedbackup = "";
 
+function text_of_html(h)
+{
+  if(document.all) {
+     return h.innerText;
+  } else {
+     return h.textContent;
+  }
+}
+
+function unescape_html(s)
+{
+  u = document.getElementById("unescape");
+  u.innerHTML = s;
+  return text_of_html(u)
+}
+
 function initialize()
 {
   if (readCookie("session") == null) {
@@ -109,28 +125,25 @@ function suppressdefault(e,flag)
    return !flag;
 }
 
-function restoreSelection(adjust) {
+function restoreSelection(r) {
     unlocked.focus();
-    if (savedRange != null) {
+    if (r != null) {
         if (window.getSelection)//non IE and there is already a selection
         {
             var s = window.getSelection();
             if (s.rangeCount > 0) 
                 s.removeAllRanges();
-	    range = document.createRange();
-	    range.setStart(savedsc,savedso + adjust);
-	    range.collapse(true);
-            s.addRange(range);
+            s.addRange(r);
         }
         else 
             if (document.createRange)//non IE and no selection
             {
-                window.getSelection().addRange(savedRange);
+                window.getSelection().addRange(r);
             }
             else 
                 if (document.selection)//IE
                 {
-                    savedRange.select();
+                    r.select();
                 }
     }
 }
@@ -151,16 +164,24 @@ function keypress(e)
 	i = unlocked.innerHTML.lastIndexOf('\\',j);
        	if (i >= 0) {
 	  match = unlocked.innerHTML.substring(i,j);
-	  pre = unlocked.innerHTML.substring(0,i);
-	  post = unlocked.innerHTML.substring(j);
-	  
-	  sym = lookup_tex(match);
-	  if (typeof sym != "undefined") {
-	     len1 = unlocked.innerText.length;
-             unlocked.innerHTML = pre + sym + post;
-	     len2 = unlocked.innerText.length;
-             restoreSelection(len2 - len1); 
- 	     return suppressdefault(e,true);
+	  sym = unescape_html(lookup_tex(match));
+	  if (sym != "undefined") {
+             if (window.getSelection) { // non IE
+                savedRange.setStart(savedsc,savedso - (j-i));
+                savedRange.deleteContents();
+                savedRange.insertNode(document.createTextNode(sym));
+                savedsc.parentNode.normalize();
+                if (savedRange.collapsed) { // Mozilla
+                  savedRange.setEnd(savedsc,savedRange.endOffset + sym.length);
+                }
+                savedRange.collapse(false);
+             } else {
+                savedRange.moveStart(i-j);
+                savedRange.text(sym);
+                savedRange.collapse(false);
+             }
+             restoreSelection(savedRange); 
+       	     return suppressdefault(e,true);
 	  }
 	  else {
              // restoreSelection(0); 
@@ -173,13 +194,24 @@ function keypress(e)
    }
 }
  
+var logtxt = "";
+
 function debug(txt)
 {
         // internet explorer (v.9) doesn't work with innerHTML
 	// but google chrome's innerText is, in a sense, "write only"
 	// what should we do?
         // logarea.innerText = txt + "\n" + logarea.innerText;
-        logarea.innerHTML = txt; // + "\n" + logarea.innerText;
+        logtxt = logtxt + "\n" + txt;
+}
+
+function showLog() {
+  logWin = window.open( "", "Matita Log",
+     "width=600,height=450,status,scrollbars,resizable,screenX=20,screenY=40,left=20,top=40");
+  logWin.document.write('<html><head><title>Matita Log' + '</title></head>');	
+  logWin.document.write('<body><textarea style="width:100%;height:100%;">' +
+    logtxt + '</textarea></body></html>');
+  logWin.document.close(); 
 }
 
 function listhd(l)
@@ -543,10 +575,18 @@ function gotoTop()
                      debug("goto top failed");
                   }
                   else
-                     unlocked.innerHTML = locked.innerHTML + unlocked.innerHTML
-                     locked.innerHTML = ""
-                     hideSequent();
-                     unlocked.scrollIntoView(true);
+                        statements = listnil();
+			/*
+                        lockedlen = locked.innerHTML.length - statementlen;
+			statement = locked.innerHTML.substr(lockedlen, statementlen);
+                        locked.innerHTML = locked.innerHTML.substr(0,lockedlen);
+			unlocked.innerHTML = statement + unlocked.innerHTML;
+			*/
+			unlocked.innerHTML = lockedbackup + unlocked.innerHTML;
+			lockedbackup = "";
+                        locked.innerHTML = lockedbackup;
+                        hideSequent();
+                        unlocked.scrollIntoView(true);
 		} else {
 			debug("goto top failed");
 		} 
@@ -665,9 +705,10 @@ function retrieveFile(thefile)
 	callServer("open",processor,"file=" + escape(thefile)); 
 }
 
-function showLibrary(title,callback)
+function showLibrary(title,callback,reloadDialog)
 { 
-	var req = null; 
+	var req = null;
+        dialogBox.reload = reloadDialog; 
         // pause();
 	if (window.XMLHttpRequest)
 	{
@@ -696,7 +737,7 @@ function showLibrary(title,callback)
 			if(stat == 200)
 			{
 			  debug(req.responseText);
-			  showDialog("<H2>" + title + "</H2>",req.responseText, callback);
+                          showDialog("<H2>" + title + "</H2>",req.responseText, callback);
 			} 
 		} 
 	};
@@ -739,7 +780,7 @@ function uploadOK()
 function openDialog()
 {  
 	callback = function (fname) { retrieveFile(fname); };
-	showLibrary("Open file", callback);
+	showLibrary("Open file", callback, openDialog);
 }
 
 function saveDialog()
@@ -751,7 +792,7 @@ function saveDialog()
 		   (unlocked.innerHTML.html_to_matita()).sescape(),
 	 	   false,saveDialog); 
         };
-	showLibrary("Save file as", callback);
+	showLibrary("Save file as", callback, saveDialog);
 }
 
 function newDialog()
@@ -760,7 +801,7 @@ function newDialog()
 	  dialogBox.style.display = "none";
 	  saveFile(fname,"","",false,newDialog,true);
 	};
-	showLibrary("Create new file", callback);
+	showLibrary("Create new file", callback, newDialog);
 }
 
 
@@ -802,6 +843,30 @@ function saveFile(fname,lockedtxt,unlockedtxt,force,reloadDialog,reloadFile)
 	else { debug("no file selected"); }
 }
 
+function createDir() {
+   abortDialog();
+   dirname = prompt("New directory name:\ncic:/matita/","newdir");
+   if (dirname != null) {
+        if (dirname.substr(0,1) != "/")
+          dirname = "/" + dirname;
+	processor = function(xml) {
+		if (is_defined(xml)) {
+		  if (xml.childNodes[0].textContent != "ok") {
+                      alert("An error occurred :-(");
+		  }
+		} else {
+                      alert("An error occurred :-(");
+		}
+                dialogBox.reload();
+	};
+        pause();
+        callServer("save",processor,"file=" + escape(dirname) + 
+                                    "&locked=&unlocked=&force=false&dir=true");
+   } else {
+      dialogBox.reload();
+   }
+}
+
 function commitAll()
 {
 	processor = function(xml) {
@@ -816,6 +881,20 @@ function commitAll()
         callServer("commit",processor);
 }
 
+function updateAll()
+{
+	processor = function(xml) {
+		if (is_defined(xml)) {
+			debug("update succeeded(?)");
+		} else {
+			debug("update failed!");
+		}
+		resume();
+	};
+        pause();
+        callServer("update",processor);
+}
+
 var goalcell;
 
 function hideSequent() {
diff --git a/matitaB/matita/netplex.conf b/matitaB/matita/netplex.conf
index 858ea6e8e..5e947c28b 100644
--- a/matitaB/matita/netplex.conf
+++ b/matitaB/matita/netplex.conf
@@ -116,6 +116,13 @@ netplex {
             handler = "commit";
           }
         };
+        uri {
+          path = "/update";
+          service {
+            type = "dynamic";
+            handler = "update";
+          }
+        };
       };
     };
     workload_manager {