From acf77bb24694158a57444c7f32da46ceac8b30c4 Mon Sep 17 00:00:00 2001 From: Wilmer Ricciotti Date: Tue, 6 Sep 2011 12:00:20 +0000 Subject: [PATCH] First attempt at svn commit of developments. Fixes a problem with hyperlinks (the tag was not consumed correctly if it appeared at the end of a command/tactic). --- matitaB/components/METAS/meta.helm-extlib.src | 2 +- .../content_pres/cicNotationLexer.ml | 106 +++++++++----- .../content_pres/cicNotationParser.ml | 22 ++- matitaB/components/extlib/hExtlib.ml | 6 + matitaB/components/extlib/hExtlib.mli | 2 + .../ng_disambiguation/nCicDisambiguate.ml | 2 +- matitaB/matita/Makefile | 1 - matitaB/matita/index.html | 4 +- matitaB/matita/matitaEngine.ml | 27 ++++ matitaB/matita/matitaEngine.mli | 2 + matitaB/matita/matitaFilesystem.ml | 42 ++++++ matitaB/matita/matitaFilesystem.mli | 6 + matitaB/matita/matitaScript.ml | 30 +--- matitaB/matita/matitadaemon.ml | 131 ++++++++++++++++-- matitaB/matita/matitaweb.js | 99 ++++++++++--- matitaB/matita/netplex.conf | 14 ++ 16 files changed, 392 insertions(+), 104 deletions(-) diff --git a/matitaB/components/METAS/meta.helm-extlib.src b/matitaB/components/METAS/meta.helm-extlib.src index a355cb2da..d0cd02bf4 100644 --- a/matitaB/components/METAS/meta.helm-extlib.src +++ b/matitaB/components/METAS/meta.helm-extlib.src @@ -1,4 +1,4 @@ -requires="str unix camlp5.gramlib" +requires="str unix camlp5.gramlib netstring" version="0.0.1" archive(byte)="extlib.cma" archive(native)="extlib.cmxa" diff --git a/matitaB/components/content_pres/cicNotationLexer.ml b/matitaB/components/content_pres/cicNotationLexer.ml index f5e8ba010..f85d2e776 100644 --- a/matitaB/components/content_pres/cicNotationLexer.ml +++ b/matitaB/components/content_pres/cicNotationLexer.ml @@ -82,12 +82,13 @@ let regexp hreftitle = "title=" qstring let regexp hrefclose = xmarkup "/" [ 'A' 'a' ] ymarkup let regexp tag_cont = ident_letter | xml_digit | "_" | "-" -let regexp tagname = ident_letter tag_cont* -let regexp opentag = xmarkup tagname -let regexp closetag = xmarkup "/" tagname ymarkup -let regexp attribute = tagname "=" qstring +let regexp gtagname = [ 'B' - 'Z' 'b' - 'z' ] | ident_letter tag_cont+ +let regexp attrname = ident_letter tag_cont* +let regexp gopentag = xmarkup gtagname +let regexp closetag = xmarkup "/" gtagname ymarkup +let regexp attribute = attrname "=" qstring let regexp generictag = - opentag (utf8_blank+ attribute)* ymarkup + gopentag (utf8_blank+ attribute)* ymarkup let regexp tex_token = '\\' ident @@ -329,43 +330,52 @@ let update_table loc desc href loctable = if desc <> None || href <> None then (let s,e = HExtlib.loc_of_floc loc in + prerr_endline (Printf.sprintf "*** [%d,%d] \"%s\",\"%s\"" s e (so_pp href) (so_pp desc)); + + Printf.printf "*** [%d,%d] \"%s\",\"%s\"" + s e (so_pp href) (so_pp desc); LocalizeEnv.add loc (href,desc) loctable) else loctable ;; let level2_ast_token loctable status = - let rec aux desc href = + let rec aux desc href in_tag = lexer | let_rec -> return lexbuf ("LETREC","") | let_corec -> return lexbuf ("LETCOREC","") | we_proved -> return lexbuf ("WEPROVED","") | we_have -> return lexbuf ("WEHAVE","") - | utf8_blank+ -> ligatures_token (aux desc href) lexbuf + | utf8_blank+ -> ligatures_token (aux desc href in_tag) lexbuf | meta -> let s = Ulexing.utf8_lexeme lexbuf in return lexbuf ("META", String.sub s 1 (String.length s - 1)) | implicit -> return lexbuf ("IMPLICIT", "") | placeholder -> return lexbuf ("PLACEHOLDER", "") - | hreftag -> aux_in_tag None None lexbuf - | hrefclose -> aux None None lexbuf + | hreftag -> aux_attr None None lexbuf + | hrefclose -> return lexbuf ("LEXING_ERROR", Ulexing.utf8_lexeme lexbuf) + (* ignore other tags *) | generictag - | closetag -> ligatures_token (aux desc href) lexbuf - | ident -> loctable := - update_table (loc_of_buf lexbuf) desc href !loctable; - handle_keywords lexbuf (fun x -> StringSet.mem x status) "IDENT" + | closetag -> ligatures_token (aux desc href in_tag) lexbuf + | ident -> if in_tag then + aux_close_tag desc href ("IDENT", Ulexing.utf8_lexeme lexbuf) lexbuf + else handle_keywords lexbuf (fun x -> StringSet.mem x status) "IDENT" | variable_ident -> return lexbuf ("IDENT", Ulexing.utf8_lexeme lexbuf) - | pident -> loctable := - update_table (loc_of_buf lexbuf) desc href !loctable; - handle_keywords lexbuf (fun x -> StringSet.mem x status) "PIDENT" - | number -> loctable := - update_table (loc_of_buf lexbuf) desc href !loctable; - return lexbuf ("NUMBER", Ulexing.utf8_lexeme lexbuf) - | tex_token -> loctable := - update_table (loc_of_buf lexbuf) desc href !loctable; - return lexbuf (expand_macro lexbuf) + | pident -> if in_tag then + aux_close_tag desc href ("PIDENT", Ulexing.utf8_lexeme lexbuf) lexbuf + else handle_keywords lexbuf (fun x -> StringSet.mem x status) "PIDENT" + | number -> let token = "NUMBER", Ulexing.utf8_lexeme lexbuf + in + if in_tag then + aux_close_tag desc href token lexbuf + else return lexbuf token + | tex_token -> let token = expand_macro lexbuf + in + if in_tag then + aux_close_tag desc href token lexbuf + else return lexbuf token | nreference -> return lexbuf ("NREF", Ulexing.utf8_lexeme lexbuf) | uri -> return lexbuf ("URI", Ulexing.utf8_lexeme lexbuf) | qstring -> @@ -386,27 +396,53 @@ let level2_ast_token loctable status = Ulexing.utf8_sub_lexeme lexbuf 2 (Ulexing.lexeme_length lexbuf - 4) in return lexbuf ("NOTE", comment) *) - ligatures_token (aux desc href) lexbuf + ligatures_token (aux desc href in_tag) lexbuf | begincomment -> return lexbuf ("BEGINCOMMENT","") | endcomment -> return lexbuf ("ENDCOMMENT","") | eof -> return_eoi lexbuf - | _ -> loctable := - update_table (loc_of_buf lexbuf) desc href !loctable; - return_symbol lexbuf (Ulexing.utf8_lexeme lexbuf) - - and aux_in_tag desc href = lexer - | utf8_blank+ -> ligatures_token (aux_in_tag desc href) lexbuf + | _ -> let token = "SYMBOL", (Ulexing.utf8_lexeme lexbuf) + in + if in_tag then + aux_close_tag desc href token lexbuf + else return lexbuf token + + and aux_attr desc href = lexer + | utf8_blank+ -> ligatures_token (aux_attr desc href) lexbuf | href -> - aux_in_tag desc + aux_attr desc (Some (Ulexing.utf8_sub_lexeme lexbuf 6 (Ulexing.lexeme_length lexbuf - 7))) lexbuf | hreftitle -> - aux_in_tag + aux_attr (Some (Ulexing.utf8_sub_lexeme lexbuf 7 (Ulexing.lexeme_length lexbuf - 8))) href lexbuf - | ">" -> aux desc href lexbuf - | _ -> aux None None lexbuf - in aux None None + | ymarkup -> aux desc href true lexbuf + | _ -> return lexbuf ("LEXING_ERROR", Ulexing.utf8_lexeme lexbuf) + +(* and aux_in_tag desc href = lexer + | ident -> loctable := + update_table (loc_of_buf lexbuf) desc href !loctable; + handle_keywords lexbuf (fun x -> StringSet.mem x status) "IDENT" + | variable_ident -> + return lexbuf ("IDENT", Ulexing.utf8_lexeme lexbuf) + | pident -> loctable := + update_table (loc_of_buf lexbuf) desc href !loctable; + handle_keywords lexbuf (fun x -> StringSet.mem x status) "PIDENT" + | number -> loctable := + update_table (loc_of_buf lexbuf) desc href !loctable; + return lexbuf ("NUMBER", Ulexing.utf8_lexeme lexbuf) + | tex_token -> loctable := + update_table (loc_of_buf lexbuf) desc href !loctable; + return lexbuf (expand_macro lexbuf) + | _ -> loctable := + update_table (loc_of_buf lexbuf) desc href !loctable; + return_symbol lexbuf (Ulexing.utf8_lexeme lexbuf) + *) + and aux_close_tag desc href token = lexer + | hrefclose -> loctable := update_table (loc_of_buf lexbuf) desc href !loctable; + return lexbuf token + | _ -> return lexbuf ("LEXING_ERROR", Ulexing.utf8_lexeme lexbuf) + in aux None None false let rec level1_pattern_token = lexer @@ -416,7 +452,7 @@ let rec level1_pattern_token = | hrefclose -> return lexbuf ("ATAGEND","") | generictag | closetag -> ligatures_token level1_pattern_token lexbuf - | ident ->handle_keywords lexbuf (fun x -> List.mem x level1_keywords) "IDENT" + | ident -> handle_keywords lexbuf (fun x -> List.mem x level1_keywords) "IDENT" | variable_ident -> return lexbuf ("IDENT", Ulexing.utf8_lexeme lexbuf) | pident->handle_keywords lexbuf (fun x->List.mem x level1_keywords) "PIDENT" | color -> return lexbuf ("COLOR", Ulexing.utf8_lexeme lexbuf) diff --git a/matitaB/components/content_pres/cicNotationParser.ml b/matitaB/components/content_pres/cicNotationParser.ml index 8043d73a3..4894218e8 100644 --- a/matitaB/components/content_pres/cicNotationParser.ml +++ b/matitaB/components/content_pres/cicNotationParser.ml @@ -724,10 +724,24 @@ EXTEND let uri,_ = CicNotationLexer.LocalizeEnv.find loc !loctable in match uri with - | Some u -> id, `Uri u - | None -> id, `Ambiguous + | Some u -> + prerr_endline ("trovata interpretazione per " ^ id ^ ": " ^ u); + id, `Uri u + | None -> + prerr_endline ("identificatore ambiguo: " ^ id); + id, `Ambiguous with - | Not_found -> id, `Ambiguous ]]; + | Not_found -> + prerr_endline ("identificatore non trovato: " ^ id); + id, `Ambiguous ]]; + gnum: [ + [ n = NUMBER -> + try + match CicNotationLexer.LocalizeEnv.find loc !loctable with + | _uri, Some interpr -> n, Some (Some "cic:/fakeuri.def(1)",interpr) + | _ -> n,None + with + | Not_found -> n,None ]]; arg: [ [ LPAREN; names = LIST1 gident SEP SYMBOL ","; SYMBOL ":"; ty = term; RPAREN -> @@ -866,7 +880,7 @@ EXTEND | u = URI -> return_term loc (Ast.Ident (NUri.name_of_uri (NUri.uri_of_string u), `Uri u)) | r = NREF -> return_term loc (Ast.NRef (NReference.reference_of_string r)) - | n = NUMBER -> return_term loc (Ast.Num (n, None)) + | (n,interpr) = gnum -> return_term loc (Ast.Num (n, interpr)) | IMPLICIT -> return_term loc (Ast.Implicit `JustOne) | SYMBOL <:unicode> -> return_term loc (Ast.Implicit `Vector) | PLACEHOLDER -> return_term loc Ast.UserInput diff --git a/matitaB/components/extlib/hExtlib.ml b/matitaB/components/extlib/hExtlib.ml index 0b13cd83e..6b2b68d68 100644 --- a/matitaB/components/extlib/hExtlib.ml +++ b/matitaB/components/extlib/hExtlib.ml @@ -687,3 +687,9 @@ let rec list_skip n l = | _, [] -> assert false ;; +let utf8_parsed_text s floc = + let start, stop = loc_of_floc floc in + let len = stop - start in + let res = Netconversion.ustring_sub `Enc_utf8 start len s in + res, String.length res + diff --git a/matitaB/components/extlib/hExtlib.mli b/matitaB/components/extlib/hExtlib.mli index a772d4a53..394f259e4 100644 --- a/matitaB/components/extlib/hExtlib.mli +++ b/matitaB/components/extlib/hExtlib.mli @@ -172,3 +172,5 @@ val chop_prefix: string -> string -> string val touch: string -> unit val profiling_enabled: bool ref + +val utf8_parsed_text : string -> Stdpp.location -> string * int diff --git a/matitaB/components/ng_disambiguation/nCicDisambiguate.ml b/matitaB/components/ng_disambiguation/nCicDisambiguate.ml index b9ea25cfa..95ee85c24 100644 --- a/matitaB/components/ng_disambiguation/nCicDisambiguate.ml +++ b/matitaB/components/ng_disambiguation/nCicDisambiguate.ml @@ -19,7 +19,7 @@ module Ast = NotationPt module NRef = NReference let debug_print s = prerr_endline (Lazy.force s);; -let debug_print _ = ();; +(* let debug_print _ = ();; *) let cic_name_of_name = function | Ast.Ident (n,_) -> n diff --git a/matitaB/matita/Makefile b/matitaB/matita/Makefile index 9a03d41bf..ed24d2c61 100644 --- a/matitaB/matita/Makefile +++ b/matitaB/matita/Makefile @@ -61,7 +61,6 @@ CMLI = \ matitaInit.mli \ $(NULL) WMLI = \ - matitaScriptLexer.mli \ matitaTypes.mli \ matitaMisc.mli \ applyTransformation.mli \ diff --git a/matitaB/matita/index.html b/matitaB/matita/index.html index 75912b578..9a2343aa4 100644 --- a/matitaB/matita/index.html +++ b/matitaB/matita/index.html @@ -27,7 +27,9 @@ title="Execute the script until the current position of the cursor."> Bottom -

+ + +

diff --git a/matitaB/matita/matitaEngine.ml b/matitaB/matita/matitaEngine.ml index 48ff2d360..83eb235fb 100644 --- a/matitaB/matita/matitaEngine.ml +++ b/matitaB/matita/matitaEngine.ml @@ -318,6 +318,33 @@ and assert_ng ~already_included ~compiling ~asserted ~include_paths ?outch ?uid end ;; +let eos status s = + let only_dust_RE = Pcre.regexp "^(\\s|\n|%%[^\n]*\n)*$" in + let rec is_there_only_comments status s = + if Pcre.pmatch ~rex:only_dust_RE s then raise End_of_file; + let strm = + GrafiteParser.parsable_statement status + (Ulexing.from_utf8_string s) in + match GrafiteParser.parse_statement status strm with + | GrafiteAst.Comment (loc,_) -> + let _,parsed_text_length = HExtlib.utf8_parsed_text s loc in + (* CSC: why +1 in the following lines ???? *) + let parsed_text_length = parsed_text_length + 1 in + let remain_len = String.length s - parsed_text_length in + let next = String.sub s parsed_text_length remain_len in + is_there_only_comments status next + | GrafiteAst.Executable _ -> false + in + try is_there_only_comments status s + with + | NCicLibrary.IncludedFileNotCompiled _ + | HExtlib.Localized _ + | CicNotationParser.Parse_error _ -> false + | End_of_file -> true + | Invalid_argument "Array.make" -> false +;; + + let assert_ng ~include_paths ?outch mapath = snd (assert_ng ~include_paths ~already_included:[] ~compiling:[] ~asserted:[] ?outch mapath) diff --git a/matitaB/matita/matitaEngine.mli b/matitaB/matita/matitaEngine.mli index 3bbc6a113..ea19ef41d 100644 --- a/matitaB/matita/matitaEngine.mli +++ b/matitaB/matita/matitaEngine.mli @@ -51,3 +51,5 @@ val eval_ast : GrafiteTypes.status val assert_ng: include_paths:string list -> ?outch:out_channel -> string -> bool + +val eos : GrafiteTypes.status -> string -> bool diff --git a/matitaB/matita/matitaFilesystem.ml b/matitaB/matita/matitaFilesystem.ml index 49091b2f5..ffdf9bb0d 100644 --- a/matitaB/matita/matitaFilesystem.ml +++ b/matitaB/matita/matitaFilesystem.ml @@ -25,6 +25,10 @@ exception SvnError of string;; +let mutex = Mutex.create ();; + +let to_be_committed = ref [];; + let exec_process cmd = let (stdout, stdin, stderr) as chs = Unix.open_process_full cmd [||] in let outlines = ref [] in @@ -48,6 +52,8 @@ let exec_process cmd = errno, output ^ "\n\n" ^ errors | _ -> assert false)) +(* 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 @@ -113,3 +119,39 @@ let reset_lib () = let to_be_removed = (Helm_registry.get "matita.rt_base_dir") ^ "/users/*" in ignore (Sys.command ("rm -rf " ^ to_be_removed)) ;; + +(* adds a user to the commit queue; concurrent instances possible, so we + * enclose the update in a CS + *) +let add_user uid = + Mutex.lock mutex; + to_be_committed := uid::List.filter (fun x -> x <> uid) !to_be_committed; + Mutex.unlock mutex; +;; + +(* 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 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 + ("svn ci --message \"commit by user " ^ user ^ "\" " ^ rt_dir ^ "/users/" ^ user ^ "/") + in + if errno = 0 then () + else raise (SvnError outstr) + +let do_global_commit () = + prerr_endline ("to be committed: " ^ String.concat " " !to_be_committed); + List.fold_left + (fun acc u -> + try + commit u; + acc + with + | SvnError outstr -> + prerr_endline outstr; + u::acc) + [] (List.rev !to_be_committed) +;; diff --git a/matitaB/matita/matitaFilesystem.mli b/matitaB/matita/matitaFilesystem.mli index 275ebff5b..ed840d230 100644 --- a/matitaB/matita/matitaFilesystem.mli +++ b/matitaB/matita/matitaFilesystem.mli @@ -5,3 +5,9 @@ val checkout : string -> unit val html_of_library : string -> string val reset_lib : unit -> unit + +(* val commit : string -> unit *) + +val add_user : string -> unit + +val do_global_commit : unit -> string list diff --git a/matitaB/matita/matitaScript.ml b/matitaB/matita/matitaScript.ml index 69859470f..aa51b36a0 100644 --- a/matitaB/matita/matitaScript.ml +++ b/matitaB/matita/matitaScript.ml @@ -180,12 +180,12 @@ and eval_statement include_paths (buffer : GText.buffer) status script | `Ast (st, text) -> st, text in let text_of_loc floc = - let nonskipped_txt,_ = MatitaGtkMisc.utf8_parsed_text unparsed_text floc in + let nonskipped_txt,_ = HExtlib.utf8_parsed_text unparsed_text floc in let start, stop = HExtlib.loc_of_floc floc in let floc = HExtlib.floc_of_loc (0, start) in - let skipped_txt,_ = MatitaGtkMisc.utf8_parsed_text unparsed_text floc in + let skipped_txt,_ = HExtlib.utf8_parsed_text unparsed_text floc in let floc = HExtlib.floc_of_loc (0, stop) in - let txt,len = MatitaGtkMisc.utf8_parsed_text unparsed_text floc in + let txt,len = HExtlib.utf8_parsed_text unparsed_text floc in txt,nonskipped_txt,skipped_txt,len in match st with @@ -1023,29 +1023,7 @@ object (self) | _::[] -> true | _ -> false - method eos = - let rec is_there_only_comments status s = - if Pcre.pmatch ~rex:only_dust_RE s then raise Margin; - let strm = - GrafiteParser.parsable_statement status - (Ulexing.from_utf8_string s)in - match GrafiteParser.parse_statement status strm with - | GrafiteAst.Comment (loc,_) -> - let _,parsed_text_length = MatitaGtkMisc.utf8_parsed_text s loc in - (* CSC: why +1 in the following lines ???? *) - let parsed_text_length = parsed_text_length + 1 in - let remain_len = String.length s - parsed_text_length in - let next = String.sub s parsed_text_length remain_len in - is_there_only_comments status next - | GrafiteAst.Executable _ -> false - in - try is_there_only_comments self#status self#getFuture - with - | NCicLibrary.IncludedFileNotCompiled _ - | HExtlib.Localized _ - | CicNotationParser.Parse_error _ -> false - | Margin | End_of_file -> true - | Invalid_argument "Array.make" -> false + method eos = MatitaEngine.eos self#status self#getFuture (* debug *) method dump () = diff --git a/matitaB/matita/matitadaemon.ml b/matitaB/matita/matitadaemon.ml index 5d745eab7..c21bed2e7 100644 --- a/matitaB/matita/matitadaemon.ml +++ b/matitaB/matita/matitadaemon.ml @@ -9,12 +9,6 @@ let libdir uid = (rt_path ()) ^ "/users/" ^ uid let utf8_length = Netconversion.ustring_length `Enc_utf8 -let utf8_parsed_text s floc = - let start, stop = HExtlib.loc_of_floc floc in - let len = stop - start in - let res = Netconversion.ustring_sub `Enc_utf8 start len s in - res, String.length res - (*** from matitaScript.ml ***) (* let only_dust_RE = Pcre.regexp "^(\\s|\n|%%[^\n]*\n)*$" *) @@ -38,7 +32,7 @@ let eval_statement include_paths (* (buffer : GText.buffer) *) status (* script let _,lend = HExtlib.loc_of_floc floc in let parsed_text, _parsed_text_len = - utf8_parsed_text unparsed_text (HExtlib.floc_of_loc (0,lend)) in + HExtlib.utf8_parsed_text unparsed_text (HExtlib.floc_of_loc (0,lend)) in let byte_parsed_text_len = String.length parsed_text in let unparsed_txt' = String.sub unparsed_text byte_parsed_text_len @@ -198,10 +192,12 @@ let retrieve (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = 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 + (* cgi # set_header ~cache:`No_cache ~content_type:"text/xml; charset=\"utf-8\"" (); + *) let filename = libdir uid ^ "/" ^ (cgi # argument_value "file") in prerr_endline ("reading file " ^ filename); let body = @@ -228,20 +224,23 @@ let retrieve (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = include_paths := incpaths; let status = MatitaAuthentication.get_status sid in MatitaAuthentication.set_status sid (status#set_baseuri baseuri); + cgi # set_header + ~cache:`No_cache + ~content_type:"text/xml; charset=\"utf-8\"" + (); cgi#out_channel#output_string body; with | Not_found _ -> cgi # set_header ~status:`Internal_server_error ~cache:`No_cache - ~content_type:"text/xml; charset=\"utf-8\"" + ~content_type:"text/html; charset=\"utf-8\"" ()); cgi#out_channel#commit_work() ;; let advance0 sid text = let status = MatitaAuthentication.get_status sid in - let history = MatitaAuthentication.get_history sid in let status = status#reset_disambiguate_db () in let (st,new_statements,new_unparsed),(* newtext TODO *) _,parsed_len = try @@ -256,7 +255,6 @@ let advance0 sid text = ignore (SmallLexer.mk_small_printer interpr outstr stringbuf); prerr_endline ("parser output: " ^ !outstr); MatitaAuthentication.set_status sid st; - MatitaAuthentication.set_history sid (st::history); parsed_len, Netencoding.Html.encode ~in_enc:`Enc_utf8 ~prefer_name:false () (html_of_matita !outstr), new_unparsed, st @@ -338,6 +336,67 @@ let logout (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = let text = read_file (rt_path () ^ "/logout.html") in cgi#out_channel#output_string text with + | Not_found _ -> + cgi # set_header + ~status:`Internal_server_error + ~cache:`No_cache + ~content_type:"text/html; charset=\"utf-8\"" + ()); + cgi#out_channel#commit_work() +;; + +let save (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = + let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in + let env = cgi#environment in + (try + let sid = Uuidm.of_string (Netcgi.Cookie.value (env#cookie "session")) in + let sid = HExtlib.unopt sid in + let status = MatitaAuthentication.get_status sid in + let uid = MatitaAuthentication.user_of_session sid in + 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 + prerr_endline ("Matita will save the file for user " ^ uid); + 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; + cgi # set_header + ~cache:`No_cache + ~content_type:"text/xml; charset=\"utf-8\"" + (); + cgi#out_channel#output_string "ok" + 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() +;; + +let initiate_commit (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = + let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in + let env = cgi#environment in + (try + let errors = MatitaFilesystem.do_global_commit () in + prerr_endline ("commit errors: " ^ (String.concat " " errors)); + cgi # set_header + ~cache:`No_cache + ~content_type:"text/xml; charset=\"utf-8\"" + (); + cgi#out_channel#output_string "ok" + with | Not_found _ -> cgi # set_header ~status:`Internal_server_error @@ -355,13 +414,17 @@ let advance (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = (try let sid = Uuidm.of_string (Netcgi.Cookie.value (env#cookie "session")) in let sid = HExtlib.unopt sid in + (* cgi # set_header ~cache:`No_cache ~content_type:"text/xml; charset=\"utf-8\"" (); + *) let text = cgi#argument_value "body" in prerr_endline ("body =\n" ^ text); + let history = MatitaAuthentication.get_history sid in let parsed_len, new_parsed, new_unparsed, new_status = advance0 sid text in + MatitaAuthentication.set_history sid (new_status::history); let txt = output_status new_status in let body = "" ^ @@ -369,6 +432,10 @@ let advance (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = ^ "" in prerr_endline ("sending advance response:\n" ^ body); + cgi # set_header + ~cache:`No_cache + ~content_type:"text/xml; charset=\"utf-8\"" + (); cgi#out_channel#output_string body with | Not_found _ -> @@ -386,6 +453,7 @@ let gotoBottom (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = (try let sid = Uuidm.of_string (Netcgi.Cookie.value (env#cookie "session")) in let sid = HExtlib.unopt sid in + let history = MatitaAuthentication.get_history sid in let rec aux parsed_len parsed_txt text = try @@ -397,13 +465,17 @@ let gotoBottom (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = let status = MatitaAuthentication.get_status sid in GrafiteTypes.Serializer.serialize ~baseuri:(NUri.uri_of_string status#baseuri) status; + if parsed_len > 0 then + MatitaAuthentication.set_history sid (status::history); parsed_len, parsed_txt | _ -> parsed_len, parsed_txt - in + in + (* cgi # set_header ~cache:`No_cache ~content_type:"text/xml; charset=\"utf-8\"" (); + *) let text = cgi#argument_value "body" in prerr_endline ("body =\n" ^ text); let parsed_len, new_parsed = aux 0 "" text in @@ -419,6 +491,10 @@ let gotoBottom (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = ^ "" in*) prerr_endline ("sending goto bottom response:\n" ^ body); + cgi # set_header + ~cache:`No_cache + ~content_type:"text/xml; charset=\"utf-8\"" + (); cgi#out_channel#output_string body with Not_found -> cgi#set_header ~status:`Internal_server_error ~cache:`No_cache @@ -429,13 +505,16 @@ let gotoBottom (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = let retract (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in let env = cgi#environment in + prerr_endline "executing retract"; (try let sid = Uuidm.of_string (Netcgi.Cookie.value (env#cookie "session")) in let sid = HExtlib.unopt sid in + (* cgi # set_header ~cache:`No_cache ~content_type:"text/xml; charset=\"utf-8\"" (); + *) let history = MatitaAuthentication.get_history sid in let new_history,new_status = match history with @@ -443,12 +522,18 @@ let retract (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = history, status | [_] -> (prerr_endline "singleton";failwith "retract") | _ -> (prerr_endline "nil"; assert false) in + prerr_endline "before time_travel"; NCicLibrary.time_travel new_status; + prerr_endline "after time travel"; MatitaAuthentication.set_history sid new_history; MatitaAuthentication.set_status sid new_status; prerr_endline ("after retract history.length = " ^ string_of_int (List.length new_history)); let body = output_status new_status in + cgi # set_header + ~cache:`No_cache + ~content_type:"text/xml; charset=\"utf-8\"" + (); cgi#out_channel#output_string body with _ -> cgi#set_header ~status:`Internal_server_error ~cache:`No_cache @@ -463,13 +548,19 @@ let viewLib (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = let sid = Uuidm.of_string (Netcgi.Cookie.value (env#cookie "session")) in let sid = HExtlib.unopt sid in + (* cgi # set_header ~cache:`No_cache ~content_type:"text/html; charset=\"utf-8\"" (); + *) let uid = MatitaAuthentication.user_of_session sid in let html = MatitaFilesystem.html_of_library uid in + cgi # set_header + ~cache:`No_cache + ~content_type:"text/html; charset=\"utf-8\"" + (); cgi#out_channel#output_string ((* "\n" ^ @@ -594,6 +685,20 @@ let start() = dyn_translator = (fun _ -> ""); (* not needed *) dyn_accept_all_conditionals = false; } in + let do_save = + { Nethttpd_services.dyn_handler = (fun _ -> save); + 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 do_commit = + { Nethttpd_services.dyn_handler = (fun _ -> initiate_commit); + 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 @@ -605,7 +710,9 @@ let start() = ; "login", do_login ; "logout", do_logout ; "reset", do_resetlib - ; "viewlib", do_viewlib] + ; "viewlib", do_viewlib + ; "save", do_save + ; "commit", do_commit] () in MatitaInit.initialize_all (); MatitaAuthentication.deserialize (); diff --git a/matitaB/matita/matitaweb.js b/matitaB/matita/matitaweb.js index fb6c0869d..07dbb06f6 100644 --- a/matitaB/matita/matitaweb.js +++ b/matitaB/matita/matitaweb.js @@ -15,6 +15,7 @@ var dialogBox; var dialogTitle; var dialogContent; var metasenv = ""; +var lockedbackup = ""; function initialize() { @@ -336,6 +337,8 @@ function switch_goal(meta) } } +// the following is used to avoid escaping unicode, which results in +// the server being unable to unescape the string String.prototype.sescape = function() { var patt1 = /%/gi; var patt2 = /=/gi; @@ -469,15 +472,17 @@ function advanceForm1() // debug("advance: received response\nBEGIN\n" + req.responseText + "\nEND"); parsed = xml.getElementsByTagName("parsed")[0]; len = parseInt(parsed.getAttribute("length")); - len0 = unlocked.innerHTML.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); - locked.innerHTML = locked.innerHTML + parsedtxt; //.matita_to_html(); + lockedbackup += parsedtxt; + locked.innerHTML = lockedbackup; unlocked.innerHTML = unparsedtxt.matita_to_html(); - len1 = unlocked.innerHTML.length; - len2 = len0 - len1; + // len1 = unlocked.innerHTML.length; + // len2 = len0 - len1; + len2 = parsedtxt.length; metasenv = xml.getElementsByTagName("meta"); populate_goalarray(metasenv); statements = listcons(len2,statements); @@ -499,19 +504,23 @@ function gotoBottom() // debug("goto bottom: 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); - locked.innerHTML = locked.innerHTML + parsedtxt; //.matita_to_html(); - unlocked.innerHTML = unparsedtxt.matita_to_html(); - len1 = unlocked.innerHTML.length; - len2 = len0 - len1; - metasenv = xml.getElementsByTagName("meta"); - populate_goalarray(metasenv); - statements = listcons(len2,statements); - unlocked.scrollIntoView(true); + if (len > 0) { + // 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; //.matita_to_html(); + unlocked.innerHTML = unparsedtxt.matita_to_html(); + // len1 = unlocked.innerHTML.length; + len2 = parsedtxt.length; + metasenv = xml.getElementsByTagName("meta"); + populate_goalarray(metasenv); + if (len2 > 0) + statements = listcons(len2,statements); + unlocked.scrollIntoView(true); + } } else { debug("goto bottom failed"); } @@ -532,15 +541,16 @@ function gotoPos(offset) if (is_defined(xml)) { parsed = xml.getElementsByTagName("parsed")[0]; len = parseInt(parsed.getAttribute("length")); - len0 = unlocked.innerHTML.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); - locked.innerHTML = locked.innerHTML + parsedtxt; //.matita_to_html(); + lockedbackup += parsedtxt; + locked.innerHTML = lockedbackup; //.matita_to_html(); unlocked.innerHTML = unparsedtxt.matita_to_html(); - len1 = unlocked.innerHTML.length; - len2 = len0 - len1; + // len1 = unlocked.innerHTML.length; + len2 = parsedtxt.length; metasenv = xml.getElementsByTagName("meta"); // populate_goalarray(metasenv); statements = listcons(len2,statements); @@ -569,10 +579,17 @@ function retract() // 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; + */ + lockedlen = lockedbackup.length - statementlen; + statement = lockedbackup.substr(lockedlen, statementlen); + lockedbackup = lockedbackup.substr(0,lockedlen); + locked.innerHTML = lockedbackup; + unlocked.innerHTML = statement + unlocked.innerHTML; metasenv = xml.getElementsByTagName("meta"); populate_goalarray(metasenv); unlocked.scrollIntoView(true); @@ -592,7 +609,8 @@ function openFile() processor = function(xml) { if (is_defined(xml)) { - locked.innerHTML = ""; + lockedbackup = ""; + locked.innerHTML = lockedbackup; unlocked.innerHTML = xml.documentElement.textContent; } else { debug("file open failed"); @@ -606,7 +624,8 @@ function retrieveFile(thefile) processor = function(xml) { if (is_defined(xml)) { - locked.innerHTML = ""; + lockedbackup = "" + locked.innerHTML = lockedbackup; debug(xml.getElementsByTagName("file")[0].childNodes[0].nodeValue); unlocked.innerHTML = xml.getElementsByTagName("file")[0].childNodes[0].nodeValue; @@ -615,6 +634,7 @@ function retrieveFile(thefile) } }; dialogBox.style.display = "none"; + current_fname = thefile; callServer("open",processor,"file=" + escape(thefile)); } @@ -659,6 +679,39 @@ function showLibrary() } +function saveFile() +{ + processor = function(xml) { + if (is_defined(xml)) { + debug("file saved!"); + } else { + debug("save file failed"); + } + resume(); + }; + if (is_defined(current_fname)) { + pause(); + callServer("save",processor,"file=" + escape(current_fname) + + "&locked=" + (locked.innerHTML.html_to_matita()).sescape() + + "&unlocked=" + (unlocked.innerHTML.html_to_matita()).sescape()); + } + else { debug("no file selected"); } +} + +function commitAll() +{ + processor = function(xml) { + if (is_defined(xml)) { + debug("commit succeeded(?)"); + } else { + debug("commit failed!"); + } + resume(); + }; + pause(); + callServer("commit",processor); +} + var goalcell; function hideSequent() { diff --git a/matitaB/matita/netplex.conf b/matitaB/matita/netplex.conf index daa41247d..8764b1738 100644 --- a/matitaB/matita/netplex.conf +++ b/matitaB/matita/netplex.conf @@ -95,6 +95,20 @@ netplex { handler = "reset"; } }; + uri { + path = "/save"; + service { + type = "dynamic"; + handler = "save"; + } + }; + uri { + path = "/commit"; + service { + type = "dynamic"; + handler = "commit"; + } + }; }; }; workload_manager { -- 2.39.2