       "Remove trailing whitespace from STRING."
       (if (string-match "[ \t\n\r]+\\'" string)
           (replace-match "" t t string)
-        string))
-    (defsubst string-trim (string)
-      "Remove leading and trailing whitespace from STRING."
-      (string-trim-left (string-trim-right string)))))
+        string))))
+
+(defun fstar--string-trim (s)
+  "Trim S, or return nil if nil."
+  (when s (string-trim-left (string-trim-right s))))
 
 ;;; Group
 

            (fstar-subp--column-number-at-pos pos))))

(defconst fstar-subp--info-response-regex
  "^(defined at \\(.+?\\)(\\([0-9]+\\),\\([0-9]+\\)-\\([0-9]+\\),\\([0-9]+\\)))")

(cl-defstruct fstar-pos-info
  source-file def-start def-end type)

(defun fstar-subp--info-continuation (continuation pos success response)
  "Handle the results (SUCCESS and RESPONSE) of an #info query at POS.
If response is valid, forward results to CONTINUATION.  With nil
POS, this function can also handle results of position-less #info queries."
  (if (and success
           (or (null pos) (eq (point) pos)) ;; Point didn't move since request
           (string-match fstar-subp--info-response-regex response))
      (funcall continuation
               (make-fstar-pos-info
                :source-file (match-string 1 response)
                :def-start (cons (string-to-number (match-string 2 response))
                                 (string-to-number (match-string 3 response)))
                :def-end (cons (string-to-number (match-string 4 response))
                               (string-to-number (match-string 5 response)))
                :type (string-trim (substring response (match-end 0)))))
    (funcall continuation nil)))

(defun fstar--eldoc-continuation (continuation info)
  "Pass highlighted type information from INFO to CONTINUATION."
  (when info
    (funcall continuation (fstar-highlight-string (fstar-pos-info-type info)))))

(defun fstar--eldoc-function ()
  "Compute an eldoc string for current point.

  (when (fboundp 'advice-remove)
    (advice-remove 'eldoc-message #'fstar--eldoc-truncate-message)))

;;;; Doc at point

(defun fstar--doc-at-point-continuation (info)
  "Show documentation in INFO."
  (-if-let* ((doc (and info (fstar-symbol-info-doc info))))
      (with-help-window "*fstar-doc*"
        (princ doc))
    (message
     (substitute-command-keys
      (concat "No documentation found. "
              "Try visiting the source file with \\[fstar-jump-to-definition]")))))

(defun fstar-doc-at-point ()
  "Show documentation of identifier at point, if any."
  (interactive)
  (fstar-subp--ensure-available #'user-error)
  (unless fstar-compat--can-use-info
    (user-error "This feature isn't available in F* < 0.9.4.1"))
  (fstar-subp--query (fstar-subp--positional-info-query (point))
                (apply-partially #'fstar-subp--info-continuation
                                 #'fstar--doc-at-point-continuation
                                 (point))))

;;;; xref-like features

(defun fstar--save-point ()
