MQueryInterpreter: interface updated

freeze() & thaw() method put around "freeze() ; push('$')" to avoid
rendering of a TML document which is not in math mode.

patch

- New interface for the MathQL interpreter (1.3 version)
- Two toplevels committed in ocaml/mathql_test (new directory)

New queries added:
 * Locate Inductive Principle
 * Match Conclusion (previously it was just a synonim for SearchPattern)

The two lexers now raise CicTextualParser0.LexerFailure instead of
Failure "int_of_string". Easier to catch.

* "Invalid UWOBO Server" ==> "Untrusted UWOBO Server"
* Added mowgli.cs.unibo.it to the list of trusted UWOBO servers.

* topurl was re-declared and used with two different meanings ==> renamed
  the first occurrence into interface_topurl
* the r.e. that extract the topurl from the URL has been fixed

1. param.name=value parameters added to the getpage method
2. index.html modified to use all the param.name parameters

Added preprocess feature to "getpage" method. Using this feature you can
fill "@processorURL@" 'holes' in .html javascript pages.

The processorURL parameter must now be instantiated by the searchEngine.
(i.e. index.html is now a template to be filled in before returning it to
 the browser)

* Hbugs interface clean-up.
* Moved every Hbugs.notify invocation into the refresh_proof function
* Added a Hbugs.clear

