Partial implementation of "go to cursor" action.

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

diff --git a/matitaB/matita/matitadaemon.ml b/matitaB/matita/matitadaemon.ml
index 95ddb1800be1f950d195eb98829437c03ef6f150..f6e686c531ff5c4e79476b280d8164708cf645ef 100644 (file)
--- a/matitaB/matita/matitadaemon.ml
+++ b/matitaB/matita/matitadaemon.ml
@@ -27,11 +27,16 @@ let eval_statement include_paths (* (buffer : GText.buffer) *) status (* script
   let _,lend = HExtlib.loc_of_floc floc in 
   let parsed_text, parsed_text_len = 
     MatitaGtkMisc.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 
+      (String.length unparsed_text - byte_parsed_text_len)
+  in
   
   let status = 
     MatitaEngine.eval_ast ~include_paths ~do_heavy_checks:false status ("",0,ast)
   in 
-  (status, parsed_text),"",(*parsed_text_len*) Glib.Utf8.length parsed_text
+  (status, parsed_text, unparsed_txt'),"",(*parsed_text_len*) Glib.Utf8.length parsed_text
 
 
 let status = ref (new MatitaEngine.status "cic:/matita");;
@@ -94,8 +99,10 @@ let output_status s =
   String.concat "\n\n" txt
 ;; *)
 
+(* returns the length of the executed text and an html representation of the
+ * current metasenv*)
 let advance text (* (?bos=false) *) =
-     let (st,new_statements),(* newtext TODO *) _,parsed_len =
+     let (st,new_statements,new_unparsed),(* newtext TODO *) _,parsed_len =
        (* try *)
          eval_statement include_paths (*buffer*) !status (`Raw text)
        (* with End_of_file -> raise Margin *)
@@ -103,7 +110,31 @@ let advance text (* (?bos=false) *) =
      status := st;
      history := st :: !history;
      let txt = output_status !status in
-     parsed_len, txt
+     parsed_len, new_unparsed, txt
+;;
+
+let heading_nl_RE = Pcre.regexp "^\\s*\n\\s*";;
+
+let first_line s =
+  let s = Pcre.replace ~rex:heading_nl_RE s in
+  try
+    let nl_pos = String.index s '\n' in
+    String.sub s 0 nl_pos
+  with Not_found -> s
+;;
+
+let gotoBottom =
+  let rec aux parsed_len metasenv text =
+    try
+      prerr_endline ("evaluating: " ^ first_line text);
+      let plen,new_unparsed,cur_metasenv = advance text in
+      aux (parsed_len+plen) cur_metasenv new_unparsed
+    with 
+    | End_of_file -> parsed_len, metasenv
+    | _ -> 
+       prerr_endline ("goto bottom debug: metasenv = \n" ^ metasenv);
+       parsed_len, metasenv
+  in aux 0 ""
 ;;
 
 let retract () =
@@ -127,7 +158,7 @@ let read_file fname =
        lines := input_line chan :: !lines
      done;
    with End_of_file -> close_in chan);
-  String.concat "\r\n" (List.rev !lines)
+  String.concat "\n" (List.rev !lines)
 ;;
 
 let load_index outchan =
@@ -137,7 +168,12 @@ let load_index outchan =
 
 let load_doc filename outchan =
   let s = read_file filename in
-  Http_daemon.respond ~headers:["Content-Type", "text/html"] ~code:(`Code 200) ~body:s outchan
+  let is_png = 
+    try String.sub filename (String.length filename - 4) 4 = ".png"
+    with Invalid_argument _ -> false
+  in
+  let contenttype = if is_png then "image/png" else "text/html" in
+  Http_daemon.respond ~headers:["Content-Type", contenttype] ~code:(`Code 200) ~body:s outchan
 ;;
 
 let call_service outchan =
@@ -199,10 +235,30 @@ let callback req outchan =
   | "/advance" ->
       let script = req#body in
       prerr_endline ("body length = " ^ (string_of_int (String.length script)));
-      let (parsed_len,txt), res, code =
+      let (parsed_len,_,txt), res, code =
         try advance script, "OK", `Code 200
         with 
         | HExtlib.Localized(_,e) 
+        | e -> 
+                (prerr_endline ("exception: " ^ Printexc.to_string e);
+                (try 
+                  NTacStatus.pp_tac_status !status
+                with e -> prerr_endline ("inner exception: " ^
+                  Printexc.to_string e));
+                prerr_endline "end status";
+                let txt = output_status !status in
+                (0,"",txt), Printexc.to_string e, `Code 500)
+      in
+      (* prerr_endline ("server response:\n" ^ txt); *)
+      let body = (string_of_int parsed_len) ^ "@" ^ txt in
+      Http_daemon.respond ~code ~body outchan
+  | "/bottom" ->
+      let script = req#body in
+      prerr_endline ("body length = " ^ (string_of_int (String.length script)));
+      let (parsed_len,txt), res, code =
+        try gotoBottom script, "OK", `Code 200
+        with 
+        | HExtlib.Localized(_,e) 
         | e -> 
                 (prerr_endline ("exception: " ^ Printexc.to_string e);
                 (try 
@@ -213,7 +269,7 @@ let callback req outchan =
                 let txt = output_status !status in
                 (0,txt), Printexc.to_string e, `Code 500)
       in
-      prerr_endline ("server response:\n" ^ txt);
+      (* prerr_endline ("server response:\n" ^ txt); *)
       let body = (string_of_int parsed_len) ^ "@" ^ txt in
       Http_daemon.respond ~code ~body outchan
   | "/retract" ->