equal
deleted
inserted
replaced
75 |
75 |
76 def eq_content(other: State): Boolean = |
76 def eq_content(other: State): Boolean = |
77 command.source == other.command.source && |
77 command.source == other.command.source && |
78 status == other.status && |
78 status == other.status && |
79 results == other.results && |
79 results == other.results && |
80 markup == other.markup |
80 markups == other.markups |
81 |
81 |
82 private def add_status(st: Markup): State = copy(status = st :: status) |
82 private def add_status(st: Markup): State = copy(status = st :: status) |
83 |
83 |
84 private def add_markup(file_name: String, m: Text.Markup): State = |
84 private def add_markup(file_name: String, m: Text.Markup): State = |
85 copy(markups = markups + (file_name -> (get_markup(file_name) + m))) |
85 copy(markups = markups + (file_name -> (get_markup(file_name) + m))) |