* Removed several  try .... with _ -> (which make thread killing impossible ;-((
* The CicTypeChecker module now uses just a single TypeCheckerFailure exception

Removed several  try .... with _ -> (which make thread killing impossible ;-((

catch only PXP exceptions in xml_document to avoid thread breakage

1) fromdos on any html/* file
2) added a new method ask_uwobo to copy to the user a document that is
   asked to UWOBO (i.e. given a URL, it checks that it is a request to
   a trusted server)
3) templateambipdq?.html changed in such a way that no character that needs
   XML escaping happears. In this way we can apply stylesheets on them and
   what we get is valid HTML + JavaScript
4) All the functions that used to print the result as ASCII have been changed
   to generate an HELM Theory File.
5) The JavaScript code now asks the searchEngine to ask_uwobo an URL that
   is obtained by asking UWOBO to apply the stylesheets from theory files to
   HTML. The UWOBO URL (and parameters) are now hard-coded in JavaScript ;-((

As a result, we now have a very pretty rendering of the results. The
hyperlinks are enabled and fully working. Well done!

- no more CSCisms for MathML editor: now use mathml editor debian and
  findlib package

We have a big architectural problem here: the Hbugs hints when applied
may have an argument which is a term (now in textual form). Depending on the
current parser in use, the syntax for the textual form must be TeX or
ASCII art. Which one is the right one? The current momentary patch activates
the TeX syntax.

Underscore must be quted in TeX. Fixed.

I now register the gdome2-xslt call-back functions for error processing.
They print the error/warning messages in the HTML debug windows.

'{' and '}' are now considered as blanks

1. internal links fixed
2. title added

NEW: manual added and linked to the interface.

Added an hyperlink to the on-line manual.

* New release of the client-side interface.
* Closes the following bug: if an ambiguous query (with more than one
  ambiguous term) was issued twice and all the aliases were cleaned
  between the two queries, disambiguation was not asked to the user
  for each ambiguous term but the first one.

Ooopps. I forgot this one.

CVS repository fix: reversion of some lines (related to libhttp) to a working
version.

Pending changes on the checked-out repository committed. Ask Zack for
the changelog ;-)

Pending changes in the checked-out repository committed. Ask Zack for
the changelong ;-)

Partial upgrade to the new disambiguating lexer/parser.

First committed version that (may) use the MathML editor to enter formulas.

...

First committed version of the textual parser able to parse TeX syntax.
(This should be the second release of the parser, but the first one was
never committed.)

First commit towards more powerful disambiguation possibilities, where
an expression can be disambiguated yelding totally different terms.
Required, for example, to disambiguate operators that have interpretations
with a different arity (as Leibniz equality and the decidable equality over
natural numbers).

Comment fixed.

Bug introduced: the alias combo-box now accepts multiple selections (but
use just the last selected item).

A dialog box is now opened when Restart is pushed while composing a query.

Bug fixed: all the pages were not asked to the daemon ==> all the hyperlinks
were broken.

Many changes in the client-side interfaces:
 1. Bug fix: after a SearchPattern query it was impossible to interact
    any more with the "alias" editor. The problem was that the JavaScript
    code assumed the existence of a parent frame that is not always there.
    Closes #24
 2. New release of the client-side interface with some bug fixes in the
    grammar production

Big change: parenthesis can now be put in any place to disambiguate the
expression. The case "(expr) -> expr" is no more an exception. An application
node is generated iff more than one expression is put inside the parenthesis.

added .cvsignore

- parse postgres connection string also from environment variable
- solved some compatibility issues with MathQL
- use old Misc functions from MQueryMisc

- use new mquery generator module
- no longer use mQuery* stuff from ../gTopLevel

added META.helm-mquery_generator

minimal changes:
- added a TODO comment
- factorized some code
- removed old useless debugging prints

build bytecode code by default

build also mquery_generator module

added dep on helm-mquery_generator

added TacticChaser module to emebed functions which search set of
tactics which can be applied

defined an explicit "status" type

moved mquery generation stuff in a new module

- added HBugs support
- switched to multi threaded implementation
- fixed references from Misc to MQueryMisc module
- moved search pattern apply in ../ocaml/tactics/tacticChaser.ml*

- added HBugs notification after tactic application
- bugfix: removed some useless status save
- defined module type "Tactics", module type returned by Make functor

- added dependencies on hbugs-client, threads, helm-mquery_generator
- build using -thread switch

moved mquery generation in ../ocaml/mquery_generator/

- added and exposed get_current_status_as_xml
- removed apply_tactic and can_apply_tactic

- moved exception IllFormedUri, string_of_cic_textual_parser_uri,
  cic_textual_parser_uri_of_string,
  wrong_xpointer_format_from_wrong_xpointer_format' to MQueryMisc
- moved here strip_xml_headings from gTopLevel.ml

fixed references to functions moved from Misc to MQueryMisc

added HBugs interface module for gTopLevel

rebuilt

removed tmp_dir no longer needed (it was used only by ClientHTTP module)

bugfix: use temporary file name to avoid file access clashes when the
same teporary dir is used by many processes

- added pp_to_outchan and pp_to_string for other medium pretty printing
- factorized implementation of pretty printers so that it's used by all
  pretty printing functions

Makefile patched

Makefile.common.in and .depend backtracked to my last commit (before the
ones of Ferruccio) and then modified. Dependencies between a file and a
library are now handled correctly.

packege dependences calculation patched

package dependences calulation fixed

SQL quoting fixed in relation.ml

Added new module DiscriminationTactics

Added buttons for new tactics Injection and Discriminate

Added module DiscriminationTactics with brand new tactics Injection and
Discriminate, both working only in simple situation

patches for the new interface of text_of_query/text_of result

new interface for text_of_query/text_of_result + bug fixes

Dependency simplification.

Minor module re-organization:
1. SequentPp is now no more dependent from proofEngine
2. the functions to apply stylesheets from DOM documents to DOM documents
   are not any longer exported by ApplyStylesheets

...

The scratch window is now based on the sequent_viewer widget.

Major module reorganization:
- new module TermViewer: holds widgets to render and interact with sequents
  and proofs at the CIC level
- new module ApplyStylesheets: functions to apply stylesheets and map
  terms and sequents to MathML Presentation
- new module InvokeTactics: it is a functor that gives back a module that
  defines one callback function for every tactic

1. helmns and domImpl moved to the misc module ;-(
2. all the constants and functions relative to stylesheet applications have
   been moved to the new module ApplyStylesheets, whose interface is really
   minimal.

Minor code reorganization:
 1. several functions unrelated do disambiguation moved from Disambiguate
    do Misc.
 2. TermEditor module added. It implements a widget for entering terms.
    The widget is also responsible for the disambiguation.
 3. TermEditor is now the only widget that uses the Disambiguate module.

Tactics button rearranged.

Clear and ClearBody moved to the pop-up menu.
No check is done so far to avoid activating them when the selected "term"
is not an hypothesis.

replace_lifting generalized to the simultaneous replacement of n terms.

ProofEngineHelpers.mk_fresh_name now used in place of "dummy_for_rewrite".

1. Added a callback to the generalize tactic to generate a fresh name.
2. Dead code removal in various files.

Added a callback to the generalize tactic to generate a fresh name.

Generalize now works on a list of convertible terms, generalizing all of
them at once.

Generalize tactic moved to the contextual menu.

New: we now have a new pop-up menu for the reduction tactics.

1.  All the reduction tactics have been modified to reduce several (sub)terms
    at once.
2.  To reduce several (sub)terms at once you can use the new multiple
    selection feature.

All the reduction tactics have been modified to reduce several (sub)terms
at once.

Multiple selection is now enabled in the goal and check windows.
All the tactics still behave as before.

maction toggle restored

Optional callbacks have been added to tactics that need to introduce
new fresh names directly (i.e. without calling other tactics that need
fresh names). The default behaviour is _MUCH_ nicer than the previous
dummy one and is fully functional.

Corollary 1: all the code of tactics.cma is now reentrant.
Corollary 2: the user can be asked the fresh name if it is requested
             by a top-level tactic.

Dead code removed.

Decompose now has a new parameter which is the callback to call to select the
uris that must be used for the decomposition.

Decompose now has a new parameter that is the callback function to call
to select the uris that must be decomposed.

Fixed. It was no more working since the move of the tactics under the ocaml
repository.

added META for module helm-tactics

moved tactics from gTopLevel to the new module ocaml/tactics