Macro stepper status bar notifications
original commit: f65c8c3427367bbb4c7d6cd561f8334645725d37
This commit is contained in:
parent
7ca1056337
commit
4d752710de
|
@ -203,15 +203,7 @@
|
|||
(get-field one-by-one? config))
|
||||
(menu-option/notify-box extras-menu
|
||||
"Extra navigation"
|
||||
(get-field extra-navigation? config))
|
||||
#|
|
||||
(menu-option/notify-box extras-menu
|
||||
"Suppress warnings"
|
||||
(get-field suppress-warnings? config))
|
||||
(menu-option/notify-box extras-menu
|
||||
"(Debug) Catch internal errors?"
|
||||
(get-field debug-catch-errors? config))
|
||||
|#)
|
||||
(get-field extra-navigation? config)))
|
||||
|
||||
;; fixup-menu : menu -> void
|
||||
;; Delete separators at beginning/end and duplicates in middle
|
||||
|
|
97
collects/macro-debugger/view/gui-util.rkt
Normal file
97
collects/macro-debugger/view/gui-util.rkt
Normal file
|
@ -0,0 +1,97 @@
|
|||
#lang racket/base
|
||||
(require racket/class
|
||||
racket/gui/base)
|
||||
(provide status-area%)
|
||||
|
||||
(define SHOW-DELAY 1000)
|
||||
(define FADE-DELAY 400)
|
||||
(define NAP-TIME 0.1)
|
||||
|
||||
(define status-area%
|
||||
(class* object% (#| status-area<%> |#)
|
||||
(init parent)
|
||||
|
||||
(define lock (make-semaphore 1))
|
||||
|
||||
(define-syntax-rule (with-lock . body)
|
||||
(dynamic-wind (lambda () (semaphore-wait lock))
|
||||
(lambda () . body)
|
||||
(lambda () (semaphore-post lock))))
|
||||
|
||||
(define timer (new timer% (notify-callback (lambda () (update)))))
|
||||
|
||||
(define pane
|
||||
(new horizontal-pane%
|
||||
(parent parent)
|
||||
(stretchable-height #f)))
|
||||
(define message
|
||||
(new message%
|
||||
(parent pane)
|
||||
(label "")
|
||||
(auto-resize #t)
|
||||
(style '(deleted))))
|
||||
|
||||
#|
|
||||
Four states:
|
||||
- 'none = no message displayed, none pending
|
||||
- 'pending = no message displayed, message pending
|
||||
- 'shown = message displayed
|
||||
- 'fade = message displayed, waiting to erase
|
||||
|#
|
||||
(define state 'none)
|
||||
(define pending #f)
|
||||
|
||||
(define/public (set-status msg [immediate? #f])
|
||||
(with-lock
|
||||
(when immediate? (send timer stop))
|
||||
(cond [msg
|
||||
(case state
|
||||
((none)
|
||||
(cond [#f ;; immediate?
|
||||
(set! state 'shown)
|
||||
(send pane change-children (lambda _ (list message)))
|
||||
(send message set-label msg)
|
||||
(set! pending #f)
|
||||
(sleep/yield NAP-TIME)]
|
||||
[else
|
||||
(set! state 'pending)
|
||||
(set! pending msg)
|
||||
(unless immediate? (send timer start SHOW-DELAY #t))]))
|
||||
((pending)
|
||||
(set! pending msg))
|
||||
((shown)
|
||||
(send message set-label msg))
|
||||
((fade)
|
||||
(send timer stop) ;; but (update) may already be waiting
|
||||
(set! state 'shown)
|
||||
(send message set-label msg)))]
|
||||
[(not msg)
|
||||
(case state
|
||||
((none) (void))
|
||||
((pending)
|
||||
(send timer stop) ;; but (update) may already be waiting
|
||||
(set! state 'none)
|
||||
(set! pending #f))
|
||||
((shown)
|
||||
(set! state 'fade)
|
||||
(unless immediate? (send timer start FADE-DELAY #t))))])
|
||||
(when immediate? (update*) (sleep/yield NAP-TIME))))
|
||||
|
||||
(define/private (update)
|
||||
(with-lock (update*)))
|
||||
|
||||
(define/private (update*)
|
||||
(case state
|
||||
((pending)
|
||||
(set! state 'shown)
|
||||
(send pane change-children (lambda _ (list message)))
|
||||
(send message set-label pending)
|
||||
(set! pending #f))
|
||||
((fade)
|
||||
(set! state 'none)
|
||||
(send pane change-children (lambda _ null)))
|
||||
((none shown)
|
||||
;; timer not stopped in time; do nothing
|
||||
(void))))
|
||||
|
||||
(super-new)))
|
|
@ -14,6 +14,7 @@
|
|||
"../model/deriv.rkt"
|
||||
"../model/deriv-util.rkt"
|
||||
"cursor.rkt"
|
||||
"gui-util.rkt"
|
||||
unstable/gui/notify
|
||||
(only-in mzscheme [#%top-interaction mz-top-interaction]))
|
||||
(provide macro-stepper-widget%
|
||||
|
@ -28,6 +29,13 @@
|
|||
(init-field config)
|
||||
(init-field/i (director director<%>))
|
||||
|
||||
(define frame (send parent get-top-level-window))
|
||||
(define eventspace (send frame get-eventspace))
|
||||
|
||||
(define-syntax-rule (with-eventspace . body)
|
||||
(parameterize ((current-eventspace eventspace))
|
||||
(queue-callback (lambda () . body))))
|
||||
|
||||
;; Terms
|
||||
|
||||
;; all-terms : (list-of TermRecord)
|
||||
|
@ -56,16 +64,17 @@
|
|||
(add trec)))
|
||||
|
||||
;; add : TermRecord -> void
|
||||
(define/public (add trec)
|
||||
(set! all-terms (cons trec all-terms))
|
||||
(let ([display-new-term? (cursor:at-end? terms)]
|
||||
[invisible? (send/i trec term-record<%> get-deriv-hidden?)])
|
||||
(unless invisible?
|
||||
(cursor:add-to-end! terms (list trec))
|
||||
(trim-navigator)
|
||||
(if display-new-term?
|
||||
(refresh)
|
||||
(update)))))
|
||||
(define/private (add trec)
|
||||
(with-eventspace
|
||||
(set! all-terms (cons trec all-terms))
|
||||
(let ([display-new-term? (cursor:at-end? terms)]
|
||||
[invisible? (send/i trec term-record<%> get-deriv-hidden?)])
|
||||
(unless invisible?
|
||||
(cursor:add-to-end! terms (list trec))
|
||||
(trim-navigator)
|
||||
(if display-new-term?
|
||||
(refresh)
|
||||
(update))))))
|
||||
|
||||
;; remove-current-term : -> void
|
||||
(define/public (remove-current-term)
|
||||
|
@ -98,7 +107,8 @@
|
|||
(send/i sbc sb:controller<%> reset-primary-partition)
|
||||
(update/preserve-view))
|
||||
|
||||
(define area (new vertical-panel% (parent parent)))
|
||||
(define superarea (new vertical-pane% (parent parent)))
|
||||
(define area (new vertical-panel% (parent superarea)))
|
||||
(define supernavigator
|
||||
(new horizontal-panel%
|
||||
(parent area)
|
||||
|
@ -130,12 +140,16 @@
|
|||
(send/i sbview sb:syntax-browser<%> get-controller))
|
||||
(define control-pane
|
||||
(new vertical-panel% (parent area) (stretchable-height #f)))
|
||||
|
||||
(define/i macro-hiding-prefs hiding-prefs<%>
|
||||
(new macro-hiding-prefs-widget%
|
||||
(parent control-pane)
|
||||
(stepper this)
|
||||
(config config)))
|
||||
|
||||
(define status-area
|
||||
(new status-area% (parent superarea)))
|
||||
|
||||
(send/i sbc sb:controller<%>
|
||||
listen-selected-syntax
|
||||
(lambda (stx) (send/i macro-hiding-prefs hiding-prefs<%> set-syntax stx)))
|
||||
|
@ -238,28 +252,25 @@
|
|||
(list navigator extra-navigator)
|
||||
(list navigator)))))
|
||||
|
||||
(define/public (change-status msg [immediate? #f])
|
||||
(send status-area set-status msg immediate?))
|
||||
|
||||
;; Navigation
|
||||
#|
|
||||
(define/public-final (at-start?)
|
||||
(send/i (focused-term) term-record<%> at-start?))
|
||||
(define/public-final (at-end?)
|
||||
(send/i (focused-term) term-record<%> at-end?))
|
||||
|#
|
||||
(define/public-final (navigate-to-start)
|
||||
(send/i (focused-term) term-record<%> navigate-to-start)
|
||||
(update/save-position))
|
||||
(update/preserve-lines-view))
|
||||
(define/public-final (navigate-to-end)
|
||||
(send/i (focused-term) term-record<%> navigate-to-end)
|
||||
(update/save-position))
|
||||
(update/preserve-lines-view))
|
||||
(define/public-final (navigate-previous)
|
||||
(send/i (focused-term) term-record<%> navigate-previous)
|
||||
(update/save-position))
|
||||
(update/preserve-lines-view))
|
||||
(define/public-final (navigate-next)
|
||||
(send/i (focused-term) term-record<%> navigate-next)
|
||||
(update/save-position))
|
||||
(update/preserve-lines-view))
|
||||
(define/public-final (navigate-to n)
|
||||
(send/i (focused-term) term-record<%> navigate-to n)
|
||||
(update/save-position))
|
||||
(update/preserve-lines-view))
|
||||
|
||||
(define/public-final (navigate-up)
|
||||
(when (focused-term)
|
||||
|
@ -272,48 +283,99 @@
|
|||
(cursor:move-next terms)
|
||||
(refresh/move))
|
||||
|
||||
;; Update
|
||||
;; enable/disable-buttons : -> void
|
||||
(define/private (enable/disable-buttons [? #t])
|
||||
(define term (and ? (focused-term)))
|
||||
;; (message-box "alert" (format "enable/disable: ~s" ?))
|
||||
(send area enable ?)
|
||||
(send (send frame get-menu-bar) enable ?)
|
||||
(send nav:start enable (and ? term (send/i term term-record<%> has-prev?)))
|
||||
(send nav:previous enable (and ? term (send/i term term-record<%> has-prev?)))
|
||||
(send nav:next enable (and ? term (send/i term term-record<%> has-next?)))
|
||||
(send nav:end enable (and ? term (send/i term term-record<%> has-next?)))
|
||||
(send nav:text enable (and ? term #t))
|
||||
(send nav:up enable (and ? (cursor:has-prev? terms)))
|
||||
(send nav:down enable (and ? (cursor:has-next? terms))))
|
||||
|
||||
;; update/save-position : -> void
|
||||
(define/private (update/save-position)
|
||||
(update/preserve-lines-view))
|
||||
;; Async update & refresh
|
||||
|
||||
(define-syntax-rule (with-update-thread . body)
|
||||
(begin (enable/disable-buttons #f)
|
||||
(thread (lambda ()
|
||||
(let () . body)
|
||||
(enable/disable-buttons #t)))))
|
||||
|
||||
;; Update
|
||||
|
||||
;; update/preserve-lines-view : -> void
|
||||
(define/public (update/preserve-lines-view)
|
||||
(define text (send/i sbview sb:syntax-browser<%> get-text))
|
||||
(define start-box (box 0))
|
||||
(define end-box (box 0))
|
||||
(send text get-visible-line-range start-box end-box)
|
||||
(update)
|
||||
(send text scroll-to-position
|
||||
(send text line-start-position (unbox start-box))
|
||||
#f
|
||||
(send text line-start-position (unbox end-box))
|
||||
'start))
|
||||
(with-update-thread
|
||||
(define text (send/i sbview sb:syntax-browser<%> get-text))
|
||||
(define start-box (box 0))
|
||||
(define end-box (box 0))
|
||||
(send text get-visible-line-range start-box end-box)
|
||||
(update*)
|
||||
(send text scroll-to-position
|
||||
(send text line-start-position (unbox start-box))
|
||||
#f
|
||||
(send text line-start-position (unbox end-box))
|
||||
'start)))
|
||||
|
||||
;; update/preserve-view : -> void
|
||||
(define/public (update/preserve-view)
|
||||
(define text (send/i sbview sb:syntax-browser<%> get-text))
|
||||
(define start-box (box 0))
|
||||
(define end-box (box 0))
|
||||
(send text get-visible-position-range start-box end-box)
|
||||
(update)
|
||||
(send text scroll-to-position (unbox start-box) #f (unbox end-box) 'start))
|
||||
(with-update-thread
|
||||
(define text (send/i sbview sb:syntax-browser<%> get-text))
|
||||
(define start-box (box 0))
|
||||
(define end-box (box 0))
|
||||
(send text get-visible-position-range start-box end-box)
|
||||
(update*)
|
||||
(send text scroll-to-position (unbox start-box) #f (unbox end-box) 'start)))
|
||||
|
||||
;; update : -> void
|
||||
;; Updates the terms in the syntax browser to the current step
|
||||
(define/private (update)
|
||||
(with-update-thread
|
||||
(update*)))
|
||||
|
||||
(define/private (update*)
|
||||
;; update:show-prefix : -> void
|
||||
(define (update:show-prefix)
|
||||
;; Show the final terms from the cached synth'd derivs
|
||||
(for ([trec (in-list (cursor:prefix->list terms))])
|
||||
(send/i trec term-record<%> display-final-term)))
|
||||
;; update:show-current-step : -> void
|
||||
(define (update:show-current-step)
|
||||
(when (focused-term)
|
||||
(send/i (focused-term) term-record<%> display-step)))
|
||||
;; update:show-suffix : -> void
|
||||
(define (update:show-suffix)
|
||||
(let ([suffix0 (cursor:suffix->list terms)])
|
||||
(when (pair? suffix0)
|
||||
(for ([trec (in-list (cdr suffix0))])
|
||||
(send/i trec term-record<%> display-initial-term)))))
|
||||
;; update-nav-index : -> void
|
||||
(define (update-nav-index)
|
||||
(define term (focused-term))
|
||||
(set-current-step-index
|
||||
(and term (send/i term term-record<%> get-step-index))))
|
||||
|
||||
(define text (send/i sbview sb:syntax-browser<%> get-text))
|
||||
(define position-of-interest 0)
|
||||
(define multiple-terms? (> (length (cursor->list terms)) 1))
|
||||
(send text begin-edit-sequence #f)
|
||||
(send/i sbview sb:syntax-browser<%> erase-all)
|
||||
|
||||
;;(change-status "Showing prefix")
|
||||
;;(sleep 1)
|
||||
(update:show-prefix)
|
||||
(when multiple-terms? (send/i sbview sb:syntax-browser<%> add-separator))
|
||||
(set! position-of-interest (send text last-position))
|
||||
;;(change-status "Showing current step")
|
||||
;;(sleep 1)
|
||||
(update:show-current-step)
|
||||
(when multiple-terms? (send/i sbview sb:syntax-browser<%> add-separator))
|
||||
;;(change-status "Showing suffix")
|
||||
;;(sleep 1)
|
||||
(update:show-suffix)
|
||||
(send text end-edit-sequence)
|
||||
(send text scroll-to-position
|
||||
|
@ -322,58 +384,23 @@
|
|||
(send text last-position)
|
||||
'start)
|
||||
(update-nav-index)
|
||||
(enable/disable-buttons))
|
||||
|
||||
;; update:show-prefix : -> void
|
||||
(define/private (update:show-prefix)
|
||||
;; Show the final terms from the cached synth'd derivs
|
||||
(for-each (lambda (trec) (send/i trec term-record<%> display-final-term))
|
||||
(cursor:prefix->list terms)))
|
||||
|
||||
;; update:show-current-step : -> void
|
||||
(define/private (update:show-current-step)
|
||||
(when (focused-term)
|
||||
(send/i (focused-term) term-record<%> display-step)))
|
||||
|
||||
;; update:show-suffix : -> void
|
||||
(define/private (update:show-suffix)
|
||||
(let ([suffix0 (cursor:suffix->list terms)])
|
||||
(when (pair? suffix0)
|
||||
(for-each (lambda (trec)
|
||||
(send/i trec term-record<%> display-initial-term))
|
||||
(cdr suffix0)))))
|
||||
|
||||
;; update-nav-index : -> void
|
||||
(define/private (update-nav-index)
|
||||
(define term (focused-term))
|
||||
(set-current-step-index
|
||||
(and term (send/i term term-record<%> get-step-index))))
|
||||
|
||||
;; enable/disable-buttons : -> void
|
||||
(define/private (enable/disable-buttons)
|
||||
(define term (focused-term))
|
||||
(send nav:start enable (and term (send/i term term-record<%> has-prev?)))
|
||||
(send nav:previous enable (and term (send/i term term-record<%> has-prev?)))
|
||||
(send nav:next enable (and term (send/i term term-record<%> has-next?)))
|
||||
(send nav:end enable (and term (send/i term term-record<%> has-next?)))
|
||||
(send nav:text enable (and term #t))
|
||||
(send nav:up enable (cursor:has-prev? terms))
|
||||
(send nav:down enable (cursor:has-next? terms)))
|
||||
(change-status #f)
|
||||
#| (enable/disable-buttons) |#)
|
||||
|
||||
;; --
|
||||
|
||||
;; refresh/resynth : -> void
|
||||
;; Macro hiding policy has changed; invalidate cached parts of trec
|
||||
(define/public (refresh/resynth)
|
||||
(for-each (lambda (trec) (send/i trec term-record<%> invalidate-synth!))
|
||||
(cursor->list terms))
|
||||
(for ([trec (in-list (cursor->list terms))])
|
||||
(send/i trec term-record<%> invalidate-synth!))
|
||||
(refresh))
|
||||
|
||||
;; refresh/re-reduce : -> void
|
||||
;; Reduction config has changed; invalidate cached parts of trec
|
||||
(define/private (refresh/re-reduce)
|
||||
(for-each (lambda (trec) (send/i trec term-record<%> invalidate-steps!))
|
||||
(cursor->list terms))
|
||||
(for ([trec (in-list (cursor->list terms))])
|
||||
(send/i trec term-record<%> invalidate-steps!))
|
||||
(refresh))
|
||||
|
||||
;; refresh/move : -> void
|
||||
|
@ -383,18 +410,17 @@
|
|||
|
||||
;; refresh : -> void
|
||||
(define/public (refresh)
|
||||
(when (focused-term)
|
||||
(send/i (focused-term) term-record<%> on-get-focus))
|
||||
(send nav:step-count set-label "")
|
||||
(let ([term (focused-term)])
|
||||
(when term
|
||||
(let ([step-count (send/i term term-record<%> get-step-count)])
|
||||
(when step-count
|
||||
;; +1 for end of expansion "step"
|
||||
(send nav:step-count set-label (format "of ~s" (add1 step-count)))))))
|
||||
(update))
|
||||
|
||||
(define/private (foci x) (if (list? x) x (list x)))
|
||||
(with-update-thread
|
||||
(when (focused-term)
|
||||
(send/i (focused-term) term-record<%> on-get-focus))
|
||||
(send nav:step-count set-label "")
|
||||
(let ([term (focused-term)])
|
||||
(when term
|
||||
(let ([step-count (send/i term term-record<%> get-step-count)])
|
||||
(when step-count
|
||||
;; +1 for end of expansion "step"
|
||||
(send nav:step-count set-label (format "of ~s" (add1 step-count)))))))
|
||||
(update*)))
|
||||
|
||||
;; Hiding policy
|
||||
|
||||
|
@ -410,7 +436,7 @@
|
|||
(super-new)
|
||||
(show-macro-hiding-panel (send/i config config<%> get-show-hiding-panel?))
|
||||
(show-extra-navigation (send/i config config<%> get-extra-navigation?))
|
||||
(refresh/move)
|
||||
;;(refresh/move)
|
||||
))
|
||||
|
||||
(define (macro-stepper-widget/process-mixin %)
|
||||
|
|
|
@ -55,6 +55,17 @@
|
|||
|
||||
(define steps-position #f)
|
||||
|
||||
(define/private (status msg)
|
||||
(send stepper change-status msg))
|
||||
(define-syntax with-status
|
||||
(syntax-rules ()
|
||||
[(ws msg #:immediate . body)
|
||||
(begin (send stepper change-status msg #t)
|
||||
(begin0 (let () . body)))]
|
||||
[(ws msg . body)
|
||||
(begin (send stepper change-status msg)
|
||||
(begin0 (let () . body)))]))
|
||||
|
||||
(super-new)
|
||||
|
||||
(define-syntax define-guarded-getters
|
||||
|
@ -114,22 +125,24 @@
|
|||
(with-handlers ([(lambda (e) #t)
|
||||
(lambda (e)
|
||||
(set! raw-deriv-oops e))])
|
||||
(set! raw-deriv
|
||||
(parse-derivation
|
||||
(events->token-generator events))))))
|
||||
(with-status "Parsing expansion derivation" #:immediate
|
||||
(set! raw-deriv
|
||||
(parse-derivation
|
||||
(events->token-generator events)))))))
|
||||
|
||||
;; recache-deriv! : -> void
|
||||
(define/private (recache-deriv!)
|
||||
(unless (or deriv deriv-hidden?)
|
||||
(recache-raw-deriv!)
|
||||
(when raw-deriv
|
||||
(let ([process (send/i stepper widget<%> get-preprocess-deriv)])
|
||||
(let ([d (process raw-deriv)])
|
||||
(when (not d)
|
||||
(set! deriv-hidden? #t))
|
||||
(when d
|
||||
(set! deriv d)
|
||||
(set! shift-table (compute-shift-table d))))))))
|
||||
(with-status "Processing expansion derivation" #:immediate
|
||||
(let ([process (send/i stepper widget<%> get-preprocess-deriv)])
|
||||
(let ([d (process raw-deriv)])
|
||||
(when (not d)
|
||||
(set! deriv-hidden? #t))
|
||||
(when d
|
||||
(set! deriv d)
|
||||
(set! shift-table (compute-shift-table d)))))))))
|
||||
|
||||
;; recache-synth! : -> void
|
||||
(define/private (recache-synth!)
|
||||
|
@ -140,38 +153,40 @@
|
|||
(unless (or raw-steps raw-steps-oops)
|
||||
(recache-synth!)
|
||||
(when deriv
|
||||
(let ([show-macro? (or (send/i stepper widget<%> get-show-macro?)
|
||||
(lambda (id) #t))])
|
||||
(with-handlers ([(lambda (e) #t)
|
||||
(lambda (e)
|
||||
(set! raw-steps-oops e))])
|
||||
(let-values ([(raw-steps* binders* definites* estx* error*)
|
||||
(parameterize ((macro-policy show-macro?))
|
||||
(reductions+ deriv))])
|
||||
(set! raw-steps raw-steps*)
|
||||
(set! raw-steps-estx estx*)
|
||||
(set! raw-steps-exn error*)
|
||||
(set! raw-steps-binders binders*)
|
||||
(set! raw-steps-definites definites*)))))))
|
||||
(with-status "Computing reduction steps" #:immediate
|
||||
(let ([show-macro? (or (send/i stepper widget<%> get-show-macro?)
|
||||
(lambda (id) #t))])
|
||||
(with-handlers ([(lambda (e) #t)
|
||||
(lambda (e)
|
||||
(set! raw-steps-oops e))])
|
||||
(let-values ([(raw-steps* binders* definites* estx* error*)
|
||||
(parameterize ((macro-policy show-macro?))
|
||||
(reductions+ deriv))])
|
||||
(set! raw-steps raw-steps*)
|
||||
(set! raw-steps-estx estx*)
|
||||
(set! raw-steps-exn error*)
|
||||
(set! raw-steps-binders binders*)
|
||||
(set! raw-steps-definites definites*))))))))
|
||||
|
||||
;; recache-steps! : -> void
|
||||
(define/private (recache-steps!)
|
||||
(unless (or steps)
|
||||
(recache-raw-steps!)
|
||||
(when raw-steps
|
||||
(set! steps
|
||||
(and raw-steps
|
||||
(let* ([filtered-steps
|
||||
(if (send/i config config<%> get-show-rename-steps?)
|
||||
raw-steps
|
||||
(filter (lambda (x) (not (rename-step? x)))
|
||||
raw-steps))]
|
||||
[processed-steps
|
||||
(if (send/i config config<%> get-one-by-one?)
|
||||
(reduce:one-by-one filtered-steps)
|
||||
filtered-steps)])
|
||||
(cursor:new processed-steps))))
|
||||
(restore-position))))
|
||||
(with-status "Processing reduction steps"
|
||||
(set! steps
|
||||
(and raw-steps
|
||||
(let* ([filtered-steps
|
||||
(if (send/i config config<%> get-show-rename-steps?)
|
||||
raw-steps
|
||||
(filter (lambda (x) (not (rename-step? x)))
|
||||
raw-steps))]
|
||||
[processed-steps
|
||||
(if (send/i config config<%> get-one-by-one?)
|
||||
(reduce:one-by-one filtered-steps)
|
||||
filtered-steps)])
|
||||
(cursor:new processed-steps))))
|
||||
(restore-position)))))
|
||||
|
||||
;; reduce:one-by-one : (list-of step) -> (list-of step)
|
||||
(define/private (reduce:one-by-one rs)
|
||||
|
@ -268,37 +283,40 @@
|
|||
|
||||
;; display-initial-term : -> void
|
||||
(define/public (display-initial-term)
|
||||
(cond [raw-deriv-oops
|
||||
(send/i displayer step-display<%> add-internal-error
|
||||
"derivation" raw-deriv-oops #f events)]
|
||||
[else
|
||||
(send/i displayer step-display<%> add-syntax (wderiv-e1 deriv))]))
|
||||
(with-status "Rendering term"
|
||||
(cond [raw-deriv-oops
|
||||
(send/i displayer step-display<%> add-internal-error
|
||||
"derivation" raw-deriv-oops #f events)]
|
||||
[else
|
||||
(send/i displayer step-display<%> add-syntax (wderiv-e1 deriv))])))
|
||||
|
||||
;; display-final-term : -> void
|
||||
(define/public (display-final-term)
|
||||
(recache-steps!)
|
||||
(cond [(syntax? raw-steps-estx)
|
||||
(send/i displayer step-display<%> add-syntax raw-steps-estx
|
||||
#:binders raw-steps-binders
|
||||
#:shift-table shift-table
|
||||
#:definites raw-steps-definites)]
|
||||
[(exn? raw-steps-exn)
|
||||
(send/i displayer step-display<%> add-error raw-steps-exn)]
|
||||
[else (display-oops #f)]))
|
||||
(with-status "Rendering term"
|
||||
(cond [(syntax? raw-steps-estx)
|
||||
(send/i displayer step-display<%> add-syntax raw-steps-estx
|
||||
#:binders raw-steps-binders
|
||||
#:shift-table shift-table
|
||||
#:definites raw-steps-definites)]
|
||||
[(exn? raw-steps-exn)
|
||||
(send/i displayer step-display<%> add-error raw-steps-exn)]
|
||||
[else (display-oops #f)])))
|
||||
|
||||
;; display-step : -> void
|
||||
(define/public (display-step)
|
||||
(recache-steps!)
|
||||
(cond [steps
|
||||
(let ([step (cursor:next steps)])
|
||||
(if step
|
||||
(send/i displayer step-display<%> add-step step
|
||||
#:shift-table shift-table)
|
||||
(send/i displayer step-display<%> add-final raw-steps-estx raw-steps-exn
|
||||
#:binders raw-steps-binders
|
||||
#:shift-table shift-table
|
||||
#:definites raw-steps-definites)))]
|
||||
[else (display-oops #t)]))
|
||||
(with-status "Rendering step"
|
||||
(cond [steps
|
||||
(let ([step (cursor:next steps)])
|
||||
(if step
|
||||
(send/i displayer step-display<%> add-step step
|
||||
#:shift-table shift-table)
|
||||
(send/i displayer step-display<%> add-final raw-steps-estx raw-steps-exn
|
||||
#:binders raw-steps-binders
|
||||
#:shift-table shift-table
|
||||
#:definites raw-steps-definites)))]
|
||||
[else (display-oops #t)])))
|
||||
|
||||
;; display-oops : boolean -> void
|
||||
(define/private (display-oops show-syntax?)
|
||||
|
|
|
@ -24,22 +24,19 @@
|
|||
(hash-remove! stepper-frames s))
|
||||
|
||||
(define/public (add-obsoleted-warning)
|
||||
(hash-for-each stepper-frames
|
||||
(lambda (stepper-frame flags)
|
||||
(unless (memq 'no-obsolete flags)
|
||||
(send/i stepper-frame stepper-frame<%> add-obsoleted-warning)))))
|
||||
(for ([(stepper-frame flags) (in-hash stepper-frames)])
|
||||
(unless (memq 'no-obsolete flags)
|
||||
(send/i stepper-frame stepper-frame<%> add-obsoleted-warning))))
|
||||
(define/public (add-trace events)
|
||||
(hash-for-each stepper-frames
|
||||
(lambda (stepper-frame flags)
|
||||
(unless (memq 'no-new-traces flags)
|
||||
(send/i (send/i stepper-frame stepper-frame<%> get-widget) widget<%>
|
||||
add-trace events)))))
|
||||
(for ([(stepper-frame flags) (in-hash stepper-frames)])
|
||||
(unless (memq 'no-new-traces flags)
|
||||
(send/i (send/i stepper-frame stepper-frame<%> get-widget) widget<%>
|
||||
add-trace events))))
|
||||
(define/public (add-deriv deriv)
|
||||
(hash-for-each stepper-frames
|
||||
(lambda (stepper-frame flags)
|
||||
(unless (memq 'no-new-traces flags)
|
||||
(send/i (send/i stepper-frame stepper-frame<%> get-widget) widget<%>
|
||||
add-deriv deriv)))))
|
||||
(for ([(stepper-frame flags) (in-hash stepper-frames)])
|
||||
(unless (memq 'no-new-traces flags)
|
||||
(send/i (send/i stepper-frame stepper-frame<%> get-widget) widget<%>
|
||||
add-deriv deriv))))
|
||||
|
||||
(define/public (new-stepper [flags '()])
|
||||
(define stepper-frame (new-stepper-frame))
|
||||
|
|
Loading…
Reference in New Issue
Block a user