• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Community
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
      • Theories
      • Rule-classes
      • Proof-builder
      • Recursion-and-induction
      • Hons-and-memoization
      • Events
      • Parallelism
      • History
      • Programming
      • Operational-semantics
      • Real
      • Start-here
        • Gentle-introduction-to-ACL2-programming
        • ACL2-tutorial
          • Introduction-to-the-theorem-prover
          • Pages Written Especially for the Tours
          • The-method
          • Advanced-features
          • Interesting-applications
          • Tips
          • Alternative-introduction
          • Tidbits
          • Annotated-ACL2-scripts
          • Startup
          • ACL2-as-standalone-program
          • ACL2-sedan
            • Defunc
            • Cgen
            • Ccg
            • Defdata
            • ACL2s-user-guide
            • ACL2s-tutorial
            • ACL2s-implementation-notes
            • Match
            • ACL2s-faq
            • ACL2s-intro
            • ACL2s-defaults
            • Definec
            • ACL2s-utilities
            • ACL2s-interface
              • Itest?-query
              • ACL2s-event
              • ACL2s-query
              • Quiet-mode-hooks
              • ACL2s-interface-symbol-package-tips
              • ACL2s-compute
              • ACL2s-interface::ACL2s-interface-utils
              • Quiet-mode
                • Capture-output
              • ACL2s-installation
            • Talks
            • Nqthm-to-ACL2
            • Tours
            • Emacs
          • About-ACL2
        • Miscellaneous
        • Output-controls
        • Bdd
        • Macros
        • Installation
        • Mailing-lists
      • Interfacing-tools
      • Hardware-verification
      • Software-verification
      • Math
      • Testing-utilities
    • ACL2s-interface

    Quiet-mode

    Control whether or not the acl2s-interface attempts to suppress ACL2 printed output

    Examples:
    (quiet-mode-on)    ; from this point forward all acl2s-interface functions will
                       ; attempt to suppress all ACL2 printed output
    (quiet-mode-off)   ; (default) from this point forward all acl2s-interface
                       ; functions will print any ACL2 output as normal

    Most of the ACL2s interface functions also take a :quiet argument for locally controlling quiet mode without affecting the global setting.

    The ACL2s interface provides hooks for code that should run when quiet mode is enabled or disabled. See quiet-mode-hooks for more information.