#|
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 "tool.ss" "drscheme")
           (lib "mred.ss" "mred")
           (lib "framework.ss" "framework")
           (lib "class.ss")
           (lib "unit.ss"))
  (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) 
        (void)
        #;(parameterize ([current-output-port (get-write-port)])
            (newline)
            (display ">>> This ACL2 session has been shut down. <<<")
            (newline)))
      
      ;; 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)
                                               interrupt-acl2))))
          #;(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]
                     [callback 
                      (lambda (b e) (void)
                        (send prooftree-editor 
                              focus-console-on-prior-checkpoint))]))
          (send previous-checkpoint enable #f)
          
          (set! next-checkpoint
                (new button% 
                     [label "Next Checkpoint >"] 
                     [parent acl2-button-panel]
                     [callback 
                      ;; refocus window to the next checkpoint
                      (lambda (b e) (void)
                        (send prooftree-editor 
                              focus-console-on-next-checkpoint))]))
          (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
                 (text:hide-caret/selection-mixin
                  text:searching%))
          ()
          (define/augment (can-load-file?) #f)
          (define/override (allow-close-with-no-filename?) #t)
          (super-new)))
      
      #;(define/augment (can-close?) #f)
      
      ;; Need to figure out how to override the default editor:file<%>
      ;; save-warning-dialog
      (define/augment (on-close)
        (notify-controller-of-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)
                             (string-append
                              "acl2." 
                              (number->string (current-seconds))
                              ".txt"))))
      (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)
      ))
  
  #|
  ;; TEMPORARY TESTING CODE
  (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)))
      str))
  
  (show-proof-window test-data)
  |#
  )