From: Wilmer Ricciotti Date: Tue, 31 May 2011 13:59:37 +0000 (+0000) Subject: Partial implementation of "go to cursor" action. X-Git-Tag: make_still_working~2476 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=735c93deb88ebc24614e7f2d899a2ed0dd480314;p=helm.git Partial implementation of "go to cursor" action. --- diff --git a/matitaB/matita/index.html b/matitaB/matita/index.html index 98692b5ad..fa119b5ba 100644 --- a/matitaB/matita/index.html +++ b/matitaB/matita/index.html @@ -2,7 +2,7 @@ - + + + +

- +

- + + +

+ +

@@ -415,20 +550,19 @@ function removeElement(id) { inside a PRE tag, a CR will be reflected in the document presentation) -->

-  
(* script lungo lungo lungo lungo lungo lungo lungo lungo lungo lungo lungo lungo lungo lungo lungo lungo lungo lungo lungo lungo lungo lungo lungo lungo *)


(* script *)

lungo lungo lungo lungo lungo lungo lungo lungo lungo lungo lungo lungo lungo lungo lungo lungo lungo lungo lungo lungo lungo lungo lungo lungo

- +

diff --git a/matitaB/matita/matitadaemon.ml b/matitaB/matita/matitadaemon.ml index 95ddb1800..f6e686c53 100644 --- 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" ->