#|
When the language preferences indicate that we should try to admit definitions
when 'Run' is clicked, a dialog with a progress gauge appears.  That dialog
is defined here.
|#
(module admit-dialog mzscheme
  (require (lib "class.ss")
           (lib "mred.ss" "mred")
           (lib "port.ss")
           
           (file "acl2-process.scm"))
  (provide admit-dialog%)
  
  (require (file "eprintf.scm"))
  
  (define *dialog-message* "Checking Definitions in ACL2...")
  
  ;; FIX:  Ought to have a cancel button... it can't interrupt ACL2, but
  ;;       at least we can prevent rest of the forms from going through.
  (define admit-dialog%
    (class* dialog% ()
      (inherit show)
      (super-new [label "Admitting Definitions Window"]
                 [width 400] #;[height 75])
      
      (init-field expressions)
      
      (field [gauge (new gauge%
                         [label *dialog-message*]
                         [parent this] 
                         [range (length expressions)])])
      
      (field [admitted? (void)])
      
      (define/private (increment-gauge!)
        (send gauge set-value (add1 (send gauge get-value))))
      
      ;; Mutates `admitted?' to reflect success (#t or #f)
      (define/private (admit-expressions!)
        (let ([acl2 (new acl2-process%
                         [acl2-output-port (open-output-nowhere)]
                         [send-new-prooftree void])])
          (send acl2 start!)
          (set! admitted?
                (andmap (lambda (s)
                          (let ([? (send acl2 s-exp->repl s)])
                            (increment-gauge!)
                            ?)) 
                        expressions))
          (send acl2 stop!)
          ;; Sends control back to after (show #t) below
          (show #f)))
      
      ;; -> Boolean
      (define/public (admit!)
        (queue-callback (lambda () (admit-expressions!)))
        (show #t)
        ;; Control resumes here upon (show #f)
        admitted?)))
  
  )