Close the .glob file after having saved .vo

This is a no op for standard Coq, but is important for
Paral-ITP, since saving the library to disk forces all
frozen computations, and some of them may spit out glob
data, so the file descriptor must be valid.
Ideutils: comment on missing Glib utf8 handling function
States: frozen states can hold closures

States.freeze takes ~marshallable:bool, so that (only) when we want to
marshal data to disk/network we can ask the freeze functions of the
summary to force lazy values.  The flag is propagated to Lib and Summary.
Summary: support selective freeze

One can freeze/unfreeze a portion of the summary.
New module Xml_printer (dual to Xml_parser)

Code for printing XML moved from xml_utils.ml to xml_printer.ml
and improved to generate less garbage using Buffer.t systematically.
Coqide: view -> zoom in / out / fit

This commit adds zoom facilities that are useful for demos (quickly
increate font size) and daily use (set size so that 80 colums fit
the window width).
Side effect free implementation of admit (Isabelle's oracle)

new Axiom in Logic.v,  proof_admitted : False.

admit now simply cases proof_admitted and does
not create a new Axiom in the environment.
Add future library to represent pure computations

Since the whole system is imperative, futures are run protecting
the global state, and the final state is also saved to let the user
freely chain futures. For now their evaluation semantics is the one of
lazy_t.
State Transaction Machine

This is the work described in the Coq Workshop 2012 paper.
The interp function just populates a graph of transaction, then one
can observe a node in the graph forcing its evaluation.
When possible proofs (branches of the graph) are stocked inside
futures, thus the node corresponding to Qed can be reached without
executing the proof script. The environment thus may hold proof promises
(instead of proof objects) for some theorems, and bad promises
are discovered only joining the safe environment.
Imperative modifications to the environment made by some tactics are
now explicitly declared by the tactic and modeled as let-in/beta-redexes
at the root of the proof term. An examples are abstract tactic.
theories/ hacked to make STM compile the whole library

Problems:
1) Ltac _parsing_ seems to trigger globalization, so we force the
   execution of the previous states by hand in the scripts with 'Join.'
2) Some tactic declarations have been reworded putting Local in front
   (not really needed)
3) An occurrence of ring seems to diverge, commented out.
4) Detection of Module with parameters (a command that must be executed
   immediately (classification as VtNow) since it changes the grammar
   is incomplete, explitic 'Join.' added instead
Searchable stack data structure for Coqide
Coqide ported to STM (CHECK COMMENT)

Main changes for STM:
1) protocol/serialization implementation with much less copy/paste
2) protocol changed to carry state ids
3) colouring reflects the actual status of every span (evaluated or not)
4) button to force the evaluation of the whole buffer
5) cmd_stack and backtracking completely changed to use state numbers
   instead of counting sentences

Collateral changes:
1) Coq_lex now identifies sentences and comments in a precise way,
   and corresponding tags are set in the text_buffer
2) Finding sentences, re-lexing on user action, relocating the caret
   adjusted to the new lexing/tagging
3) Unjustified zapped away but still doable
4) Less copy/paste in tags et similia
5) coqtop/handle locking mechanism improved to "allow" recursive locking
6) tentative Emacs/PG mode