equal
deleted
inserted
replaced
79 |
79 |
80 /* overlays */ |
80 /* overlays */ |
81 |
81 |
82 private var overlays = Document.Overlays.empty |
82 private var overlays = Document.Overlays.empty |
83 |
83 |
84 def add_overlay(command: Command, name: String, args: List[String]): Unit = |
84 def insert_overlay(command: Command, name: String, args: List[String]): Unit = |
85 Swing_Thread.require { overlays += ((command, name, args)) } |
85 Swing_Thread.require { overlays = overlays.insert(command, (name, args)) } |
86 |
86 |
87 def remove_overlay(command: Command, name: String, args: List[String]): Unit = |
87 def remove_overlay(command: Command, name: String, args: List[String]): Unit = |
88 Swing_Thread.require { overlays -= ((command, name, args)) } |
88 Swing_Thread.require { overlays = overlays.remove(command, (name, args)) } |
89 |
89 |
90 |
90 |
91 /* perspective */ |
91 /* perspective */ |
92 |
92 |
93 // owned by Swing thread |
93 // owned by Swing thread |