• Top
    • Documentation
      • Xdoc
        • Undocumented
        • Save
        • Defsection
        • Markup
        • Preprocessor
        • Emacs-links
          • Defxdoc
          • Katex-integration
          • Constructors
          • Entities
          • Save-rendered
          • Add-resource-directory
          • Defxdoc+
          • Testing
          • Order-subtopics
          • Save-rendered-event
          • Archive-matching-topics
          • Missing-parents
          • Archive-xdoc
          • Xdoc-extend
          • Set-default-parents
          • Defpointer
          • Defxdoc-raw
          • Xdoc-tests
          • Xdoc-prepend
          • Defsection-progn
          • Gen-xdoc-for-file
        • ACL2-doc
        • Pointers
        • Doc
        • Documentation-copyright
        • Args
        • ACL2-doc-summary
        • Finding-documentation
        • Broken-link
      • Books
      • Recursion-and-induction
      • Boolean-reasoning
      • Projects
      • Debugging
      • Std
      • Proof-automation
      • Macro-libraries
      • ACL2
      • Interfacing-tools
      • Hardware-verification
      • Software-verification
      • Testing-utilities
      • Math
    • Xdoc

    Emacs-links

    Instructions for integrating XDOC web pages with Emacs.

    Preprocessor directives such as @(def get-xdoc-table) result in the introduction of special links for Emacs. Here's what these links look like:

    Function: get-xdoc-table

    (defun get-xdoc-table (world)
           (cdr (assoc-eq 'doc
                          (table-alist 'xdoc world))))

    Depending on your environment, it may be easy to configure your web browser so that clicking on these links will cause Emacs to directly open up the appropriate source file and jump to the named function.

    The basic idea is:

    • Each Emacs link generates a Data URIs that tells your web browser to download a new, generated file whose MIME type is application/x-acl2-xdoc-link.
    • You configure your web browser to send application/x-acl2-xdoc-link files to Emacs.
    • You configure your Emacs to carry out a tags search instead of loading these files.

    The net effect is that clicking on these links will send you directly to the desired function in the source code. This is really slick if you can get it working.

    Configuring Emacs

    Loading the XDOC Elisp

    The XDOC directory includes a file called xdoc.el, which tells emacs what to do with these xdoc-link files. To tell emacs to load this file at startup, you can just add a command to your .emacs file like:

    (load "/path/to/acl2/books/xdoc/xdoc.el")

    This file will be loaded automatically if you load the file of emacs utilities that comes with ACL2:

    (load "/path/to/acl2/emacs/emacs-acl2.el")

    Managing your TAGS tables

    For emacs to make sense of the links you follow, it will need to have the appropriate tags tables loaded for all of the libraries you are using.

    If you aren't familiar with tags, you basically just need to:

    • Occasionally generate TAGS files for your libraries, using the command etags *.lisp or similar.
    • Tell Emacs to "visit" these tags tables with visit-tags-table.
    Jared's Approach:
    • I add a TAGS target to my Makefiles, so that when I build my library the etags *.lisp command is re-run and the TAGS file is kept up to date. The Makefile syntax is:
      TAGS: $(wildcard *.lisp)
            etags *.lisp
    • Then, in my .emacs file, I have a series of commands like the following:
      (ignore-errors (visit-tags-table "/path/to/acl2/TAGS"))
      (ignore-errors (visit-tags-table "/path/to/acl2/books/xdoc/TAGS"))
      (ignore-errors (visit-tags-table "/path/to/my/stuff/TAGS"))
      This ensures that the relevant TAGS files are loaded every time I start Emacs. The use of ignore-errors prevents Emacs from complaining if one of these TAGS files was deleted in a "make clean" or similar.
    • One final addition to the .emacs file is:
      (setq tags-revert-without-query t)
      which tells Emacs to go ahead and reload these files when they are rebuilt by Make, instead of prompting you if you want to reload them.

    Setting up Emacsclient (recommended)

    You can set things up so that links open up in new instances of Emacs, or in new buffers of an already-running Emacs.

    If you want everything to open up in a new instance of Emacs, you can skip this section. But I prefer to use a single Emacs for everything, and just have links open up in new buffers.

    This is quite easy. First, add (server-start) to your .emacs file and restart Emacs.

    Next, to ensure everything is working properly, launch a separate terminal and type:

    emacsclient --no-wait my-file

    If all is well, my-file will be loaded into your already-running emacs as a new buffer.

    Configuring the Web Browser

    The last thing we need to do is instruct your web browser to send xdoc-link files to Emacs.

    How to do this depends on your web browser and/or operating system. In some cases it may be hard to pass command-line options to emacs directly, so you may find it useful to use the script emacsclient-wrapper.sh, found in the xdoc directory.

    The basic starting point is probably to try to click on an emacs link like append and try to tell your browser to open it with the emacsclient-wrapper.sh script. If your browser opens it with some other program, you might need to edit the default file associations of your operating system or window manager.