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-controller^
  (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/public (start-acl2)
        (with-handlers ([exn:fail:user? (lambda (e) (show-start-failure-message
                                                     (exn-message e)))]
                        [exn:not-saved? (lambda (_) (show-save-first-message))])
          (let ([path (find-acl2)]
                [dir (or (get-directory) 
                         (raise (make-exn:not-saved 
                                 "Save your work before starting ACL2"
            (when path
              (parameterize ([current-directory dir])
                (send acl2-controller start-acl2 path)
                (set! active-acl2-session? #t)
                (send (get-frame) show-proof-buttons))))))
      ;; 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)
                 (send acl2-controller certify-book 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) (shutdown-acl2))
      (define/public (new-settings-set)
        (unless active-acl2-session?
          (send (get-frame) hide-proof-buttons (dracula-language-selected?))))