#|
Defines a unit that adds buttons to the DrS frame.
|#
(module dracula-frame-mixin (lib "a-unit.ss")
  (require (lib "class.ss")
           (lib "mred.ss" "mred")
           (lib "tool.ss" "drscheme")
           (lib "unit.ss")
           (lib "list.ss")
           ;(file "../tool-name.scm")
           "uninstall.scm"
           "execute-button-clicked.scm")
  (require "dracula-frame-mixin-sig.scm")

  (require "eprintf.scm")

  (import ;acl2-language^
   drscheme:tool^)
  (export dracula-frame-mixin^)

  ;; A PanelRecord is (make-panel-record Panel Panel)
  ;; representing a panel and its parent, respectively.
  (define-struct panel-record (self parent))

  (define dracula-unit-frame-mixin
    (mixin (drscheme:unit:frame<%>) (drscheme:unit:frame<%>)
      (inherit get-button-panel
               get-definitions-text
               get-interactions-text
               get-menu-bar
               get-current-tab
               get-top-level-window
               get-eventspace)

      ;; (Or PanelRecord #f)
      ;; Records the current proof buttons, if any.
      (field [proof-buttons #f])

      ;; During on-execute in language<%>, allows us to determine whether
      ;; the Run button was physically clicked.
      (define/override (execute-callback)
        (when (send (get-current-tab) admit-before-run)
          (super execute-callback)))

      (define/augment (on-tab-change from to)
        (send to activate)
        (inner (void) on-tab-change from to))

      ;; Adapted the following three defns from MzTake code
      (define/override (get-definitions/interactions-panel-parent)
        (let* ([original (super get-definitions/interactions-panel-parent)]
               [parent (new vertical-panel% [parent original])]
               [buttons (new horizontal-panel%
                             [parent parent]
                             [stretchable-height #f]
                             [alignment '(center center)]
                             [style '(border)])]
               [children (new vertical-panel% [parent parent])])
          (send parent change-children (lambda (l) (list children)))
          (set! proof-buttons (make-panel-record buttons parent))
          children))

      (define/private (button-panel)
        (panel-record-self proof-buttons))

      (define/private (parent-panel)
        (panel-record-parent proof-buttons))

      (define/public (hide-proof-buttons enable-Prove?)
        (when proof-buttons
          (send (parent-panel)
                change-children
                (lambda (l) (remq (button-panel) l)))
          (send Prove-button enable enable-Prove?)))

      (define/public (show-proof-buttons)
        (when proof-buttons
          (send (parent-panel)
                change-children
                (lambda (l) (cons (button-panel) (remq (button-panel) l))))
          (send Prove-button enable #f)))

      (define/public (enable-Prove-button enable?)
        (send Prove-button enable enable?))

      (define/public (disable-buttons)
        (for-each (lambda (b) (send b enable #f)) buttons-w/o-interrupt&stop&Prove))

      (define/public (enable-buttons)
        (for-each (lambda (b) (send b enable #t)) buttons-w/o-interrupt&stop&Prove))

      (super-new)

      ;; Add an Uninstall option to the Dracula menu.
      (inherit get-language-menu
               register-capability-menu-item)
      (let ([super-menu (get-language-menu)])
        (new separator-menu-item% [parent super-menu])
        (register-capability-menu-item
         'drscheme:special:uninstall-acl2-tool super-menu)
        (new menu-item%
             [label (string-append "Uninstall Dracula")]
             [parent super-menu]
             [callback uninstall-callback])
        (register-capability-menu-item
         'drscheme:special:uninstall-acl2-tool super-menu))

      ;; BUTTONS ;;
      (define-syntax (notify-controller stx)
        (syntax-case stx ()
          [(_ msg-name) #'(lambda (b e) (send (get-current-tab) msg-name))]))

      (define Prove-button
        (begin
          (unless proof-buttons
            (error 'dracula-unit-frame-mixin
                   "Prove button initialized before panel"))
          (new button% [label "Start ACL2"]
               [parent (get-button-panel)]
               [callback (notify-controller start-acl2)])))

      (define-syntax (define-control-buttons stx)
        (syntax-case stx ()
          [(_ [name lbl controller-msg] ...)
           #'(begin (define name
                      (begin
                        (unless proof-buttons
                          (error 'dracula-unit-frame-mixin
                                 "~s button initalized before panel"
                                 lbl))
                        (new button% [label lbl]
                             [parent (button-panel)]
                             [callback (notify-controller controller-msg)])))
                    ...)]))

      (define-control-buttons
        [admit-next-button "Admit Next" admit-next]
        [admit-all-button "Admit All" admit-all]
        [undo-last-button "Undo Last" undo-last]
        [reset-acl2-button "Undo All" undo-all]
        [certify-book-button "Save / Certify" certify-as-book]
        [interrupt-proof-button "Interrupt Proof" interrupt-acl2]
        [stop-prover-button "Shutdown ACL2" shutdown-acl2])

      (define buttons (list Prove-button admit-next-button admit-all-button undo-last-button
                            certify-book-button
                            interrupt-proof-button
                            reset-acl2-button stop-prover-button))

      (define buttons-w/o-interrupt&stop&Prove
        (remq Prove-button
              (remq interrupt-proof-button
                    (remq stop-prover-button buttons))))

      ;(enable-Prove-button (is-acl2? (send (get-definitions-text) get-next-settings)))
      ))
  )