The controller that mediates between the ACL2 process and the Dracula GUI
lives here.  Each tab has a controller, and the proof buttons in the frame
just forward messages to (get-current-tab).
(module dracula-tab-mixin (lib "")
  (require (lib "")
           (lib "" "mred")
           (lib "" "framework")
           (lib "" "drscheme")
           (lib "")
  (require "dracula-tab-mixin-sig.scm"
  (require "../language/find-acl2.scm")
  ;(require "eprintf.scm")
  ;; Do not remove this require!
  (require "../language/dracula-language.scm")
  ;; This is here to mark an implicit dependence that the dracula-gui tool
  ;; has on dracula-language.plt.  The method `dracula-language-selected?'
  ;; below sends `dracula-language?' to a DrS language object.  That method
  ;; does not necessarily exist unless the dracula-language.plt has extended
  ;; the DrS language interface. 
  (import ;acl2-settings^
  (export dracula-tab-mixin^)
  (define dracula:unit:tab<%> 
    (interface (drscheme:unit:tab<%>)
      admit-next admit-all undo-last undo-all
      start-acl2 interrupt-acl2 shutdown-acl2
  ;; Language-Settings -> Boolean
  (define (admit-before-run? lang-settings)
    (let ([settings (drscheme:language-configuration:language-settings-settings lang-settings)])
      (and (pair? settings)
           (acl2-settings? (car settings))
           (acl2-settings-admit-before-run? (car settings)))))
  (define-struct (exn:not-saved exn:fail) ())
  (define dracula-tab-mixin
    (mixin (drscheme:unit:tab<%>) (dracula:unit:tab<%>)
      (inherit get-frame get-defs
      ;; wrap around forms to execute them with buttons temporarily disabled.
      ;; (Interrupt & Stop are never disabled)
      (define-syntax (with-disabled-buttons stx)
        (syntax-case stx ()
          [(_ form ...)
           #'(begin (send (get-frame) disable-buttons)
                    (let ([x (begin form ...)])
                      (send (get-frame) enable-buttons)
      (field [acl2-controller (new acl2-controller%)])
      (field [active-acl2-session? #f])
      (define/private (dracula-language-selected?)
        (let* ([settings (send (get-defs) get-next-settings)]
               [language (drscheme:language-configuration:language-settings-language settings)])
          ;; see the big note by the require above regarding this method call:
          (send language dracula-language?)))
      (define/public (activate)
        (if active-acl2-session?
            (send (get-frame) show-proof-buttons)
            (send (get-frame) hide-proof-buttons (dracula-language-selected?))))
      (define/private (show-start-failure-message msg)
        (message-box "Failed to start ACL2"
                     '(ok stop)))
      (define/private (show-save-first-message)
        (message-box "Save before starting ACL2"
                     "Please save your code before starting ACL2"
                     '(ok stop)))

      (define/private (show-book-name-message)
        (message-box "Filename extension for certified books"
                     "ACL2 books must have the .lisp file extension."
                     '(ok stop)))

      (define/private (show-certify-success-message file)
        (message-box "Certification Success"
                      "File ~s has been successfully certified as an ACL2 book."

      (define/private (show-certify-failure-message file)
        (message-box "Certification Failure"
                      "File ~s could not be certified as an ACL2 book."
      (define/public (start-acl2)
        ;; Hide the "Start" button
        (send (get-frame) hide-proof-buttons #f)
            (with-handlers ([exn?
                             (lambda (e)
                               (if (exn:not-saved? e)
                                   (show-start-failure-message (exn-message e)))
              (let ([path (find-acl2)]
                    [dir (or (get-directory) 
                             (raise (make-exn:not-saved 
                                     "Save your work before starting ACL2"
                (and path
                     (parameterize ([current-directory dir])
                       (send acl2-controller start-acl2 path)
                       (set! active-acl2-session? #t)
                       (send (get-frame) show-proof-buttons)
          ;; Restore the "Start" button on failure
          (send (get-frame) hide-proof-buttons #t)))
      ;; Attempt to admit the definitions window if that setting is enabled.
      ;; Produce #t iff either the admission succeeds or the setting is disabled.
      (define/public (admit-before-run)
        (let ([settings (send (get-defs) get-next-settings)])
          (if (admit-before-run? settings)
               (send acl2-controller admit-definitions-window 
                     (get-defs) (get-frame)))
      (define/public (admit-next) 
        (with-disabled-buttons (send acl2-controller admit-next (get-defs))))
      (define/public (admit-all)
        (with-disabled-buttons (send acl2-controller admit-all (get-defs))))
      (define/public (undo-last) 
        (with-disabled-buttons (send acl2-controller undo-last (get-defs))))
      (define/public (undo-all) 
         (send (get-defs) unhighlight-all)
         (send acl2-controller undo-all)))

      (define book-re (regexp "\\.lisp$"))

      (define/private (get-book-name path)
        (let* ([str (path->string path)])
          (and (regexp-match? book-re str)
               (regexp-replace book-re str ""))))

      (define/public (certify-as-book)
         (if (send (get-frame) save)
              [(get-book-name (send (get-frame) get-filename))
               (lambda (filename)
                 (send (get-defs) unhighlight-all)
                 (if (send acl2-controller certify-book filename)
                     (show-certify-success-message filename)
                     (show-certify-failure-message filename)))]
              [else (show-book-name-message)])
      (define/public (interrupt-acl2) 
         (send acl2-controller interrupt-acl2)))
      (define/public (shutdown-acl2)
         (send (get-defs) unhighlight-all)
         (send acl2-controller shutdown-acl2)
         (set! active-acl2-session? #f)
         (send (get-frame) hide-proof-buttons (dracula-language-selected?))))
      (define/augment (on-close)
        (inner (void) on-close))

      (define/public (new-settings-set)
        (unless active-acl2-session?
          (send (get-frame) hide-proof-buttons (dracula-language-selected?))))