diff --git a/src/commands/verify_program.rs b/src/commands/verify_program.rs index 4f79464..bfc32d8 100644 --- a/src/commands/verify_program.rs +++ b/src/commands/verify_program.rs @@ -1,10 +1,11 @@ pub fn run

(program_path: P, specification_path: P, - proof_direction: crate::problem::ProofDirection, no_simplify: bool) + proof_direction: crate::problem::ProofDirection, no_simplify: bool, + color_choice: crate::output::ColorChoice) where P: AsRef, { //let context = crate::translate::verify_properties::Context::new(); - let mut problem = crate::Problem::new(); + let mut problem = crate::Problem::new(color_choice); log::info!("reading specification “{}”", specification_path.as_ref().display()); diff --git a/src/error.rs b/src/error.rs index 738ed3e..eae125a 100644 --- a/src/error.rs +++ b/src/error.rs @@ -22,6 +22,7 @@ pub enum Kind //ParseConstantDeclaration, UnknownProofDirection(String), UnknownDomainIdentifier(String), + UnknownColorChoice(String), VariableNameNotAllowed(String), FormulaNotClosed(std::rc::Rc), NoCompletedDefinitionFound(std::rc::Rc), @@ -142,6 +143,11 @@ impl Error Self::new(Kind::UnknownDomainIdentifier(domain_identifier)) } + pub(crate) fn new_unknown_color_choice(color_choice: String) -> Self + { + Self::new(Kind::UnknownColorChoice(color_choice)) + } + pub(crate) fn new_variable_name_not_allowed(variable_name: String) -> Self { Self::new(Kind::VariableNameNotAllowed(variable_name)) @@ -230,6 +236,8 @@ impl std::fmt::Debug for Error "unknown proof direction “{}” (allowed: integer, program)", proof_direction), Kind::UnknownDomainIdentifier(ref domain_identifier) => write!(formatter, "unknown domain identifier “{}” (allowed: int, program)", domain_identifier), + Kind::UnknownColorChoice(ref color_choice) => write!(formatter, + "unknown color choice “{}” (allowed: auto, always, never)", color_choice), Kind::VariableNameNotAllowed(ref variable_name) => write!(formatter, "variable name “{}” not allowed (program variables must start with X, Y, or Z and integer variables with I, J, K, L, M, or N)", variable_name), diff --git a/src/main.rs b/src/main.rs index 3ed04d8..ff4c514 100644 --- a/src/main.rs +++ b/src/main.rs @@ -23,6 +23,10 @@ enum Command /// Do not simplify translated program #[structopt(long)] no_simplify: bool, + + /// Whether to use colors in the output (auto, always, never) + #[structopt(name = "color", long, default_value = "auto")] + color_choice: anthem::output::ColorChoice, } } @@ -40,8 +44,9 @@ fn main() specification_path, proof_direction, no_simplify, + color_choice, } => anthem::commands::verify_program::run(&program_path, &specification_path, - proof_direction, no_simplify), + proof_direction, no_simplify, color_choice), } } diff --git a/src/output.rs b/src/output.rs index e097a73..40f8569 100644 --- a/src/output.rs +++ b/src/output.rs @@ -1,6 +1,7 @@ pub(crate) mod shell; pub(crate) mod tptp; +pub use shell::ColorChoice; pub(crate) use shell::Shell; #[derive(Clone, Copy, Debug, Eq, Ord, PartialEq, PartialOrd)] diff --git a/src/output/shell.rs b/src/output/shell.rs index bc4ba87..740f60c 100644 --- a/src/output/shell.rs +++ b/src/output/shell.rs @@ -6,12 +6,7 @@ pub struct Shell enum ShellOutput { Basic(Box), - WithColorSupport - { - stream: termcolor::StandardStream, - color_choice: ColorChoice, - is_a_tty: bool, - }, + WithColorSupport(termcolor::StandardStream), } #[derive(Clone, Copy, Eq, PartialEq)] @@ -24,16 +19,15 @@ pub enum ColorChoice impl Shell { - pub fn from_stdout() -> Self + pub fn from_stdout(color_choice: ColorChoice) -> Self { Self { - output: ShellOutput::WithColorSupport + output: match color_choice { - stream: - termcolor::StandardStream::stdout(ColorChoice::Auto.to_termcolor_color_choice()), - color_choice: ColorChoice::Auto, - is_a_tty: atty::is(atty::Stream::Stdout), + ColorChoice::Never => ShellOutput::Basic(Box::new(std::io::stdout())), + _ => ShellOutput::WithColorSupport(termcolor::StandardStream::stdout( + color_choice.to_termcolor_color_choice())), }, } } @@ -67,7 +61,7 @@ impl ShellOutput match *self { Self::Basic(ref mut write) => write!(write, "{}", text), - Self::WithColorSupport{ref mut stream, ..} => + Self::WithColorSupport(ref mut stream) => { stream.reset()?; stream.set_color(color)?; @@ -89,7 +83,7 @@ impl ShellOutput match *self { Self::Basic(ref mut write) => writeln!(write, ""), - Self::WithColorSupport{ref mut stream, ..} => writeln!(stream, ""), + Self::WithColorSupport(ref mut stream) => writeln!(stream, ""), } } @@ -103,7 +97,7 @@ impl ShellOutput let _ = match *self { Self::Basic(ref mut write) => write.write_all(erase_sequence), - Self::WithColorSupport{ref mut stream, ..} => stream.write_all(erase_sequence), + Self::WithColorSupport(ref mut stream) => stream.write_all(erase_sequence), }; } } @@ -124,3 +118,32 @@ impl ColorChoice } } } + +impl std::fmt::Debug for ColorChoice +{ + fn fmt(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result + { + match self + { + ColorChoice::Always => write!(formatter, "always"), + ColorChoice::Never => write!(formatter, "never"), + ColorChoice::Auto => write!(formatter, "auto"), + } + } +} + +impl std::str::FromStr for ColorChoice +{ + type Err = crate::Error; + + fn from_str(s: &str) -> Result + { + match s + { + "always" => Ok(ColorChoice::Always), + "never" => Ok(ColorChoice::Never), + "auto" => Ok(ColorChoice::Auto), + _ => Err(crate::Error::new_unknown_color_choice(s.to_string())), + } + } +} diff --git a/src/problem.rs b/src/problem.rs index 5c89e83..04df4a7 100644 --- a/src/problem.rs +++ b/src/problem.rs @@ -28,7 +28,7 @@ pub struct Problem impl Problem { - pub fn new() -> Self + pub fn new(color_choice: crate::output::ColorChoice) -> Self { Self { @@ -37,7 +37,7 @@ impl Problem statements: std::cell::RefCell::new(std::collections::BTreeMap::new()), - shell: std::cell::RefCell::new(crate::output::Shell::from_stdout()), + shell: std::cell::RefCell::new(crate::output::Shell::from_stdout(color_choice)), } }