X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=inline;f=ocaml_new%2Fconsole.ml;fp=ocaml_new%2Fconsole.ml;h=696a74d9abe151e3c873d7267e317ed6e0a7bb96;hb=21c829a0b518a725f4db3d21250ad00dcf3bb889;hp=0000000000000000000000000000000000000000;hpb=4c157f176c89dcb5633d60c5be8a444ae0529c29;p=fireball-separation.git

diff --git a/ocaml_new/console.ml b/ocaml_new/console.ml
new file mode 100644
index 0000000..696a74d
--- /dev/null
+++ b/ocaml_new/console.ml
@@ -0,0 +1,141 @@
+type fancyobj = <
+  to_string : unit -> string;
+  to_html : unit -> string
+>;;
+
+let sepx = "\xe2\xbf\x96";;
+let endx = "\xe2\xbf\x97";;
+
+let socket_name = "/tmp/fancy.log";;
+
+let html_enabled = Sys.file_exists socket_name;;
+
+let socket = let open Unix in
+  if html_enabled
+  then socket PF_UNIX SOCK_STREAM 0
+  else socket PF_INET SOCK_STREAM 0;;
+
+let html_enabled = if html_enabled then
+  try
+    let _ = Unix.connect socket (Unix.ADDR_UNIX socket_name) in true
+  with Unix.Unix_error _ -> false
+  else false
+;;
+
+let cols =
+  let process_output_to_list2 = fun command ->
+    let chan = Unix.open_process_in command in
+    let res = ref ([] : string list) in
+    let rec process_otl_aux () =
+      let e = input_line chan in
+      res := e::!res;
+      process_otl_aux() in
+    try process_otl_aux ()
+    with End_of_file ->
+      let stat = Unix.close_process_in chan in (List.rev !res,stat)
+  in let cmd_to_list command =
+    let (l,_) = process_output_to_list2 command in l
+  in try let lines = cmd_to_list "tput cols" in int_of_string (List.hd (lines))
+  with _ -> 100 (* default value *)
+;;
+
+let writeall s =
+  let _ = Unix.send socket s 0 (String.length s) [] in ()
+;;
+
+let concat ls = (String.concat sepx ls) ^ endx;;
+
+(* HELO message *)
+if html_enabled then
+  writeall(concat["helo"; String.concat " " (Array.to_list Sys.argv)])
+;;
+
+
+(* let logs objs =
+  if html_enabled then (
+    let strs = (List.map (fun x -> x#to_html()) objs) in
+    writeall (concat ("log" :: strs))
+  ); prerr_endline (String.concat " " (List.map (fun x -> x#to_string()) objs))
+;; *)
+
+let html_escape s =
+  let m = [("&", "&amp;"); (">", "&gt;"); ("<", "&lt;"); ("&quot;", "\""); ("&#39;", "'")]
+  in let m = List.map (fun (x,y) -> Str.regexp x, y) m
+  in List.fold_right (fun (x,y) z -> Str.global_replace x y z) m s;; (* FIXME TODO *)
+
+let fancy_of_string s : fancyobj = object
+  method to_string () = s
+  method to_html () = html_escape s
+end;;
+
+let empty = fancy_of_string "";;
+
+let line = ref empty;;
+
+let (/) a b = object
+  method to_string () = a
+  method to_html () = b
+end;;
+
+let (^^) a b = object
+  method to_string () = (a#to_string () ^ "" ^ b#to_string ())
+  method to_html () = a#to_html () ^ " " ^ b#to_html ()
+end;;
+
+(* Output functions on standard output *)
+
+let print_string s =
+  line := !line ^^ fancy_of_string s
+;;
+
+let print_char c =
+  print_string (String.make 1 c)
+;;
+
+(* let print_bytes : bytes -> unit *)
+
+let print_int n =
+  print_string (string_of_int n)
+;;
+
+(* val print_float : float -> unit *)
+
+let print_newline () =
+  if !line <> empty then (
+  Pervasives.print_endline (!line#to_string());
+  if html_enabled then (writeall (concat ["log"; !line#to_html()]));
+  line := empty
+  )
+;;
+
+let print f =
+  line := !line ^^ f
+;;
+
+let print_string_endline f =
+  print (fancy_of_string f); print_newline ()
+;;
+
+let print_endline f =
+  print f; print_newline ()
+;;
+
+let print_hline () =
+  print_newline ();
+  print_endline ( String.make cols '-' / "<hr>")
+;;
+
+let print_heading s =
+  print_newline ();
+  print_endline (("# " ^ s) / ("<h2>" ^ html_escape s ^ "</h2>"))
+;;
+
+let print_bullet f =
+  print_newline ();
+  print_endline (("- " / "<ul><li>") ^^ f ^^ ("" / "</ul>"))
+;;
+
+let print_math s =
+  print_endline ( s / "" );
+  if html_enabled then (writeall (concat ["math"; s]))
+;;