(module proof-tab mzscheme

  (require (lib "unit.ss")
           (lib "class.ss")
           (lib "mred.ss" "mred")
           (lib "tool.ss" "drscheme")
           (lib "pretty.ss")
           (lib "async-channel.ss")
           (lib "framework.ss" "framework")
           "../../language/find-acl2.scm"
           "../../gui/acl2-controller.scm"
           "sexp-window.scm"
           "../expansion/proof-syntax.scm"
           "../expansion/proof-commands.scm"
           "proof-signatures.scm")

  (provide proof-tab@)

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

    (define attempt-color (make-object color% "DeepSkyBlue"))
    (define failure-color (make-object color% "Crimson"))
    (define success-color (make-object color% "LimeGreen"))

    ;; proof-tab-mixin : Class<Tab> -> Class<ProofTab>
    ;; Extends DrScheme tabs for the prover.
    (define proof-tab-mixin
      (mixin (drscheme:unit:tab<%>) (proof-tab<%>)

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

        (inherit get-defs get-frame)

        ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
        ;;
        ;;  PROOF MANIPULATION
        ;;
        ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

        ;; One of: 'done, 'active, 'unknown
        (define the-state 'unknown)

        (define the-controller (new proof-controller% [observer this]))

        (define/private (make-proof-channel)
          (define channel (make-channel))
          (define defs (get-defs))
          (define (put v) (yield (channel-put-evt channel v)))
          (thread
           (lambda ()
             (drscheme:eval:expand-program
              (drscheme:language:make-text/pos
               defs 0 (send defs last-position))
              (send defs get-next-settings)
              #t ;; compile-time evals
              void ;; init
              void ;; kill
              (lambda (term recur)
                (if (eof-object? term)
                    (put term)
                    (for-each put (extract-commands term)))
                (recur)))))
          channel)

        ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
        ;;
        ;;  EVENT HANDLING
        ;;
        ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

        (define/private (set-state v)
          (set! the-state v)
          (proof-update))

        (define/public (proof-update)
          (define the-frame (get-frame))
          (case the-state
            [(done)
             (begin (send the-frame proof-enable-start #t)
                    (send the-frame proof-enable-stop #f)
                    (send (get-defs) proof-enable-edit #t))]
            [(active)
             (begin (send the-frame proof-enable-start #f)
                    (send the-frame proof-enable-stop #t)
                    (send (get-defs) proof-enable-edit #f))]
            [(unknown)
             (begin (send the-frame proof-enable-start #f)
                    (send the-frame proof-enable-stop #f)
                    (send (get-defs) proof-enable-edit #t))])
          (send the-frame proof-show (send (get-defs) proof-text?)))

        (define/public (proof-start)
          (set-state 'unknown)
          (send the-controller start (make-proof-channel)))

        (define/public (proof-stop)
          (set-state 'unknown)
          (send the-controller stop))

        (define/public (proof-active active?)
          (set-state (if active? 'active 'done)))

        (define/public (proof-term-attempt stx)
          (send (get-defs) highlight-syntax stx attempt-color))

        (define/public (proof-term-success stx)
          (send (get-defs) highlight-syntax stx success-color))

        (define/public (proof-term-failure stx)
          (send (get-defs) highlight-syntax stx failure-color))

        (define/public (proof-term-clear stx)
          (send (get-defs) unhighlight-syntax stx))

        (define/public (proof-term-clear-all)
          (send (get-defs) unhighlight-all-syntax))

        ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
        ;;
        ;;  CLASS INITIALIZATION
        ;;
        ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

        (super-new)

        ))

    )

  )