There are two excellent choices for implementing prediction markets:
(1) Use book orders that stand until filled, just as intrade.com does.
(2) Use an automated market maker (like Robin Hanson's) that stands ready to make trades.
The book orders model is very simple to implement, but can suffer from very wide Bid/Ask spreads. And, it can be tough to bet people to book orders that may never get filled.
Hanson's market maker, on the other hand, supports instant trades for anybody. The downside of automated market makers are two-fold: they often require a fair bit of sophisticated math, and they can lose (a bounded amount of) money. See http://blog.oddhead.com/2006/10/30/implementing-hansons-market-maker/
You can use book orders and a market-maker together, but it complicates some things. Hanson's market maker moves the prices continuously which makes things a little funny when you hit the price of a standing book order.
Pennock also has one or two market makers, but Hanson's is the only one that I'm well-versed in. I don't know if Pennock's market makers have fixed loss like Hanson's.
Short selling relies on the notion of borrowing shares, which is outside the scope of most prediction markets. When you have a market maker, you can always purchase the securities that represent the opposite outcome to the one you wanted to short, so there's really no need to short sell---another advantage to having a market maker.