New dictionary created to handle special syntax for CIC.
So far the following macros have been added:
\Prop
\Set
\Type
They are now rendered as Prop, Set and Type (in non-italic font).
Interface change: the get_as_string and set_term methods of the term-editors
now work on an unquoted string: the string is TeX quoted (i.e. '$' are
inserted at the beginning and end and '_' are quoted) by set_term and
unquoted by get_as_string. This solves in an almost clean way the
problem of hbugs (that had to quote the string). The solution is maybe still
partial since it is not always possible to serialize/deserialize the input
to a string. An improvement (???) would be to make the output type of
get_as_string opaque and provide two set_term: the first one's input would
be the opaque data type and the second one would be a CIC term.
* 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
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)
* Removed several try .... with _ -> (which make thread killing impossible ;-((
* The CicTypeChecker module now uses just a single TypeCheckerFailure exception
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!
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.
* 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.
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).
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.
- parse postgres connection string also from environment variable
- solved some compatibility issues with MathQL
- use old Misc functions from MQueryMisc
- 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
- 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
- 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.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.
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
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.
projects / helm.git / log