#|
A mixin for the DrS definitions text.  Implements highlighting of admitted
and rejected forms.

NOTE:
There are workarounds in this module regarding PR 7838:
 get-forward-sexp and get-backward-sexp in scheme:text% treat ' ` , and ,@
 as s-expressions

The code ought to work even when the PR is addressed, but check
back here when it is.
|#
(module dracula-defns-text-mixin (lib "a-unit.ss")
  (require (lib "class.ss")
           (lib "mred.ss" "mred")
           (lib "framework.ss" "framework")
           (lib "tool.ss" "drscheme")
           (lib "unit.ss")
           (prefix acl2: "../language/acl2-reader.scm")
           (lib "list.ss"))

  (require "../language/event-form.scm")

  (require "dracula-defns-text-mixin-sig.scm")

  (import drscheme:tool^)
  (export dracula-defns-text-mixin^)

  (define color:admit (make-object color% "PaleGreen"))
  (define color:reject (make-object color% "MistyRose"))
  (define highlight-bitmap (make-object bitmap% 10 10 #t))

  ;; An Admit is (make-admit Integer Integer Boolean (-> Void))
  ;; representing the start and end position, event/nonevent status,
  ;; and unhighlighting thunk, of an sexpression highlighted after being sent
  ;; to ACL2.
  (define-struct admit (start end event? unhighlight))

  (define dracula-defns-text-mixin
    (mixin (editor:basic<%>
            text:basic<%>
            scheme:text<%>
            (class->interface text%)
            drscheme:unit:definitions-text<%>) (drscheme:unit:definitions-text<%>)
      (inherit get-top-level-window
               get-next-settings
               get-forward-sexp
               get-backward-sexp
               get-text
               get-tab
               highlight-range)

      ;; (Listof Admit)
      ;; Represents the sucessfully admitted sexpressions, last to first.
      (field [admit-stack null])

      ;; (Or Admit #f)
      ;; Represents the latest failed admit attempt, if any.
      (field [admit-error #f])

      ;; -> (listof s-exp)
      ;; Produce a list of all s-expressions in this file
      (define/public (get-s-expressions)
        (let ([text-port (open-input-string (get-text 0 'eof #t))])
          (let loop ([expr (acl2:read text-port)]
                     [answer '()])
            (if (eof-object? expr)
                (reverse answer)
                (loop (acl2:read text-port) (cons expr answer))))))

      ;; -> Integer
      ;; Produce the end of the currently admitted area.
      (define/private (find-admit-frontier)
        (if (pair? admit-stack)
            (admit-end (car admit-stack))
            0))

      ;; -> (Or (values Integer Integer) (values #f #f))
      ;; Produce the start and end position of the next unadmitted sexpression,
      ;; or false if none.
      ;; PR 7838 reports a bug wherein ' ` , ,@ are treated as separate sexps.
      ;; This no longer seems to be the case; this code assumes correct
      ;; get-forward-sexp and get-backward-sexp behavior.
      (define/private (find-next-unadmitted-sexp)
        (let* ([frontier (find-admit-frontier)]
               [end-of-next (get-forward-sexp frontier)]
               [start-of-next (if end-of-next (get-backward-sexp end-of-next) #f)])
          (if (and end-of-next
                   start-of-next
                   (<= frontier start-of-next)
                   (< start-of-next end-of-next))
              (values start-of-next end-of-next)
              (values #f #f))))

      ;; -> (Or (values Integer Integer String) (values #f #f #f))
      ;; Produce the start position, end position, and text of the next
      ;; unadmitted sexpression, or false if none.
      (define/private (find-next-unadmitted-sexp/text)
        (let*-values ([(start end) (find-next-unadmitted-sexp)])
          (values start
                  end
                  (if (and start end) (get-text start end #t #f) #f))))

      ;; -> (Or String #f)
      ;; Produce the text of the next unadmitted sexpression, if any.
      (define/public (get-next-unadmitted-sexp)
        (let*-values ([(start end text) (find-next-unadmitted-sexp/text)])
          text))

      ;; Boolean -> Void
      ;; Color depends on admitted?
      (define/public (highlight-next-unadmitted-sexp admitted?)
        (unhighlight-error)
        (let*-values ([(start end text) (find-next-unadmitted-sexp/text)])
          (when (and start end text)
            (let* ([event? (event-form? (read (open-input-string text)))]
                   [color (if admitted? color:admit color:reject)]
                   [unhighlight (highlight-range start end color #f 'high)]
                   [admission (make-admit start end event? unhighlight)])
              (if admitted?
                  (set! admit-stack (cons admission admit-stack))
                  (set! admit-error admission))))))

      ;; -> Boolean
      ;; Unhighlight the last admitted form, if any.
      ;; Produce #t when an event form is unhighlighted.
      ;; Produce #f when a nonevent form is unhighligted,
      ;; or nothing is unhighligted.
      (define/public (unhighlight-last-admitted)
        (if (pair? admit-stack)
            (let* ([admission (car admit-stack)]
                   [rest (cdr admit-stack)]
                   [unhighlight (admit-unhighlight admission)]
                   [event? (admit-event? admission)])
              (set! admit-stack rest)
              (unhighlight)
              event?)
            #f))

      ;; -> Void
      (define/public (unhighlight-all)
        (unhighlight-error)
        (for-each (lambda (admission)
                    (apply (admit-unhighlight admission) null))
                  admit-stack)
        (set! admit-stack null))

      ;; -> Void
      (define/private (unhighlight-error)
        (when admit-error
          (apply (admit-unhighlight admit-error) null)
          (set! admit-error #f)))

      ;; Prevent editing green highlighted text
      (define/augment (can-insert? start len)
        (and (>= start (find-admit-frontier))
             (inner #t can-insert? start len)))
      (define/augment (can-delete? start len)
        (and (>= start (find-admit-frontier))
             (inner #t can-delete? start len)))

      ;; Unhighlight red error text when it's edited
      (define/augment (after-insert start len)
        (unhighlight-error)
        (inner (void) after-insert start len))
      (define/augment (after-delete start len)
        (unhighlight-error)
        (inner (void) after-insert start len))

      (define/augment (after-set-next-settings language-settings)
        (send (get-tab) new-settings-set)
        (inner (void) after-set-next-settings language-settings))
      (super-new)))
  )