From afa25e79733be21321ac11e558c0291725cbd95a Mon Sep 17 00:00:00 2001 From: Wilmer Ricciotti Date: Tue, 24 May 2011 13:24:53 +0000 Subject: [PATCH] matitaweb: added retract (undo) --- matitaB/components/content_pres/boxPp.ml | 2 +- .../content_pres/cicNotationPres.ml | 2 +- matitaB/matita/Makefile | 1 + matitaB/matita/matitadaemon.ml | 92 +++++++++---------- 4 files changed, 44 insertions(+), 53 deletions(-) diff --git a/matitaB/components/content_pres/boxPp.ml b/matitaB/components/content_pres/boxPp.ml index af11da811..5d406b9fb 100644 --- a/matitaB/components/content_pres/boxPp.ml +++ b/matitaB/components/content_pres/boxPp.ml @@ -28,7 +28,7 @@ (** {2 Pretty printing from BoxML to strings} *) -let utf8_string_length s = Utf8.compute_len s 0 (String.length s) +let utf8_string_length s = Utf8.compute_len s 0 (String.length s) let string_space = " " let string_space_len = utf8_string_length string_space diff --git a/matitaB/components/content_pres/cicNotationPres.ml b/matitaB/components/content_pres/cicNotationPres.ml index e0ca07b56..b99851add 100644 --- a/matitaB/components/content_pres/cicNotationPres.ml +++ b/matitaB/components/content_pres/cicNotationPres.ml @@ -249,7 +249,7 @@ let render status ?(prec=(-1)) = List.map boxify_pres (find_clusters terms) in (fun t -> - prerr_endline ("ast:\n" ^ (NotationPp.pp_term status t)); + (* prerr_endline ("ast:\n" ^ (NotationPp.pp_term status t));*) aux prec t) (* let render_to_boxml id_to_uri t = diff --git a/matitaB/matita/Makefile b/matitaB/matita/Makefile index 25f5d38fe..4f3bea4f7 100644 --- a/matitaB/matita/Makefile +++ b/matitaB/matita/Makefile @@ -21,6 +21,7 @@ OCAML_DEBUG_FLAGS = -g #OCAMLOPT_DEBUG_FLAGS = -p OCAMLC_FLAGS = $(OCAML_FLAGS) $(OCAML_THREADS_FLAGS) OCAMLC = $(OCAMLFIND) ocamlc$(OCAML_PROF) $(OCAMLC_FLAGS) $(OCAML_DEBUG_FLAGS) $(SYNTAXOPTIONS) +OCAMLTOP = $(OCAMLFIND) ocamlmktop$(OCAML_PROF) $(OCAMLC_FLAGS) $(OCAML_DEBUG_FLAGS) $(SYNTAXOPTIONS) OCAMLOPT = $(OCAMLFIND) opt $(OCAMLC_FLAGS) $(OCAMLOPT_DEBUG_FLAGS) OCAMLDEP = $(OCAMLFIND) ocamldep $(OCAMLDEP_FLAGS) INSTALL_PROGRAMS= matita matitac diff --git a/matitaB/matita/matitadaemon.ml b/matitaB/matita/matitadaemon.ml index d1a7e2072..3e37febbd 100644 --- a/matitaB/matita/matitadaemon.ml +++ b/matitaB/matita/matitadaemon.ml @@ -33,55 +33,47 @@ let eval_statement include_paths (* (buffer : GText.buffer) *) status (* script let status = ref (new MatitaEngine.status "cic:/matita");; +let history = ref [!status];; let include_paths = ["/home/barolo/matitaB/matita/lib"];; +let html_of_status s = + let _,_,metasenv,subst,_ = s#obj in + let txt = List.fold_left + (fun acc (nmeta,_ as meta) -> + let txt0 = snd (ApplyTransformation.ntxt_of_cic_sequent + ~metasenv ~subst ~map_unicode_to_tex:false 80 s meta) + in + prerr_endline ("### txt0 = " ^ txt0); + ("Goal ?" ^ (string_of_int nmeta) ^ "\n" ^ txt0)::acc) + [] metasenv + in + String.concat "\n\n" txt +;; + let advance text (* (?bos=false) *) = - (* if bos then LibraryClean.clean_baseuris [self#buri_of_current_file]; - (* HLog.debug ("evaluating: " ^ first_line s ^ " ...");*) - let time1 = Unix.gettimeofday () in - let entries, newtext, parsed_len = *) - let (st,_),_,parsed_len = + let (st,new_statements),(* newtext TODO *) _,parsed_len = (* try *) eval_statement include_paths (*buffer*) !status (`Raw text) (* with End_of_file -> raise Margin *) in - status := st; - let _,_,metasenv,subst,_ = !status#obj in - let txt = List.fold_left - (fun acc (nmeta,_ as meta) -> - let txt0 = snd (ApplyTransformation.ntxt_of_cic_sequent - ~metasenv ~subst ~map_unicode_to_tex:false 80 !status - meta) in - prerr_endline ("### txt0 = " ^ txt0); - ("Goal ?" ^ (string_of_int nmeta) ^ "\n" ^ txt0)::acc) - [] metasenv - in - let txt = String.concat "\n\n" txt in + status := st; + history := st :: !history; + let txt = html_of_status !status in parsed_len, txt - (*in - let time2 = Unix.gettimeofday () in - HLog.debug ("... done in " ^ string_of_float (time2 -. time1) ^ "s"); - let new_statuses, new_statements = - let statuses, texts = List.split entries in - statuses, texts - in - history <- new_statuses @ history; - statements <- new_statements @ statements; - let start = buffer#get_iter_at_mark (`MARK locked_mark) in - let new_text = String.concat "" (List.rev new_statements) in - if statement <> None then - buffer#insert ~iter:start new_text - else begin - let parsed_text = String.sub s 0 parsed_len in - if new_text <> parsed_text then begin - let stop = start#copy#forward_chars (Glib.Utf8.length parsed_text) in - buffer#delete ~start ~stop; - buffer#insert ~iter:start new_text; - end; - end; - self#moveMark (Glib.Utf8.length new_text); - buffer#insert ~iter:(buffer#get_iter_at_mark (`MARK locked_mark)) newtext*) +;; + +let retract () = + let new_history,new_status = + match !history with + _::(status::_ as history) -> + history, status + | [_] -> failwith "retract" + | _ -> assert false in + NCicLibrary.time_travel !status; + history := new_history; + status := new_status; + html_of_status !status ;; let read_file fname = @@ -114,6 +106,7 @@ let call_service outchan = e -> Http_daemon.respond ~code:(`Code 500) outchan ;; + let callback req outchan = let str = (sprintf "request path = %s\n" req#path) ^ @@ -169,22 +162,19 @@ let callback req outchan = with e -> prerr_endline ("inner exception: " ^ Printexc.to_string e)); prerr_endline "end status"; - let _,_,metasenv,subst,_ = !status#obj in - let txt = List.fold_left - (fun acc (nmeta,_ as meta) -> - let txt0 = snd (ApplyTransformation.ntxt_of_cic_sequent - ~metasenv ~subst ~map_unicode_to_tex:false 80 !status - meta) in - prerr_endline ("### txt0 = " ^ txt0); - ("Goal ?" ^ (string_of_int nmeta) ^ "\n" ^ txt0)::acc) - [] metasenv - in - let txt = String.concat "\n\n" txt in + let txt = html_of_status !status in (0,txt), Printexc.to_string e, `Code 500) in let txt = Netencoding.Url.encode ~plus:false txt in let body = (string_of_int parsed_len) ^ "#" ^ txt in Http_daemon.respond ~code ~body outchan + | "/retract" -> + (try + let txt = retract () in + Http_daemon.respond ~code:(`Code 200) ~body:txt outchan + with e -> + (prerr_endline (Printexc.to_string e); + Http_daemon.respond ~code:(`Code 500) outchan)) | url -> Http_daemon.respond_not_found ~url outchan ;; -- 2.39.2