let rec cmd_rep () =
  let inch = Istate.inchannel() in
  let outch = Istate.outchannel() in
  try
    cmd_output outch (read_from_channel inch);
    Format.fprintf outch "@?"
  with
    | Invalid_argument str -> 
        cmd_error outch str
    | Parsing.Parse_error -> 
        cmd_error outch "Syntax error"
    | End_of_file ->
         cmd_quit 0 outch;
    | Sys.Break -> 
         cmd_quit 1 outch;
    | Failure "drop" -> 
        raise (Failure "drop")
    | exc -> 
        (cmd_error outch ("Exception " ^ (Printexc.to_string exc)))

and cmd_batch () =
  let inch = Istate.inchannel() in
  let outch = Istate.outchannel() in
    try
      Parser.commandsequence Lexer.token (Lexing.from_channel inch)
    with
      | Result.Result(result) -> 
          cmd_output outch result;
          cmd_quit 0 outch
      | Invalid_argument str ->
          cmd_error outch str;
          cmd_quit 3 outch
      | Parsing.Parse_error -> 
          let number =  string_of_int !Tools.linenumber in
            cmd_error outch ("Syntax error on line " ^ number);
            cmd_quit 2 outch
      | End_of_file ->
          cmd_quit 0 outch
      | Sys.Break -> 
          cmd_quit 1 outch
      | Exc.Inconsistent ->
          Format.fprintf outch ":unsat\n@?";
          cmd_quit (-1) outch
      | exc -> 
          cmd_error outch ("Exception " ^ (Printexc.to_string exc));
          cmd_quit 4 outch



and cmd_output fmt result =
  (match result with
     | Result.Process(status) -> 
         Context.Status.pp Name.pp fmt status
     | Result.Sat(None) ->
         Format.fprintf fmt ":unsat@?"
     | Result.Sat(Some(rho, n)) ->
         Format.fprintf fmt ":sat( ";
         Name.pp fmt n;
         Format.fprintf fmt ") ";
         Prop.Assignment.pp fmt rho;
         Format.fprintf fmt "@?"
     | Result.Unit() ->
         Format.fprintf fmt ":unit@?"
     | Result.Bool(true) ->
         Format.fprintf fmt ":true@?"
     | Result.Bool(false) ->
         Format.fprintf fmt ":false@?"
     | value -> 
         Format.fprintf fmt ":val ";
         Result.output fmt value;
         Format.fprintf fmt "@?");
  cmd_endmarker fmt
        
and cmd_error fmt str =
  Format.fprintf fmt ":error %s" str;
  Format.fprintf fmt "\n%s@?" (Istate.eot())

and cmd_quit n fmt =
  do_at_exit();
  Format.fprintf fmt "\n";
  cmd_endmarker fmt;
  exit n

and cmd_endmarker fmt =
  let eot = Istate.eot () in
  if eot = "" then
    Format.pp_print_flush fmt ()
  else 
    begin
      Format.fprintf fmt "\n%s" eot;
      Format.pp_print_flush fmt ()
    end