From d58a743b89b624457d22b0417f5a1ae31dc54d50 Mon Sep 17 00:00:00 2001
From: Casey Klein <clklein@racket-lang.org>
Date: Mon, 8 Aug 2011 11:11:03 -0500
Subject: [PATCH] Fixes define-judgment-form at the top-level with errortrace
 enabled

---
 collects/redex/private/reduction-semantics.rkt | 12 ++++++++++--
 collects/redex/tests/tl-test.rkt               | 11 +++++++++++
 2 files changed, 21 insertions(+), 2 deletions(-)

diff --git a/collects/redex/private/reduction-semantics.rkt b/collects/redex/private/reduction-semantics.rkt
index cb14524538..01d47a53d5 100644
--- a/collects/redex/private/reduction-semantics.rkt
+++ b/collects/redex/private/reduction-semantics.rkt
@@ -1495,8 +1495,7 @@
          (define nts (definition-nts lang stx syn-err-name))
          (define-values (judgment-form-name dup-form-names mode position-contracts clauses)
            (parse-define-judgment-form-body #'body syn-err-name stx))
-         (syntax-property
-          (prune-syntax
+         (define definitions
            #`(begin
                (define-syntax #,judgment-form-name 
                  (judgment-form '#,judgment-form-name '#,mode #'judgment-form-proc #'#,lang #'judgment-form-lws))
@@ -1517,6 +1516,15 @@
                                    [(_ clauses)
                                     (compile-judgment-form-lws (syntax->list #'clauses))]))])
                    (delayed #,clauses)))))
+         (syntax-property
+          (prune-syntax
+           (if (eq? 'top-level (syntax-local-context))
+               ; Introduce the names before using them, to allow
+               ; judgment form definition at the top-level.
+               #`(begin 
+                   (define-syntaxes (judgment-form-proc judgment-form-lws) (values))
+                   #,definitions)
+               definitions))
           'disappeared-use
           (map syntax-local-introduce dup-form-names)))]))
   
diff --git a/collects/redex/tests/tl-test.rkt b/collects/redex/tests/tl-test.rkt
index e0f2cd4df8..ffc706a3e9 100644
--- a/collects/redex/tests/tl-test.rkt
+++ b/collects/redex/tests/tl-test.rkt
@@ -2024,6 +2024,17 @@
                                   
                                   })))
     
+    (parameterize ([current-namespace (make-base-namespace)])
+      (eval '(require errortrace))
+      (eval '(require redex/reduction-semantics))
+      (eval '(define-language L))
+      (eval '(define-judgment-form L
+               mode : I
+               [(J a)
+                (J b)]
+               [(J b)]))
+      (test (eval '(judgment-holds (J a))) #t))
+    
     (parameterize ([current-namespace (make-base-namespace)])
       (eval '(require redex/reduction-semantics))
       (eval '(define-language L