...

workaround for an assertion failure during rendering (missing sort of some ids)

removed orders_op from library (now in le_arith and lt_arith).

...

This commit re-commits version 1.61, removing the error (a "." in a regular
expression that did not match "\n").

REVERT OF MY PREVIOUS COMMIT THAT INTRODUCES A CRITICAL BUG (some lines
are automatically _removed_ from the script). I will commit again as soon
as I fix the bug.

Committing all the recent development of Andrea after the merge between his
commits and my recent commits (that added notation here and there).

More notation.

Management of automatic insertion of aliases and "goal" commands reimplemented
almost from scratch. The new commands inserted are now distinct entities in
the history. As a consequence going up in the script is now a step by step
operation and going up and going down are invertible operations, as they
should be.

Code simplification.

Bug fixed: added a _undoable_action critical section to the reset method of
MatitaScript.script to avoid a Gtk assertion failure.

dead code removed

fixed matitamake to handle development with names with spaces
the engine now has 2 different exception to report 2 diffrent problems:
- UnableToInclude
- IncluedFileNotCompiled

refactored gui handling code so that MatitaMathView is linked before MatitaGui
and all callback registrations happen in matitaGui.ml rather than matita.ml

...

matitaMisc.ml

safe mkdir implemented

proof of concept implementation of cut and paste from gtkMathView to text
(still via debug menu item "print selected terms")

renamed development related windows

added #proofConclusion

cosmetic changes

added get_proof_conclusione and list_tl_at

highlighted notation keywords

...

fixed cic_notation dependencies

better boxes (with more line breaking hints) for objects rendering

*** empty log message ***

bugfix: added xref on ast built via pattern matching from cic (3 -> 2)

added id_of_annterm: Cic.annterm -> Cic.id

bugfix: no more xref on bound names

added low level rendering attributes (indent, spacing, ...)

rendering from markup to string

improved debugging pretty printing of xref

"Coq's " prefix added to every interpretation.

Flickering bug fixed.

locate_in_term generalized to locate_in_conjecture

Comments added.

Bug solved: the #reparent method of Gtk should NOT be used:
see http://www.gtk.org/faq/#AEN636.
This solves the flickering problem that occurred when a new tab was selected.

Implementation of locate_in finished.

typo s/\\OF/\\of/

fixed typo in helpers for generating hv and hov boxes

draft version of locate_in_term

...

unreleased version of the bindings, with more gtkmathview method bounds and dependencies on gmetadom 0.2.3

...

**** Experimental: ****

After the disambiguation, if the term is no longer ambiguous, we forget the
environment. In this way we are forced to do more work later (since we have
less aliases), but we have more freedom (since we have less aliases) in the
future disambiguations.

typo fixed

"Coq's " prefix added to every interpretation.

Bug fixed: list_uniq o List.sort used in the lookup function to return only
one interpretation in case of duplicate interpretation definitions. This
happens when a module A defines an interpretation, it is included by B and
C and then a module D includes both B and C, thus defining the interpretation
twice.

bigger disambiguate chiuches win

...

More notation (up to where the open bugs allow me to put it without adding
too many aliases).

A little bit more of notation here and there.

some more changes and corrections

Notation for equality used everywhere.

Note: due to a bug in the notation machinery, the declaration of the notation
is a bit cumbersome (it uses a URI and an alias; it should use no alias and
just eq in place of the URI). To be fixed.

...

Bug solved: X-style paste (i.e. paste of the PRIMARY selection using the
second mouse button) used to paste locked text as locked text.

paramodulation added.

Highlighting of parse errors implemented.

Code simplification.

Bug fixed: the _advance method must delete the parsed text iff it was parsed
from the script itself (calling the getFuture method).

...

1. select_all added to the Edit menu; no shortcut for it (since the standard
   one (Ctr+A) hides the Emacs-like binding "go to beginning of line")
2. added a few standard but missing shortcuts (Ctr-N for a new document,
   Shift+Ctr+S for save as)

The edit menu items (copy/cut/delete/paste) are now sensitive to the
selection/existence of textual data in the clipboard.

- MatitaLog output redirected to stderr for every message <> Message
- matitadep gracefully recovers from the inclusion of a non-existent .ma file

building/cleaning a devel now makes buttons insensitive

...

merged transformations on top of notation code

handle multiple href

added split

implemented transformations on top of notation code

moved add_xml_declaration here

- addded unicode_of_tex
- added \neq macro

Paramodulation initialized.

...

added optional "paramodulation" parameter to auto to turn on paramodulation

added optional "paramodulation" parameter to auto to turn on paramodulation

- better exception handling
- compiled with -pack to get a Paramodulation namespace
- fixed a bug in Inference.unification_simple

When matita is started on a non-existent file, it avoids creating it
immediately!

Original semantics of a now almost random piece of code restored.
Fixes the automatic compilation of .moos when matita is started from a directory
that is not the root of a library.

An object should be removed from disk (i.e. from the Getter scope) _before_ removing it
from the environment.

CicEnvironment.remove did not remove the object from the unchecked_list.

fix

Removed debugging print.

matitaclean all now destroys the .matita/xml directory

Big changes:
 1. the .moo files are now kept in the logical structure (i.e. in .matita/xml/*)
 2. matitaclean is now able to correctly remove all the .moo files
 3. the compilation target in library and tests is now foo.mo (it used to be
    foo.moo) and it is PHONY

add_obj is ATOMIC

some prerr to better understand the mkdir -p error

added env content debug print

...

added some typechecks to avoid using equations with the wrong type

dependencies

removed .depend from .cvsignore

added some typechecks to avoid using equations with the wrong type

added CicNotation.load_notation call to disambiguate terms

if paramodulation fails, go on with the normal auto...

Bug fixed: LICENSE and AUTHORS were searched in the current dir :-(

...

Regression fixed: goto used to stop (again!) to the new cursor position when
the user clicks somewhere. The source of the regression was the difficulty of
remembering the position of the marks while the text is modified (by automatic
insertion of aliases). Solved by using ad-hoc temporary marks in place of
iterators (first version tried) and offsets (most recent version tried).

...