@@ -166,13 +166,14 @@ sexpToCommand (SexpList [SymbolAtom "add-clause", IntegerAtom line, StringAtom n
166sexpToCommand (SexpList [SymbolAtom "add-proof-clause", IntegerAtom line, StringAtom name]) = Just (AddProofClause (fromInteger line) name)
166sexpToCommand (SexpList [SymbolAtom "add-proof-clause", IntegerAtom line, StringAtom name]) = Just (AddProofClause (fromInteger line) name)
167sexpToCommand (SexpList [SymbolAtom "add-missing", IntegerAtom line, StringAtom name]) = Just (AddMissing (fromInteger line) name)
167sexpToCommand (SexpList [SymbolAtom "add-missing", IntegerAtom line, StringAtom name]) = Just (AddMissing (fromInteger line) name)
168sexpToCommand (SexpList [SymbolAtom "make-with", IntegerAtom line, StringAtom name]) = Just (MakeWithBlock (fromInteger line) name)
168sexpToCommand (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"
170-- If it's False, that means "refine", i.e. apply the name and fill in any
170-- If it's False, that means "refine", i.e. apply the name and fill in any
171-- arguments which can be done by unification.
171-- arguments which can be done by unification.
172sexpToCommand (SexpList [SymbolAtom "proof-search", IntegerAtom line, StringAtom name, SexpList hintexp]) | Just hints <- getHints hintexp = Just (ProofSearch True (fromInteger line) name hints)
172sexpToCommand (SexpList [SymbolAtom "proof-search", IntegerAtom line, StringAtom name, SexpList hintexp]) | Just hints <- getHints hintexp = Just (ProofSearch True (fromInteger line) name hints)
173 where getHints = mapM (\h -> case h of
173 where getHints = mapM (\h -> case h of
174 StringAtom s -> Just s
174 StringAtom s -> Just s
175 _ -> Nothing)
175 _ -> Nothing)
176+sexpToCommand (SexpList [SymbolAtom "refine", IntegerAtom line, StringAtom name, StringAtom hint]) = Just (ProofSearch False (fromInteger line) name [hint])
176sexpToCommand (SexpList [SymbolAtom "docs-for", StringAtom name]) = Just (DocsFor name)
177sexpToCommand (SexpList [SymbolAtom "docs-for", StringAtom name]) = Just (DocsFor name)
177sexpToCommand (SexpList [SymbolAtom "apropos", StringAtom search]) = Just (Apropos search)
178sexpToCommand (SexpList [SymbolAtom "apropos", StringAtom search]) = Just (Apropos search)
178sexpToCommand (SymbolAtom "get-options") = Just GetOpts
179sexpToCommand (SymbolAtom "get-options") = Just GetOpts