Skip to content
Commits on Feb 7, 2011
  1. Fixed "wrong number of arguments" error when invoking agda2-test-run-…

    committed
    …one.
    
    Ignore-this: 9c03898f1415345005982b82394c37b8
    
    darcs-hash:20110207100932-01858-49c4da7e4711a0ef9f5dc84031572413e866ab4d.gz
Commits on Feb 6, 2011
  1. @arc

    Simplify key-binding definitions

    arc committed
    Ignore-this: eff4aa5b400eaa021ae2d451490bf326
    
    Previously, we had a function which binds each key just for the current
    buffer, then hooked that function into the major mode.  Simpler: ensure the
    main Agda mode is loaded before we start (and therefore that it has created
    its mode-specific keymap), then directly define the bindings we want in that
    keymap.
    
    darcs-hash:20110206195954-d6142-b74e65e0dcdf359bca0ad7d419862f5f925c7d5e.gz
  2. @arc

    New `agda2-test-run-region` command

    arc committed
    Ignore-this: d31f1f16b657ff1ede355d18e9e33b15
    
    Runs all the tests within the current region.
    
    darcs-hash:20110206194628-d6142-f712d8173a40846d6f5536ea9f4e6ed9fee4cbf3.gz
  3. @arc

    Change keybindings

    arc committed
    Ignore-this: 56f8aa9802762f4b37beeee57c0424b5
    
    We now use `C-c C-v C-a` to run all tests, and `C-c C-v C-v` to run a test
    near point.  This change will ease adding commands that run other groups of
    tests.
    
    darcs-hash:20110206194505-d6142-32c0152350d616eeb1f969a3be46ccefa0ad6090.gz
  4. @arc

    Replace …-find-all-in-current-buffer with …-find-in-region

    arc committed
    Ignore-this: d43db090b54de5e1b1c787602d3e94d9
    
    A function to find test cases in the region is more reusable than one which
    finds all cases in the buffer.
    
    darcs-hash:20110206194042-d6142-874011355b210069f0d77ea0f2622d84e1a7f7f0.gz
  5. @arc

    Refactor: eliminate single-use variable

    arc committed
    Ignore-this: 552c7975041226528ec0511d1d7c9798
    
    darcs-hash:20110206151746-d6142-fb6e5ce1548225a2ecfb5bf1b302ec34ce219ac6.gz
  6. Fixed error in TAP plan syntax.

    committed
    Ignore-this: 98bea7f00327e1f968d74002988ccb8d
    
    darcs-hash:20110206122621-01858-fa510c1fa2dda55af217d9dc03d0c03e21299653.gz
  7. @arc

    Highlight failing tests in the output

    arc committed
    Ignore-this: 3b2a9bbc0f2680be0b94d86932e9a985
    
    darcs-hash:20110206120914-d6142-d9c28761c997a09a155a63428a3628c34fd67579.gz
  8. @arc

    Tighten regex

    arc committed
    Ignore-this: 1064407abe0c61359f7ccb1870194003
    
    One of the quantifiers was incorrectly greedy; this won't be a problem until
    test descriptions can span multiple lines, but it's worth fixing anyway.
    
    darcs-hash:20110206115117-d6142-76f01d09632de5072cc84e03389c830e2a84f2ef.gz
  9. @arc

    Jump from test output to source

    arc committed
    Ignore-this: b722aeb9702cad9b172616f9896a88e5
    
    Embed buttons in the TAP output buffer, so that clicking (or hitting RET) on
    a test's ok/not-ok line takes you directly to the source of that test in its
    original buffer.
    
    Actually, Emacs wants you to middle-click on each button.  But if you set
    `mouse-1-click-follows-link` true -- strongly recommended anyway! -- then a
    plain click will suffice.
    
    darcs-hash:20110206114746-d6142-30a9ef73b2fe8cd293d4f65debb875498af5771e.gz
