matitaweb: added retract (undo)

[helm.git] / matitaB / matita / matitadaemon.ml

diff --git a/matitaB/matita/matitadaemon.ml b/matitaB/matita/matitadaemon.ml
index d1a7e207226d759d1992adee1ec80c0fe21a752f..3e37febbd0d759a59e08c29d2e484fdcafd50cdb 100644 (file)
--- 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);
+      ("<B>Goal ?" ^ (string_of_int nmeta) ^ "</B>\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);
-         ("<B>Goal ?" ^ (string_of_int nmeta) ^ "</B>\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);
-                    ("<B>Goal ?" ^ (string_of_int nmeta) ^ "</B>\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  
 
 ;;