equal
deleted
inserted
replaced
26 pending_output: Set[JFile] = Set.empty) |
26 pending_output: Set[JFile] = Set.empty) |
27 { |
27 { |
28 def update_models(changed: Iterable[(JFile, VSCode_Model)]): State = |
28 def update_models(changed: Iterable[(JFile, VSCode_Model)]): State = |
29 copy( |
29 copy( |
30 models = models ++ changed, |
30 models = models ++ changed, |
31 pending_input = (pending_input /: changed) { case (set, (file, _)) => set + file }, |
31 pending_input = changed.foldLeft(pending_input) { case (set, (file, _)) => set + file }, |
32 pending_output = (pending_output /: changed) { case (set, (file, _)) => set + file }) |
32 pending_output = changed.foldLeft(pending_output) { case (set, (file, _)) => set + file }) |
33 |
33 |
34 def update_caret(new_caret: Option[(JFile, Line.Position)]): State = |
34 def update_caret(new_caret: Option[(JFile, Line.Position)]): State = |
35 if (caret == new_caret) this |
35 if (caret == new_caret) this |
36 else |
36 else |
37 copy( |
37 copy( |