last-theory-change

(defun scan-for-current-theory
  (w)
  (if (atom w)
    nil
    (if (and (eq (caar w) 'current-theory)
        (eq (cadar w) 'global-value))
      (cddar w)
      (scan-for-current-theory (cdr w)))))

(defun scan-for-last-en/disabling
  (rune en/dis w)
  (declare (xargs :mode :program))
  (b* (((when (atom w)) nil) ((unless (and (eq (caar w) 'event-landmark)
           (eq (access-event-tuple-type (cddar w)) 'in-theory))) (scan-for-last-en/disabling rune en/dis (cdr w)))
      (tail (scan-to-event (cdr w)))
      (prev-theory (current-theory1 tail nil nil))
      (prev-enabled (consp (member-equal rune prev-theory)))
      ((when (xor en/dis prev-enabled)) w))
    (scan-for-last-en/disabling rune en/dis tail)))

(defun find-last-en/disabling
  (rune state)
  (declare (xargs :mode :program :stobjs state))
  (b* ((w (w state)) (en/dis (consp (member-equal rune (current-theory1 w nil nil))))
      (ev-wrld (scan-for-last-en/disabling rune en/dis w))
      ((unless ev-wrld) (cw "Never enabled/disabled~%")
        (value :invisible))
      ((er cmd-wrld) (superior-command-world ev-wrld
          w
          'find-last-en/disabling
          state))
      (state (pe-fn1 w (standard-co state) ev-wrld cmd-wrld state)))
    (value :invisible)))