Commits on Feb 4, 2011
  1. @arc

    Fix TAP syntax error

    arc committed
    Ignore-this: adc51bc6462077a357027c7a46667080
    
    No plan was being emitted, so TAP was unable to successfully process the
    test output.
    
    darcs-hash:20110204153723-d6142-12fb9bea0f50a9539d37fc90066c768d8d0a63b3.gz
  2. Fixed punctuation of examples in commentary.

    committed
    Ignore-this: be97c8d5010695b31eeed9eac0f32bd1
    
    darcs-hash:20110204224732-01858-2c39b0febf438b6e3d8cdb87bab53328ae1f3c30.gz
  3. @arc

    Allow running single tests interactively

    arc committed
    Ignore-this: 5a36a6af0c66e2a33f8996124ea5bba7
    
    The command bound to `C-c C-v` now defaults to just running the most
    suitable test it can find near point -- either the last one ending on the
    same line as point, or the first starting after point.  The previous
    behaviour of running all tests in the buffer can be obtained by adding a
    prefix argument when invoking the command.
    
    darcs-hash:20110204142629-d6142-888579b735b5394970be1812e98a9b9095182e53.gz
  4. @arc

    Use consistent function/variable naming

    arc committed
    Ignore-this: 5c08c92eff1b253720ac707d77b1ccb6
    
    All globals now begin "agda2-test-"; we're now treating that as the
    namespace we occupy.
    
    darcs-hash:20110204133750-d6142-ea438a219524c9ada8a1613603cda6b225b87b63.gz
  5. @arc

    Tweak test-case regex

    arc committed
    Ignore-this: 580c07e0d8ebeb6a1d605cd268055b58
    
    - Ensure the leading "test" indicator is the start of a symbol; this allows
      temporarily disabling a failing test merely by doing s/test/x&/
    - Require at least one whitespace character after "test"
    - Exclude whitespace before trailing ";" from the expected value
    
    darcs-hash:20110204132824-d6142-b80619207644dfe88ba38f1487983379f4e4686c.gz
