From f1be76f2e20d12c5bf3c3bb13e7577661e2d03bb Mon Sep 17 00:00:00 2001
From: Casey Klein <clklein@racket-lang.org>
Date: Thu, 9 Sep 2010 12:06:41 -0500
Subject: [PATCH] Special-cases DrRacket's definition-finder to find Redex
 metafunction definitions

---
 collects/drracket/private/get-defs.rkt    | 138 ++++++++++++++++++++++
 collects/drracket/private/unit.rkt        | 116 +-----------------
 collects/tests/drracket/get-defs-test.rkt |  54 +++++++++
 3 files changed, 193 insertions(+), 115 deletions(-)
 create mode 100644 collects/drracket/private/get-defs.rkt
 create mode 100644 collects/tests/drracket/get-defs-test.rkt

diff --git a/collects/drracket/private/get-defs.rkt b/collects/drracket/private/get-defs.rkt
new file mode 100644
index 0000000000..826530392b
--- /dev/null
+++ b/collects/drracket/private/get-defs.rkt
@@ -0,0 +1,138 @@
+#lang racket/base
+
+(require racket/class
+         racket/function
+         racket/list
+         string-constants)
+
+(provide (struct-out defn)
+         get-definitions)
+
+;; defn = (make-defn number string number number)
+(define-struct defn (indent name start-pos end-pos) #:mutable)
+
+;; get-definitions : string boolean text -> (listof defn)
+(define (get-definitions tag-string indent? text)
+  (let* ([min-indent 0]
+         [defs (let loop ([pos 0])
+                 (let ([defn-pos (send text find-string tag-string 'forward pos 'eof #t #f)])
+                   (cond
+                     [(not defn-pos) null]
+                     [(in-semicolon-comment? text defn-pos)
+                      (loop (+ defn-pos (string-length tag-string)))]
+                     [else
+                      (let ([indent (get-defn-indent text defn-pos)]
+                            [name (get-defn-name text (+ defn-pos (string-length tag-string)))])
+                        (set! min-indent (min indent min-indent))
+                        (cons (make-defn indent name defn-pos defn-pos)
+                              (loop (+ defn-pos (string-length tag-string)))))])))])
+    
+    ;; update end-pos's based on the start pos of the next defn
+    (unless (null? defs)
+      (let loop ([first (car defs)]
+                 [defs (cdr defs)])
+        (cond
+          [(null? defs) 
+           (set-defn-end-pos! first (send text last-position))]
+          [else (set-defn-end-pos! first (max (- (defn-start-pos (car defs)) 1)
+                                              (defn-start-pos first)))
+                (loop (car defs) (cdr defs))])))
+    
+    (when indent?
+      (for-each (λ (defn)
+                  (set-defn-name! defn
+                                  (string-append
+                                   (apply string
+                                          (vector->list
+                                           (make-vector 
+                                            (- (defn-indent defn) min-indent) #\space)))
+                                   (defn-name defn))))
+                defs))
+    defs))
+
+;; in-semicolon-comment: text number -> boolean
+;; returns #t if `define-start-pos' is in a semicolon comment and #f otherwise
+(define (in-semicolon-comment? text define-start-pos)
+  (let* ([para (send text position-paragraph define-start-pos)]
+         [start (send text paragraph-start-position para)])
+    (let loop ([pos start])
+      (cond
+        [(pos . >= . define-start-pos) #f]
+        [(char=? #\; (send text get-character pos)) #t]
+        [else (loop (+ pos 1))]))))
+
+;; get-defn-indent : text number -> number
+;; returns the amount to indent a particular definition
+(define (get-defn-indent text pos)
+  (let* ([para (send text position-paragraph pos)]
+         [para-start (send text paragraph-start-position para #t)])
+    (let loop ([c-pos para-start]
+               [offset 0])
+      (if (< c-pos pos)
+          (let ([char (send text get-character c-pos)])
+            (cond
+              [(char=? char #\tab)
+               (loop (+ c-pos 1) (+ offset (- 8 (modulo offset 8))))]
+              [else
+               (loop (+ c-pos 1) (+ offset 1))]))
+          offset))))
+
+;; whitespace-or-paren?
+(define (whitespace-or-paren? char)
+  (or (char=? #\) char)
+      (char=? #\( char)
+      (char=? #\] char)
+      (char=? #\[ char)
+      (char-whitespace? char)))
+
+;; skip : text number (char -> bool) -> number
+;; Skips characters recognized by `skip?'
+(define (skip text pos skip?)
+  (let loop ([pos pos])
+    (if (>= pos (send text last-position))
+        (send text last-position)
+        (let ([char (send text get-character pos)])
+          (cond
+            [(skip? char)
+             (loop (+ pos 1))]
+            [else pos])))))
+
+;; skip-to-whitespace/paren : text number -> number
+;; skips to the next parenthesis or whitespace after `pos', returns that position.
+(define (skip-to-whitespace/paren text pos)
+  (skip text pos (negate whitespace-or-paren?)))
+
+;; skip-whitespace/paren : text number -> number
+;; skips past any parenthesis or whitespace
+(define (skip-whitespace/paren text pos)
+  (skip text pos whitespace-or-paren?))
+
+;; skip-past-non-whitespace : text number -> number
+;; skips to the first whitespace character after the first non-whitespace character
+(define (skip-past-non-whitespace text pos)
+  (skip text (skip text pos char-whitespace?) (negate char-whitespace?)))
+
+;; get-defn-name : text number -> string
+;; returns the name of the definition starting at `define-pos',
+;; assuming that the bound name is the first symbol to appear
+;; after the one beginning at `define-pos'. This heuristic 
+;; usually finds the bound name, but it breaks for Redex
+;; metafunction definitions (thus the hack below).
+(define (get-defn-name text define-pos)
+  (let* ([end-suffix-pos (skip-to-whitespace/paren text define-pos)]
+         [suffix (send text get-text define-pos end-suffix-pos)]
+         [end-header-pos 
+          (cond [(regexp-match #rx"^-metafunction(/extension)?$" suffix)
+                 => (λ (m)
+                      (let ([extension? (second m)])
+                        (skip-past-non-whitespace
+                         text
+                         (if extension?
+                             (skip-past-non-whitespace text end-suffix-pos)
+                             end-suffix-pos))))]
+                [else end-suffix-pos])]
+         [start-name-pos (skip-whitespace/paren text end-header-pos)]
+         [end-name-pos (skip-to-whitespace/paren text start-name-pos)])
+    (if (>= end-suffix-pos (send text last-position))
+        (string-constant end-of-buffer-define)
+        (send text get-text start-name-pos end-name-pos))))
diff --git a/collects/drracket/private/unit.rkt b/collects/drracket/private/unit.rkt
index 221df67300..637c271613 100644
--- a/collects/drracket/private/unit.rkt
+++ b/collects/drracket/private/unit.rkt
@@ -33,6 +33,7 @@ module browser threading seems wrong.
            "drsig.rkt"
            "auto-language.rkt"
            "insert-large-letters.rkt"
+           "get-defs.rkt"
            (prefix-in drracket:arrow: "../arrow.rkt")
            
            mred
@@ -1033,122 +1034,7 @@ module browser threading seems wrong.
                    [string-constant-no-full-name-since-not-saved 
                     (string-constant no-full-name-since-not-saved)])))
     
-    ;; defn = (make-defn number string number number)
-    (define-struct defn (indent name start-pos end-pos) #:mutable)
-    
-    ;; get-definitions : boolean text -> (listof defn)
-    (define (get-definitions tag-string indent? text)
-      (let* ([min-indent 0]
-             [defs (let loop ([pos 0])
-                     (let ([defn-pos (send text find-string tag-string 'forward pos 'eof #t #f)])
-                       (cond
-                         [(not defn-pos) null]
-                         [(in-semicolon-comment? text defn-pos)
-                          (loop (+ defn-pos (string-length tag-string)))]
-                         [else
-                          (let ([indent (get-defn-indent text defn-pos)]
-                                [name (get-defn-name text (+ defn-pos (string-length tag-string)))])
-                            (set! min-indent (min indent min-indent))
-                            (cons (make-defn indent name defn-pos defn-pos)
-                                  (loop (+ defn-pos (string-length tag-string)))))])))])
-        
-        ;; update end-pos's based on the start pos of the next defn
-        (unless (null? defs)
-          (let loop ([first (car defs)]
-                     [defs (cdr defs)])
-            (cond
-              [(null? defs) 
-               (set-defn-end-pos! first (send text last-position))]
-              [else (set-defn-end-pos! first (max (- (defn-start-pos (car defs)) 1)
-                                                  (defn-start-pos first)))
-                    (loop (car defs) (cdr defs))])))
-        
-        (when indent?
-          (for-each (λ (defn)
-                      (set-defn-name! defn
-                                      (string-append
-                                       (apply string
-                                              (vector->list
-                                               (make-vector 
-                                                (- (defn-indent defn) min-indent) #\space)))
-                                       (defn-name defn))))
-                    defs))
-        defs))
-    
-    ;; in-semicolon-comment: text number -> boolean
-    ;; returns #t if `define-start-pos' is in a semicolon comment and #f otherwise
-    (define (in-semicolon-comment? text define-start-pos)
-      (let* ([para (send text position-paragraph define-start-pos)]
-             [start (send text paragraph-start-position para)])
-        (let loop ([pos start])
-          (cond
-            [(pos . >= . define-start-pos) #f]
-            [(char=? #\; (send text get-character pos)) #t]
-            [else (loop (+ pos 1))]))))
-    
-    ;; get-defn-indent : text number -> number
-    ;; returns the amount to indent a particular definition
-    (define (get-defn-indent text pos)
-      (let* ([para (send text position-paragraph pos)]
-             [para-start (send text paragraph-start-position para #t)])
-        (let loop ([c-pos para-start]
-                   [offset 0])
-          (if (< c-pos pos)
-              (let ([char (send text get-character c-pos)])
-                (cond
-                  [(char=? char #\tab)
-                   (loop (+ c-pos 1) (+ offset (- 8 (modulo offset 8))))]
-                  [else
-                   (loop (+ c-pos 1) (+ offset 1))]))
-              offset))))
-    
-    ;; skip-to-whitespace/paren : text number -> number
-    ;; skips to the next parenthesis or whitespace after `pos', returns that position.
-    (define (skip-to-whitespace/paren text pos)
-      (let loop ([pos pos])
-        (if (>= pos (send text last-position))
-            (send text last-position)
-            (let ([char (send text get-character pos)])
-              (cond
-                [(or (char=? #\) char)
-                     (char=? #\( char)
-                     (char=? #\] char)
-                     (char=? #\[ char)
-                     (char-whitespace? char))
-                 pos]
-                [else (loop (+ pos 1))])))))
-    
-    ;; skip-whitespace/paren : text number -> number
-    ;; skips past any parenthesis or whitespace
-    (define (skip-whitespace/paren text pos)
-      (let loop ([pos pos])
-        (if (>= pos (send text last-position))
-            (send text last-position)
-            (let ([char (send text get-character pos)])
-              (cond
-                [(or (char=? #\) char)
-                     (char=? #\( char)
-                     (char=? #\] char)
-                     (char=? #\[ char)
-                     (char-whitespace? char))
-                 (loop (+ pos 1))]
-                [else pos])))))
-    
-    ;; get-defn-name : text number -> string
-    ;; returns the name of the definition starting at `define-pos'
-    (define (get-defn-name text define-pos)
-      (if (>= define-pos (send text last-position))
-          (string-constant end-of-buffer-define)
-          (let* ([start-pos (skip-whitespace/paren text (skip-to-whitespace/paren text define-pos))]
-                 [end-pos (skip-to-whitespace/paren text start-pos)])
-            (send text get-text start-pos end-pos))))
-    
     (define (set-box/f! b v) (when (box? b) (set-box! b v)))
-    
-    
-    
-    
-    
 
 ;                                        
 ;                                        
diff --git a/collects/tests/drracket/get-defs-test.rkt b/collects/tests/drracket/get-defs-test.rkt
new file mode 100644
index 0000000000..0abfad45fd
--- /dev/null
+++ b/collects/tests/drracket/get-defs-test.rkt
@@ -0,0 +1,54 @@
+#lang racket
+
+(require drracket/private/get-defs
+         racket/gui
+         string-constants)
+
+(define (get-definitions/string
+         string
+         #:define-prefix [define-prefix "(define"]
+         #:indent? [indent? #f])
+  (define text (new text%))
+  (send text insert (make-object string-snip% string))
+  (get-definitions define-prefix indent? text))
+
+(define-syntax (test-definitions stx)
+  (syntax-case stx ()
+    [(_ string (name ...))
+     #`(let ([actual (map defn-name (get-definitions/string string))]
+             [expected (list name ...)])
+         (unless (equal? actual expected)
+           (eprintf "Test failure at ~a\nActual: ~s\nExpected: ~s\n"
+                    #,(format "~a:~a:~a"
+                              (syntax-source #'stx)
+                              (syntax-line #'stx)
+                              (syntax-column #'stx))
+                    actual
+                    expected)))]))
+
+(test-definitions 
+ #<<END
+(define x 1)
+(define (f x)
+  (define y x)
+  y)
+(define y 2)
+(define
+END
+ ("x" "f" "y" "y" (string-constant end-of-buffer-define)))
+
+(test-definitions 
+ #<<END
+(define-metafunction L
+  f : p -> q
+  [(f p) t])
+(define-metafunction L
+  [(g p) t])
+(define-metafunction/extension f L
+  h : p -> q
+  [(h p) t])
+(define-metafunction/extension f L
+  [(i p) t])
+(define-metafunction
+END
+ ("f" "g" "h" "i" (string-constant end-of-buffer-define)))
\ No newline at end of file