(module proof-frame mzscheme

  (require (lib "unit.ss")
           (lib "class.ss")
           (lib "mred.ss" "mred")
           (lib "tool.ss" "drscheme")
           (lib "bitmap-label.ss" "mrlib")
           (lib "etc.ss")
           "proof-signatures.scm"
           (planet "class-utils.ss" ("cce" "class-utils.plt" 1 1)))

  (provide proof-frame@)

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

    ;; proof-frame-mixin : Class<Frame> -> Class<Frame>
    ;; Updates the main DrScheme frame to display the proof interface.
    (define proof-frame-mixin
      (mixin (drscheme:unit:frame<%>) (proof-frame<%>)

        ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
        ;;
        ;;  INHERITED METHODS
        ;;
        ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

        (inherit get-current-tab)

        ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
        ;;
        ;;  PANEL CONSTRUCTION
        ;;
        ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

        ;; drscheme-panel, proof-panel, parent-panel : Panel
        ;; Panels containing the definitions/interactions windows,
        ;; the proof controls, and the other two panels, respectively.
        ;; Initialized during super-new.
        (define parent-panel #f)
        (define proof-panel #f)
        (define drscheme-panel #f)

        ;; get-definitions/interactions-panel-parent : -> VerticalPanel
        ;; Gets called precisely once, during super-new.
        ;; Constructs the panels necessary to insert proof controls.
        (define/override (get-definitions/interactions-panel-parent)

          ;; Get the existing parent panel.
          (define top-panel
            (super get-definitions/interactions-panel-parent))

          ;; Construct an intermediate panel so we know all its children.
          (set! parent-panel (new vertical-panel% [parent top-panel]))

          ;; Construct a panel for proof controls.
          (set! proof-panel
                (new horizontal-panel%
                     [parent parent-panel]
                     [stretchable-height #f]
                     [alignment '(center center)]
                     [style '(border)]))

          ;; Construct a panel for the regular editors.
          (set! drscheme-panel (new vertical-panel% [parent parent-panel]))

          ;; Return the editor panel.
          drscheme-panel)

        ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
        ;;
        ;;  SUPERCLASS CONSTRUCTION
        ;;
        ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

        ;; Triggers construction of the panels.
        (super-new)

        ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
        ;;
        ;;  BUTTON CONSTRUCTION
        ;;
        ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

        (define start-button
          (new button%
               [parent proof-panel]
               [label "Start"]
               [callback (lambda _ (send (get-current-tab) proof-start))]))

        (define stop-button
          (new button%
               [parent proof-panel]
               [label "Stop"]
               [callback (lambda _ (send (get-current-tab) proof-stop))]))

        ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
        ;;
        ;;  GUI UPDATE METHODS
        ;;
        ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

        (define/public (proof-show visible?)
          (send parent-panel
                change-children
                (lambda (cs)
                  (if visible?
                      (list proof-panel drscheme-panel)
                      (list drscheme-panel)))))

        (define/public (proof-enable-start enabled?)
          (when start-button (send start-button enable enabled?)))

        (define/public (proof-enable-stop enabled?)
          (when stop-button (send stop-button enable enabled?)))

        ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
        ;;
        ;;  PROOF TAB EVENT NOTIFICATION
        ;;
        ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

        (define/augment (on-tab-change old-tab new-tab)
          (inner (void) on-tab-change old-tab new-tab)
          (send new-tab proof-update))

        (send (get-current-tab) proof-update)

        ))

    )

  )