@@ -166,13 +166,14 @@ sexpToCommand (SexpList [SymbolAtom "add-clause", IntegerAtom line, StringAtom n
166166sexpToCommand (SexpList [SymbolAtom "add-proof-clause", IntegerAtom line, StringAtom name]) = Just (AddProofClause (fromInteger line) name)
167167sexpToCommand (SexpList [SymbolAtom "add-missing", IntegerAtom line, StringAtom name]) = Just (AddMissing (fromInteger line) name)
168168sexpToCommand (SexpList [SymbolAtom "make-with", IntegerAtom line, StringAtom name]) = Just (MakeWithBlock (fromInteger line) name)
169−-- XXX: The Boolean in ProofSearch means "search recursively"
169+-- The Boolean in ProofSearch means "search recursively"
170170-- If it's False, that means "refine", i.e. apply the name and fill in any
171171-- arguments which can be done by unification.
172172sexpToCommand (SexpList [SymbolAtom "proof-search", IntegerAtom line, StringAtom name, SexpList hintexp]) | Just hints <- getHints hintexp = Just (ProofSearch True (fromInteger line) name hints)
173173 where getHints = mapM (\h -> case h of
174174 StringAtom s -> Just s
175175 _ -> Nothing)
176+sexpToCommand (SexpList [SymbolAtom "refine", IntegerAtom line, StringAtom name, StringAtom hint]) = Just (ProofSearch False (fromInteger line) name [hint])
176177sexpToCommand (SexpList [SymbolAtom "docs-for", StringAtom name]) = Just (DocsFor name)
177178sexpToCommand (SexpList [SymbolAtom "apropos", StringAtom search]) = Just (Apropos search)
178179sexpToCommand (SymbolAtom "get-options") = Just GetOpts