add EMIT_NEWLINE to add newlines to readline input only after query terms begin to be read (#1074, #1897)

This commit is contained in:
Mark
2023-07-20 09:39:06 -06:00
parent 4fd247f881
commit dcd7360b17
2 changed files with 13 additions and 3 deletions

View File

@@ -5797,6 +5797,7 @@ impl Machine {
pub(crate) fn read_query_term(&mut self) -> CallResult {
self.user_input.reset();
set_emit_newline(true);
set_prompt(true);
// let result = self.machine_st.read_term(self.user_input, &mut self.indices);
let result = self.machine_st.read_term_from_user_input(self.user_input, &mut self.indices);

View File

@@ -80,9 +80,16 @@ impl MachineState {
}
static mut PROMPT: bool = false;
static mut EMIT_NEWLINE: bool = false;
const HISTORY_FILE: &'static str = ".scryer_history";
pub(crate) fn set_emit_newline(value: bool) {
unsafe {
EMIT_NEWLINE = value;
}
}
pub(crate) fn set_prompt(value: bool) {
unsafe {
PROMPT = value;
@@ -161,10 +168,12 @@ impl ReadlineStream {
self.save_history();
PROMPT = false;
}
}
if self.pending_input.get_ref().get_ref().chars().last() != Some('\n') {
*self.pending_input.get_mut().get_mut() += "\n";
if EMIT_NEWLINE {
if self.pending_input.get_ref().get_ref().chars().last() != Some('\n') {
*self.pending_input.get_mut().get_mut() += "\n";
}
}
}
Ok(self.pending_input.get_ref().get_ref().len())