#lang scheme/gui

(require drscheme/tool
         framework
         "dracula-interfaces.ss"
         "executable-path.ss")

(provide dracula-drscheme-frame^
         dracula-drscheme-frame@)

(define-signature dracula-drscheme-frame^
  (dracula-drscheme-frame-mixin))

(define-unit dracula-drscheme-frame@
  (import drscheme:tool^ dracula-interfaces^)
  (export dracula-drscheme-frame^)

  (define dracula-drscheme-frame-mixin
    (mixin (drscheme:unit:frame<%>) (dracula-drscheme-frame<%>)
      (inherit get-current-tab)

      ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
      ;;
      ;;  METHODS
      ;;
      ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

      (define/override (get-definitions/interactions-panel-parent)
        (let* ([top (super get-definitions/interactions-panel-parent)]
               [mid (new panel:horizontal-dragable% [parent top])]
               [bot (new vertical-panel% [parent mid])])
          (set! dracula-gui-container mid)
          (queue-callback
           (lambda ()
             (send (get-current-tab) update-dracula-gui))
           #f)
          bot))

      (define/augment (on-tab-change old-tab new-tab)
        (queue-callback
         (lambda ()
           (send new-tab update-dracula-gui))
         #f)
        (inner (void) on-tab-change old-tab new-tab))

      (define/public (get-dracula-gui-container)
        (unless (is-a? dracula-gui-container area-container<%>)
          (error 'Dracula
                 "~a\n~a: expected an area container, got: ~e"
                 "internal error: GUI failed to initialize."
                 'get-dracula-gui-container
                 dracula-gui-container))
        dracula-gui-container)

      (define/public (get-dracula-menu-items)
        (unless (is-a? language-menu labelled-menu-item<%>)
          (error 'Dracula
                 "~a\n~a: expected a labelled menu item, got: ~e"
                 "internal error: GUI failed to initialize."
                 'get-dracula-menu-items
                 language-menu))
        (list acl2-show/hide-menu-item
              acl2-save-menu-item
              acl2-path-menu-item))

      (define/public (dracula-proof-shown shown?)
        (unless (is-a? language-menu labelled-menu-item<%>)
          (error 'Dracula
                 "~a\n~a: expected a labelled menu item, got: ~e"
                 "internal error: GUI failed to initialize."
                 'dracula-proof-shown
                 acl2-show/hide-menu-item))
        (send acl2-show/hide-menu-item set-label
          (if shown? "Hide ACL2 Window" "Show ACL2 Window")))

      ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
      ;;
      ;;  INITIALIZATION
      ;;
      ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

      (define dracula-gui-container #f)

      (super-new)

      ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
      ;;
      ;;  MENU
      ;;
      ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

      (inherit get-language-menu)

      (define language-menu (get-language-menu))

      (new separator-menu-item% [parent language-menu])

      (define acl2-show/hide-menu-item
        (new menu-item%
             [parent language-menu]
             [label "Show/Hide ACL2 Window"]
             [callback (lambda _ (send (get-current-tab) toggle-show-proof))]))

      (define acl2-save-menu-item
        (new menu-item%
             [parent language-menu]
             [label "Save ACL2 Output As..."]
             [callback (lambda _ (send (get-current-tab) save-output))]))

      (define acl2-path-menu-item
        (new menu-item%
             [label "Change ACL2 Executable Path..."]
             [parent language-menu]
             [callback (lambda _ (prompt-and-set-executable-path))]))

      )))