#|
Define an editor<%> that can display proof trees.  Given an instance of 
the ACL2 console editor, it also manages focusing on checkpoints.
|#
(module proof-tree-editor mzscheme
  (require (lib "tool.ss" "drscheme")
           (lib "mred.ss" "mred")
           (lib "framework.ss" "framework")
           (lib "class.ss")
           (lib "unit.ss"))
  (require (lib "string.ss" "srfi" "13")
           (lib "list.ss" "srfi" "1")
           (lib "14.ss" "srfi")
           (file "list-zipper.scm")
           (file "checkpoint.scm"))
  
  (provide proof-tree-editor%)
  
  (define non-newline-char-set (char-set-complement (char-set #\newline)))
  
  ;; extract-goal-name : String -> String
  ;; Produce the goal name from a checkpoint line in an ACL2 prooftree.
  ;; Checkpoint lines look like this:
  ;; c  1 |  |  |  Subgoal *1.1.2/2'' ELIM
  ;; c  4 *1.1.2 INDUCT
  (define extract-goal-name
    ;; <character:c> <natural-number> |* <goal-name>  (modulo whitespace).
    (let ([re #rx"c[ ]+[0123456789]+(?:[ ]+\\|)*[ ]+((?:Subgoal)?[ ]*[^ ]*)[ ]+"])
      (lambda (cp-line)
        (cadr (regexp-match re cp-line)))))
  
  (define text:prooftree<%> (interface (text:basic<%>)
                              set-proof-tree
                              ;...
                              ))
  
  ;; Does this want to be a mixin?
  (define proof-tree-editor%
    (class* text:basic% (text:prooftree<%>)
      (init-field console-editor)
      (init-field previous-button)
      (init-field next-button)
      
      (field [checkpoints #f])
      (field [focused? #f])
      
      (inherit begin-edit-sequence
               end-edit-sequence
               erase insert
               change-style)
      
      (define (get-checkpoint-position)
        (if checkpoints 
            (checkpoint-position (send checkpoints get-current-item))
            (send console-editor last-position)))
      
      (define (display-prooftree str)
        (begin-edit-sequence)
        (erase)
        ;; there has to be a way to permanently change the style
        (change-style (make-object style-delta% 'change-family 'modern))
        (insert str)
        (end-edit-sequence))
      
      (define/public (set-proof-tree str)
        (send previous-button enable #f)
        (send next-button enable #f)
        (display-prooftree str)
        (let* ([cp-lines (filter (lambda (s) (eq? (string-ref s 0) #\c))
                                 (string-tokenize str non-newline-char-set))]
               [goal-names (map extract-goal-name cp-lines)])
          (set! focused? #f)
          (set! checkpoints
                (if (null? goal-names)
                    #f
                    (begin (send next-button enable #t)
                           (make-zipper (make-checkpoints goal-names
                                                          console-editor)))))))
      (define (enable/disable-buttons)
        (if checkpoints
            (begin (send next-button enable (send checkpoints has-next?))
                   (send previous-button enable (send checkpoints has-prior?)))
            (begin (send next-button enable #f)
                   (send previous-button enable #f))))
      
      (define/public (focus-console-on-next-checkpoint)
        (when focused? (send checkpoints cursor-forward!))
        (set! focused? #t)
        (enable/disable-buttons)
        (let ([next-cp-position (get-checkpoint-position)])
          (when next-cp-position
            (send console-editor scroll-to-position 
                  next-cp-position #f 
                  (send console-editor last-position)
                  'start))))
      
      (define/public (focus-console-on-prior-checkpoint)
        (send checkpoints cursor-backward!)
        (set! focused? #t)
        (enable/disable-buttons)
        (let ([prior-cp-position (get-checkpoint-position)])
          (when prior-cp-position
            (send console-editor scroll-to-position prior-cp-position #f 
                  (send console-editor last-position) 
                  'start))))
      (super-new)
      ))
  
  )