(module tool mzscheme

  (require (lib "tool.ss" "drscheme")
           (lib "class.ss")
           (lib "unit.ss")
           (lib "etc.ss")
           (rename "../language/acl2-reader.scm" acl2-reader read-syntax)
           "../language/printer.scm"
           "custom-drscheme-language.scm"
           "gui/proof-signatures.scm"
           "gui/proof-ui.scm")

  (provide tool@)

  (define-signature language^
    (make-language))

  (define-unit language@
    (import proof-language^ custom-language-level^)
    (export language^)

    (define (dracula-manuals ms)
      (values (list #"acl2-html-docs" #"teachpack" #"drscheme" #"help") #t))

    (define capability-table
      (hash-table
       ['drscheme:define-popup (cons "(def" "(defun ...)")]
       ['drscheme:language-menu-title "Modular ACL2"]
       ['drscheme:special:insert-fraction #f]
       ['drscheme:special:insert-lambda #f]
       ['drscheme:special:insert-image #f]
       ['drscheme:special:insert-comment-box #f]
       ['drscheme:special:insert-gui-tool #f]
       ['drscheme:special:slideshow-menu-item #f]
       ['drscheme:special:insert-text-box #f]
       ['drscheme:special:xml-menus #f]
       ['drscheme:special:uninstall-acl2-tool #t]))

    (define (make-language)
      (custom-language-level
       "Modular ACL2 [Experimental]"
       '(planet "modular/language.scm" ("cce" "dracula.plt"))
       #:number 2000
       #:hierarchy '(("Dracula Languages" . 5000))
       #:summary "ACL2 + modules"
       #:url "http://www.ccs.neu.edu/home/cce/acl2/"
       #:reader acl2-reader
       proof-language-mixin
       (language-level-render-mixin acl2-convert #f)
       (language-level-help-desk-mixin dracula-manuals)
       (language-level-capability-mixin capability-table)
       language-level-eval-as-module-mixin
       language-level-no-executable-mixin)))

  (define-unit install@
    (import drscheme:tool^ proof-tab^ proof-text^ proof-frame^ language^)
    (export drscheme:tool-exports^)

    (drscheme:get/extend:extend-tab proof-tab-mixin)
    (drscheme:get/extend:extend-unit-frame proof-frame-mixin)
    (drscheme:get/extend:extend-definitions-text proof-text-mixin)

    (define (phase1) (void))
    (define (phase2)
      (drscheme:language-configuration:add-language (make-language))))

  (define-compound-unit/infer tool@
    (import drscheme:tool^)
    (export drscheme:tool-exports^)
    (link custom-language-level@ proof-ui@ language@ install@))

  )