Defines a unit that provides a window for viewing the ACL2 console
and proof trees.  Unit must be linked with an acl2-controller.

#| NOTE:
There's a little too much mutation in here.  Probably need to refactor
some proof-tree stuff out into the controller class.
(module acl2-proof-window mzscheme
  (require (lib "" "drscheme")
           (lib "" "mred")
           (lib "" "framework")
           (lib "")
           (lib ""))
  (require (file "proof-tree-editor.scm"))
  (provide acl2-proof-window%)
  (define *size-pref-key* 'acl2-proof-window-size)
  ;; only called once, upon startup
  (frame:setup-size-pref *size-pref-key* 600 500)
  (define acl2-proof-window%
    (class* (frame:size-pref-mixin frame:searchable%) ()
      (inherit get-editor)
      (init-field notify-controller-of-close)
      (field [proof-tree-canvas #f])
      ;; Buttons
      (field [previous-checkpoint #f])
      (field [next-checkpoint #f])
      (define/public (get-write-port)
        (send (get-editor) get-out-port))
      (define/public (shutdown-console) 
        #;(parameterize ([current-output-port (get-write-port)])
            (display ">>> This ACL2 session has been shut down. <<<")
      ;; Display the proof tree & set up checkpoints
      (define/public (set-proof-tree str)
        (send prooftree-editor set-proof-tree str))
      ;; Puts the Checkpoint buttons and prooftree display above the console
      (define/override (make-root-area-container % parent)
        (let* ([vp (new vertical-pane% [parent parent] [stretchable-height #f])]
               [acl2-button-panel (new horizontal-panel% [parent vp]
                                       [stretchable-height #f]
                                       [stretchable-width #f]
                                       [alignment '(center center)])]
               [vp2 (new panel:vertical-dragable% 
                         [parent parent] 
                         #;[stretchable-height #f])]
               [canvas (new canvas:basic% [parent vp2]
                            [editor #f])])
          (set! proof-tree-canvas canvas)
          #;(new button% (label "Interrupt ACL2") (parent acl2-button-panel)
                 (callback (lambda (b e) (send (get-acl2-controller)
          #;(new button% (label "Kill ACL2") (parent acl2-button-panel)
                 (callback (lambda (b e) (kill-thunk))))
          (set! previous-checkpoint
                (new button% 
                     [label "< Previous Checkpoint"] 
                     [parent acl2-button-panel]
                      (lambda (b e) (void)
                        (send prooftree-editor 
          (send previous-checkpoint enable #f)
          (set! next-checkpoint
                (new button% 
                     [label "Next Checkpoint >"] 
                     [parent acl2-button-panel]
                      ;; refocus window to the next checkpoint
                      (lambda (b e) (void)
                        (send prooftree-editor 
          (send previous-checkpoint enable #f)
          (super make-root-area-container % vp2)))
      ;; clear ought to be erase... but do we want that?
      (define/public (clear-console)
        (send (get-editor) clear))
      (define/override (get-editor%) 
        (class* (text:ports-mixin
          (define/augment (can-load-file?) #f)
          (define/override (allow-close-with-no-filename?) #t)
      #;(define/augment (can-close?) #f)
      ;; Need to figure out how to override the default editor:file<%>
      ;; save-warning-dialog
      (define/augment (on-close)
      ;; HELP MENU
      (define/override (help-menu:about-string)
        "About Master ACL2")
      (define/override (help-menu:about-callback item evt)
        (message-box "About Master ACL2"
                     "Master ACL2 is a language level for DrScheme and an interface to ACL2."))
      (super-new ;(height 500) (width 600)
       [size-preferences-key *size-pref-key*]
       (filename (build-path (find-system-path 'temp-dir)
                              (number->string (current-seconds))
      (field [prooftree-editor (new proof-tree-editor% 
                                    [console-editor (get-editor)]
                                    [previous-button previous-checkpoint]
                                    [next-button next-checkpoint])])
      (send proof-tree-canvas set-editor prooftree-editor)
      (send prooftree-editor insert "(This is the proof-tree window.)")
      (send (get-editor) lock #t) ;; this window is output only
      (send (get-editor) hide-caret #t)
  (define *test-file* (build-path "~" "Projects" "drscheme-acl2" "trunk" "test" "DrSEpkg" "Ex1Crypto" "iEx1.lisp"))
  (define test-data
    (let [(str (make-string (file-size *test-file*)))]
      (with-input-from-file *test-file*
        (lambda () (read-string! str)))
  (show-proof-window test-data)