#|
Locate checkpointed goals in a text editor that contains an ACL2 proof transcript.
|#
(module checkpoint mzscheme
  (require (lib "class.ss")
           (lib "struct.ss")
           (lib "list.ss")
           (lib "mred.ss" "mred"))
  
  (provide (struct checkpoint (name position))
           make-checkpoints)
  
  (define *proof-tree-start* "\n<< Starting proof tree logging >>\n")
  
  ;; A checkpoint is (make-checkpoint String Number)
  (define-struct/properties checkpoint (name position)
    ([prop:custom-write (lambda (x port write?)
                          (fprintf port "#checkpoint(~a ~a)"
                                   (checkpoint-name x)
                                   (checkpoint-position x)))]))
  
  ;; find-position-of-goal : String Editor -> (union Number #f)
  (define (find-position-of-goal goal-name editor)
    (let loop ([start (send editor find-string 
                            *proof-tree-start* 'backward (send editor last-position) 'eof)])
      ;; If we don't find the thing, the I/O thread must be lagging.
      ;; It would be nice to have an actual waitable event here instead of the
      ;; half-busy-loop, half yield hack...
      (if start
          (send editor find-string goal-name 'forward start 'eof)
          (begin (yield)
                 (let ([last-posn (send editor last-position)])
                   (loop (send editor find-string 
                               *proof-tree-start* 
                               'backward last-posn 'eof))))
          )))
  
  (define (make-checkpoints goal-names editor)
    (let ([answer 
           (reverse (foldl (lambda (goal checkpoints)
                             (cond [(find-position-of-goal goal editor)
                                    => (lambda (posn)
                                         (cons (make-checkpoint goal posn)
                                               checkpoints))]
                                   [else checkpoints]))
                           '()
                           goal-names))])
      answer))
  
  )