(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<%>)
(inherit get-tab
get-next-settings
highlight-range
port-name-matches?)
(define highlight-table (make-hash-table))
(define/public (highlight-syntax stx color)
(let* ([src (syntax-source stx)]
[pos (syntax-position stx)]
[len (syntax-span stx)])
(when (and (port-name-matches? src) 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) (v)))
(hash-table-for-each
highlight-table
(lambda (k v)
(hash-table-remove! highlight-table k))))
(define/public (proof-text?)
(let* ([settings (get-next-settings)]
[language (settings->language settings)]
[result (proof-language? language)])
result))
(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))
(super-new)
))
)
)