worker_proto.ml 927 Bytes
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27
type command =  ParseBuffer of string
              | ExecuteBuffer of string
              | Init


type output = Error of string (* msg *)
             | ErrorLoc of ((int*int*int*int) * string) (* loc * msg *)
             | Tasks of ((string * string) (* Theory (id, name) *)
                       * (string * string) (* Task (id, name *)
                       * (string * string * string)) (* VC (id, expl, code ) *)
             | Result of string list

type prover_answer = Valid | Unknown of string | Invalid of string

let marshal a =
  Js.string (String.escaped (Marshal.to_string a [Marshal.No_sharing; Marshal.Compat_32]))

let unmarshal a =
  Marshal.from_string (Scanf.unescaped (Js.to_string a)) 0



let log s = ignore (Firebug.console ## log (Js.string s))
let log_time s =
  let date = jsnew Js.date_now () in
  let date_str = string_of_float ((date ## getTime ()) /. 1000.) in
  log (date_str ^ " : " ^ s)