Back and Forward on a device: match history entries by component id

Opening a sheet on a device rebuilds the DOM, so every element is new and
the history, which matched by identity, pruned each sheet as soon as it was
recorded. On a device entries now match by id, and Back reopens a view on
the current element rather than the snapshot it was recorded with.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
This commit is contained in:
2026-10-06 23:34:21 +03:00
co-authored by Claude Opus 5.5
parent b074531795
commit 91d92d6525
2 changed files with 43 additions and 6 deletions
+1 -1
View File
@@ -8,7 +8,7 @@ so later rebinding would only ever be seen by the module that did it.
import configparser import configparser
import os 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") PROPERTIES_FILE = os.path.join(os.path.dirname(os.path.abspath(__file__)), "editor.properties")
DEFAULT_GRID_SIZE = 10 DEFAULT_GRID_SIZE = 10
DEFAULT_ADD_TIMESTAMP = True DEFAULT_ADD_TIMESTAMP = True
+42 -5
View File
@@ -2024,6 +2024,37 @@ def _sync_pane_toggle_button():
# --- Sheet view history --- # --- 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): def _tree_item_for_element(element):
"""The tree item whose sheet is this element's children, or None if it is gone. """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() children = tree.get_children()
return children[0] if children else None return children[0] if children else None
for item_id, mapped in app_state.tree_element_map.items(): for item_id, mapped in app_state.tree_element_map.items():
if mapped is element: if _same_element(mapped, element):
return item_id return item_id
return None return None
@@ -2070,7 +2101,7 @@ def _prune_view_history():
# and a Back that visibly does nothing is worse than a shorter trail. The # 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 # position still lands on whichever of the two it was on, since they are the
# same view either way. # 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: if position <= history_index:
new_index = len(kept) - 1 new_index = len(kept) - 1
continue continue
@@ -2134,11 +2165,12 @@ def record_visit(kind, element):
view_history.clear() view_history.clear()
history_index = -1 history_index = -1
# Opening what is already on screen is not a move. Compared by identity, since two # Opening what is already on screen is not a move. Compared by identity in a file,
# sheets are the same sheet only when they are the same element. # 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): if 0 <= history_index < len(view_history):
current_kind, current_element = view_history[history_index] 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 return
del view_history[history_index + 1:] del view_history[history_index + 1:]
@@ -2161,6 +2193,11 @@ def _show_history_entry(position):
if not _entry_is_reachable((kind, element)): if not _entry_is_reachable((kind, element)):
return 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 _suppress_history = True
try: try:
if kind == VIEW_SHEET: if kind == VIEW_SHEET: