diff --git a/app_state.py b/app_state.py index 0145cbb..c934321 100644 --- a/app_state.py +++ b/app_state.py @@ -8,7 +8,7 @@ so later rebinding would only ever be seen by the module that did it. import configparser import os -VERSION = "0.0.0.159" +VERSION = "0.0.0.160" PROPERTIES_FILE = os.path.join(os.path.dirname(os.path.abspath(__file__)), "editor.properties") DEFAULT_GRID_SIZE = 10 DEFAULT_ADD_TIMESTAMP = True diff --git a/main.py b/main.py index d4f1612..cc5df47 100644 --- a/main.py +++ b/main.py @@ -2024,6 +2024,37 @@ def _sync_pane_toggle_button(): # --- Sheet view history --- +def _same_element(a, b): + """Whether two history elements name the same component. + + In a file that is identity. On a device every sheet opened rebuilds the DOM from the + device, handing out fresh elements for the same components, so there it is the id. + """ + if a is b: + return True + if a is None or b is None or not app_state.live_mode: + return False + a_id = a.get("id") + return a_id is not None and a_id == b.get("id") + + +def _current_element(element): + """The element in the DOM now that names the same component as this one. + + Only a device swaps elements out from under the history; in a file, or when nothing + by that id is left, the element comes back as it was. + """ + if element is None or not app_state.live_mode: + return element + root = app_state.xml_root_element + if root is None: + return element + for candidate in root.iter(): + if _same_element(candidate, element): + return candidate + return element + + def _tree_item_for_element(element): """The tree item whose sheet is this element's children, or None if it is gone. @@ -2038,7 +2069,7 @@ def _tree_item_for_element(element): children = tree.get_children() return children[0] if children else None for item_id, mapped in app_state.tree_element_map.items(): - if mapped is element: + if _same_element(mapped, element): return item_id return None @@ -2070,7 +2101,7 @@ def _prune_view_history(): # and a Back that visibly does nothing is worse than a shorter trail. The # position still lands on whichever of the two it was on, since they are the # same view either way. - if kept and kept[-1][0] == entry[0] and kept[-1][1] is entry[1]: + if kept and kept[-1][0] == entry[0] and _same_element(kept[-1][1], entry[1]): if position <= history_index: new_index = len(kept) - 1 continue @@ -2134,11 +2165,12 @@ def record_visit(kind, element): view_history.clear() history_index = -1 - # Opening what is already on screen is not a move. Compared by identity, since two - # sheets are the same sheet only when they are the same element. + # Opening what is already on screen is not a move. Compared by identity in a file, + # where two sheets are the same sheet only when they are the same element, and by id + # on a device, where each sheet opened hands out fresh elements. if 0 <= history_index < len(view_history): current_kind, current_element = view_history[history_index] - if current_kind == kind and current_element is element: + if current_kind == kind and _same_element(current_element, element): return del view_history[history_index + 1:] @@ -2161,6 +2193,11 @@ def _show_history_entry(position): if not _entry_is_reachable((kind, element)): return + # On a device the entry may hold an element from an earlier rebuild; a panel built on + # that would show the values of that moment, not the device's. + element = _current_element(element) + view_history[position] = (kind, element) + _suppress_history = True try: if kind == VIEW_SHEET: