(module proof-interfaces mzscheme

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

  (provide proof-interfaces@)

  ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
  ;;
  ;;  INTERFACES
  ;;
  ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

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

    ;; proof-language<%> : Interface<Language>
    ;; This interface marks languages for the prover interface.
    (define proof-language<%>
      (interface (drscheme:language:language<%>)))

    ;; proof-frame<%> : Interface<Frame>
    ;; This interface represents the prover-enabled DrScheme unit frame.
    (define proof-frame<%>
      (interface (drscheme:unit:frame<%>)

        ;; Boolean -> Void
        ;; Enable or disable proof buttons
        proof-enable-start
        proof-enable-stop

        ;; Boolean -> Void
        ;; Hide or show the entire proof control panel
        proof-show

        ))

    ;; proof-text<%> : Interface<Text>
    ;; Prover-aware definitions text.
    (define proof-text<%>
      (interface (drscheme:unit:definitions-text<%>)

        ;; -> Boolean
        ;; Report whether the current language supports proofs.
        proof-text?

        ;; Boolean -> Void
        ;; Enable or disable proof editing.
        proof-enable-edit

        ;; Syntax Color -> Void
        ;; Highlights the source text for the given syntax object.
        highlight-syntax

        ;; Syntax -> Void
        ;; Unhighlights the source text for the given syntax object.
        unhighlight-syntax

        ;; -> Void
        ;; Unhighlights the source text for previously given syntax objects.
        unhighlight-all-syntax

        ))

    ;; proof-tab<%> : Interface<Tab>
    ;; This interface represents prover-aware DrScheme tabs.
    (define proof-tab<%>
      (interface (drscheme:unit:tab<%>)

        ;; -> Void
        ;; Updates the GUI, e.g. when switching languages or tabs.
        proof-update

        ;; -> Void
        ;; Reacts to the corresponding user button.
        proof-start
        proof-stop

        ;; Syntax -> Void
        ;; Reacts to proof state of individual terms.
        proof-term-attempt
        proof-term-success
        proof-term-failure
        proof-term-clear
        proof-term-clear-all

        ;; Boolean -> Void
        ;; Reacts to changes in the prover's state.
        proof-active

        ))

    ;; proof-controller<%> : Interface<Controller>
    ;; This interface represents an interactive proof.
    (define proof-controller<%>
      (interface ()

        ;; (Channel/EOF ProofCommand) -> Void
        ;; Starts a proof attempt.
        start

        ;; -> Void
        ;; Stops a proof attempt.
        stop

        )))

  )