(module proof-text mzscheme

  (require (lib "unit.ss")
           (lib "class.ss")
           (lib "mred.ss" "mred")
           (lib "tool.ss" "drscheme")
           (lib "framework.ss" "framework")
           "proof-signatures.scm")

  (provide proof-text@)

  (define-unit proof-text@
    (import drscheme:tool^ proof-language^ proof-interfaces^)
    (export proof-text^)

    (define settings->language
      drscheme:language-configuration:language-settings-language)

    (define proof-text-mixin
      (mixin
          (drscheme:unit:definitions-text<%> text:file<%> text:basic<%>)
          (proof-text<%>)

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

        (inherit get-tab get-next-settings highlight-range)

        ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
        ;;
        ;;  NEW METHODS
        ;;
        ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

        (define highlight-table (make-hash-table 'weak))

        (define/public (highlight-syntax stx color)
          (let* ([src (syntax-source stx)]
                 [pos (syntax-position stx)]
                 [len (syntax-span stx)])
            (when (and (eq? src this) pos len)
              (unhighlight-syntax stx)
              (let* ([start (- pos 1)]
                     [end (+ start len)]
                     [unhighlighter
                      (highlight-range start end color)])
                (hash-table-put! highlight-table stx unhighlighter)))))

        (define/public (unhighlight-syntax stx)
          (let* ([thunk (hash-table-get highlight-table stx #f)])
            (when thunk
              (hash-table-remove! highlight-table stx)
              (thunk))))

        (define/public (unhighlight-all-syntax)
          (hash-table-for-each
           highlight-table
           (lambda (k v)
             (hash-table-remove! highlight-table k)
             (v))))

        (define/public (proof-text?)
          (let* ([settings (get-next-settings)]
                 [language (settings->language settings)]
                 [result (proof-language? language)])
            result))

        ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
        ;;
        ;;  UPDATED METHODS
        ;;
        ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

        (define editable? #t)

        (define/public (proof-enable-edit enable?)
          (set! editable? enable?))

        (define/augment (can-insert? start len)
          (and editable? (inner #t can-insert? start len)))

        (define/augment (can-delete? start len)
          (and editable? (inner #t can-delete? start len)))

        (define/augment (after-set-next-settings settings)
          (inner (void) after-set-next-settings settings)
          (send (get-tab) proof-update))

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

        (super-new)

        ))

    )

  )