Commits on Feb 3, 2011
  1. @arc

    Change default `agda2-test-all` keybinding

    arc committed
    Ignore-this: 6df91a001917426f0c1c984b86dd1572
    
    The binding was previously `C-c t`; but the convention in Emacs is that
    bindings of the form `C-c LETTER` are reserved for end users; major modes
    may use `C-c C-LETTER` instead.
    
    However, the obvious binding, `C-c C-t`, is used by `agda2-goal-type` in the
    standard agda-mode.el, so we have to pick something different.  I've gone
    for `C-c C-v` on the grounds that it's easy to type, otherwise unused, and
    has a vaguely reasonable mnemonic ("verify").
    
    darcs-hash:20110203172939-d6142-61b3f22d50e927fa33536b0b024dca52c4075869.gz
  2. @arc

    Minor documentation tweaks

    arc committed
    Ignore-this: 7acada0cee35153671c88091fc6b0ed7
    
    darcs-hash:20110203172710-d6142-9f53de769cae1118e67ad7b09f6bf7679663c014.gz
  3. @arc

    Avoid near-identical variable names

    arc committed
    Ignore-this: 5f96a68aa58e491d0698769fa1ad6f1e
    
    In this case, the easiest approach is to use just one variable, but default
    it appropriately.
    
    darcs-hash:20110203172124-d6142-c60484148ded5595469a37e3a1f4fa649d042e85.gz
  4. @arc

    Whitespace fixups

    arc committed
    Ignore-this: ba51b5a2c18c657c5e5c688965424245
    
    - Delete trailing whitespace
    - Delete excess line-internal whitespace
    - Add blank lines between top-level forms
    - Indent uniformly with spaces (not mixed tabs/spaces)
    
    darcs-hash:20110203171510-d6142-7d865d63ea90b094296ff648b629248451f1c1c9.gz
  5. TAPified the test output.

    committed
    Ignore-this: 1a97f533fc69f7942921611f081f5108
    
    darcs-hash:20110203161556-01858-4d26805ab07e73e6c82509029a23c6c38598d4cc.gz
  6. Added a Commentary, in line with documentation guidelines.

    committed
    Ignore-this: c57fec9489deabc8dc752971fc9e1f2
    
    darcs-hash:20110203161514-01858-6e288fab24979397923992253b7cfca01a1ff44b.gz
  7. Aligned docs with Emacs conventions; documented the actual test format.

    committed
    Ignore-this: 10c2d0f0c533a4ea9852b219c41e2f81
    
    darcs-hash:20110203152935-01858-69165383404889ff4d633680d83d74d9879fe315.gz
  8. Added some docs.

    committed
    Ignore-this: d94227d5bbe6704a7638883bf3262383
    
    darcs-hash:20110203151403-01858-1d27ed101a95cac1422b896acf2dd8b5780ce277.gz
  9. Changed name of buffer to "Agda test results"

    committed
    Ignore-this: 48a1cd6450d667bb6562d696e0ba9015
    
    darcs-hash:20110203144834-01858-72f8f201695b088495ac65346a4e879c9b0eb39a.gz
  10. Remove now-useless self-tests.

    committed
    Ignore-this: e2fa6427547c04a81f6e2ae124420ba3
    
    darcs-hash:20110203144318-01858-8718403d09a24930f2573bc4fac6176be1207f84.gz
  11. User's guide (README)

    Gitit committed
    Ignore-this: fcb5856c42f712169bc574f8567c3a1b
    
    darcs-hash:20110203143549-f68ea-17c96cbdab6083f7fbdb93db851884bd4a4df161.gz
  12. Default help page

    Gitit committed
    Ignore-this: bf1de06c69a82a8b70e0ec109c3144a7
    
    darcs-hash:20110203143549-f68ea-6743672161cc226eb9fb00f09ac8758b7c859ecf.gz
  13. Default front page

    Gitit committed
    Ignore-this: c173c4b8676ae708d06d4f0221b18b7c
    
    darcs-hash:20110203143549-f68ea-9fdee29580e4178328c886ef53b588bdcd3eace5.gz
  14. Install keybindings on entry to agda2-mode.

    committed
    Ignore-this: de1f0ec1a6ce9aab3222cc34695e9802
    
    darcs-hash:20110203141054-01858-54c4033f3ce30704fbe64493b77b4653d31b9329.gz
  15. Calling into Agda now works.

    committed
    Ignore-this: 719d2f36ecfb6d65497635a0ce13b42b
    
    darcs-hash:20110203140858-01858-e3480b3cb12e4d8f622653b52911194741d4e16a.gz
Commits on Feb 2, 2011
  1. halfarsed start on the actual Agda calling code.

    committed
    Ignore-this: 6c9daae77b9625d3887070031e4dc591
    
    darcs-hash:20110202191611-01858-22ecd0e7f2acb50c7085e4d28fdefafc44857d70.gz
  2. Refactored code into producer/consumer, did some more splitting up.

    committed
    Ignore-this: a885b31e464a2b039426c44d46095b5c
    
    darcs-hash:20110202232544-01858-002f1d6b2131011813bac52b13f45286eafdcc21.gz
  3. Aaron's suggested changes.

    committed
    Ignore-this: c4a1fcc069ad00c7882a2bf1b52d9beb
    
    darcs-hash:20110202193200-01858-6f884953992fef630a6a6d5f7c03884682318028.gz
  4. Wrapped the "run all tests" code in a function.

    committed
    Ignore-this: fba8ebe2a6087137bb706b1617647145
    
    darcs-hash:20110202145350-01858-5b9de0b83e72050c9b2f95159bdde4ebacc20543.gz
  5. Mucking about with buffers and regexen.

    committed
    Ignore-this: 49c1a5b1da7771cfdffe692728de79b9
    
    darcs-hash:20110202144128-01858-075acb9c4be27370a57cade2cdd0e2b4f97a3c8d.gz
Something went wrong with that request. Please try again.