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>
</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">
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)
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 ()
;;
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
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
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
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 *)
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);
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
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
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
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,
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] (); *)
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\""
~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()
;;
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) =
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;
(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) =
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
*)
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\""
"<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()
;;
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
; "reset", do_resetlib
; "viewlib", do_viewlib
; "save", do_save
- ; "commit", do_commit]
+ ; "commit", do_commit
+ ; "update", do_update]
() in
MatitaInit.initialize_all ();
MatitaAuthentication.deserialize ();
margin-left: auto;
margin-right: auto;
border: 1px solid #ccc;
- height:440px;
+ height:415px;
width:442px;
overflow:auto;
background-color: white;
display: block;
margin-left: auto;
margin-right: auto;
- height:70%;
+ height:88%;
width:100%;
}
img.topimg {
bottom:0px;
+ border:none;
}
div.scriptarea {
margin-left: auto;
margin-right: auto;
height:100%;
- width:100%;
+ width:67%%;
min-width:67%;
+ max-width:67%;
float:left;
}
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;
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) {
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();
}
}
}
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);
}
}
+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)
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");
}
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)
{
if(stat == 200)
{
debug(req.responseText);
- showDialog("<H2>" + title + "</H2>",req.responseText, callback);
+ showDialog("<H2>" + title + "</H2>",req.responseText, callback);
}
}
};
function openDialog()
{
callback = function (fname) { retrieveFile(fname); };
- showLibrary("Open file", callback);
+ showLibrary("Open file", callback, openDialog);
}
function saveDialog()
(unlocked.innerHTML.html_to_matita()).sescape(),
false,saveDialog);
};
- showLibrary("Save file as", callback);
+ showLibrary("Save file as", callback, saveDialog);
}
function newDialog()
dialogBox.style.display = "none";
saveFile(fname,"","",false,newDialog,true);
};
- showLibrary("Create new file", callback);
+ showLibrary("Create new file", callback, newDialog);
}
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) {
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() {
handler = "commit";
}
};
+ uri {
+ path = "/update";
+ service {
+ type = "dynamic";
+ handler = "update";
+ }
+ };
};
};
workload_manager {
projects / helm.git / commitdiff