#|
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 "a-unit.ss")
  (require (lib "class.ss")
           (lib "mred.ss" "mred")
           (lib "framework.ss" "framework")
           (lib "tool.ss" "drscheme")
           (lib "unit.ss")
           "acl2-controller.scm")
  
  (require "dracula-tab-mixin-sig.scm"
           
           ;"acl2-settings-sig.scm"
           "../language/acl2-settings.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^
          drscheme:tool^)
  (export dracula-tab-mixin^)
  
  (define dracula:unit:tab<%> 
    (interface (drscheme:unit:tab<%>)
      admit-before-run
      admit-next admit-all undo-last undo-all
      start-acl2 interrupt-acl2 shutdown-acl2
      new-settings-set
      activate))
  
  ;; 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
               get-directory)
      
      ;; 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)
                      x))]))
      
      (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"
                     msg
                     (get-frame)
                     '(ok stop)))
      
      (define/private (show-save-first-message)
        (message-box "Save before starting ACL2"
                     "Please save your code before starting ACL2"
                     (get-frame)
                     '(ok stop)))

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

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

      (define/private (show-certify-failure-message file)
        (message-box "Certification Failure"
                     (format
                      "File ~s could not be certified as an ACL2 book."
                      file)))
      
      (define/public (start-acl2)
        ;; Hide the "Start" button
        (send (get-frame) hide-proof-buttons #f)
        (unless
            (with-handlers ([exn?
                             (lambda (e)
                               (if (exn:not-saved? e)
                                   (show-save-first-message)
                                   (show-start-failure-message (exn-message e)))
                               #f)])
              (let ([path (find-acl2)]
                    [dir (or (get-directory) 
                             (raise (make-exn:not-saved 
                                     "Save your work before starting ACL2"
                                     (current-continuation-marks))))])
                (and path
                     (parameterize ([current-directory dir])
                       (send acl2-controller start-acl2 path)
                       (set! active-acl2-session? #t)
                       (send (get-frame) show-proof-buttons)
                       #t))))
          ;; 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)
              (with-disabled-buttons
               (send acl2-controller admit-definitions-window 
                     (get-defs) (get-frame)))
              #t)))
      
      (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) 
        (with-disabled-buttons 
         (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)
        (with-disabled-buttons
         (if (send (get-frame) save)
             (cond
              [(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)])
             (show-save-first-message))))
      
      (define/public (interrupt-acl2) 
        (with-disabled-buttons
         (send acl2-controller interrupt-acl2)))
      
      (define/public (shutdown-acl2)
        (with-disabled-buttons
         (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)
        (inner (void) on-close))

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