(module proof-language mzscheme

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

  (provide proof-language@)

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

    ;; proof-language? : Language -> Boolean
    ;; Reports whether the prover applies to this language.
    (define (proof-language? lang)
      (is-a? lang proof-language<%>))

    ;; proof-language-mixin : Class<Language> -> Class<ProofLanguage>
    ;; This mixin applies the proof-language<%> interface.
    (define proof-language-mixin
      (mixin (drscheme:language:language<%>) (proof-language<%>)
        (super-new))))

  )