code simplification

Code clean up.

Dead code removed.

More code clean-up.

Useless code removed; interfaces simplified; etc.

1. reset of statuses simplified
2. NCicEnvironment.invalidate_all (that used to hide a bug in invalidation)
   removed. The semantics of the MTI is now more shacky, but this needs to be
   fixed in other ways.
3. {lexicon_,grafite_,...}status renamed into status

Some comments (new problems found).

Really A LOT of code to add close buttons to the tab labels :-(

Bug fixed (introduced in previous commit): opening multiple files requires first
the creation of the newScript to be replaced.

Implemented standard semantics of Load in MTI: loading a file when the current
one is unnamed and not modified does not open a new tab.

1. MatitaGuiTypes.gui interface streamlined
2. added new menu item to close a script
3. restored graying of "Save" menu item when the script is unnamed

Avoid duplicates in the list.

1. bug fixed: in the last commit on NCicLibrary we forgot that
   get_already_included must be transitively closed; fixed and changed
   the function name
2. added a cache to assert_ng (called ~asserted) to avoid re-asserting
   the same file twice during a single include command

1. bug in addition of universe constraints fixed: the recursive
   inclusion does not add constraints to the NCicLibrary.storage
2. since we no longer perform recursive cleaning,
   NCicEnvironment.invalidate_item is no longer recursive. This fixed
   definitely the bugs in undo/redo linked to "include"s

progress

more theory for lists

...

Useless code removed.

Dead and useless code removed.

Dead code removed.

When switching to a new script, the other parts of the interface are
now notified.

...

VERY EXPERIMENTAL:

first version of Matita as a Tabbed Document Interface.

The semantics of working on two tabs at the same time is not defined
(yet? ...)

...

Code clean-up

Large commit: refactoring of the code of the interface.

1. management of font sizes centralized in MatitaMisc according to the
   MVC paradigm
2. functionalities related to the script window moved from MatitaGui to
   MatitaScript

First steps towards a multi-document interface.

Class mathViewer got rid of. The circular dependency between
the scripts needs to be sorted out by putting matitaScript much
later in the chain. This commit temporary introduces bad type
expressions here and there.

1. Method screenshot moved to CicMathView where it belongs to.
2. the mutual dependency between MatitaScript and CicMathView/MatitaMathView
   needs to be solved differently (it used to be solved using guistuff, which
   I do not consider any longer a good solution). To be done.

With this commit, anything related to MathML vs Textual is now in
cicMathView.ml.

Useless methods removed.

1) matitaMathView.ml splitted into cicMathView.ml + matitaMathView.ml
2) interface of matitaMathView.ml and cicMathView.ml greatly simplifed
   so to avoid any reference to the textual/MathML datatypes.
3) up to the problem of taking screenshots, the file matitaMathView.ml
   is now oblivious of the difference between text and MathML. It will
   be soon possible to switch between text and MathML simply by changing
   the implementation of cicMathView.

Better typing.

Now useless type declaration removed.

This commit simplifies the interfaces of the various Widget-related .mli
files, so that the same inferfaces can be used both for the MathMl widget and
the textual widget.

Practically, it is now sufficient to switch between two implementations of
matitaMathView to change between MathML/textual.

Large commit:

1) some dead code removed
2) code of MatitaClean commented out (but still there for disambiguation and
   the like?)
3) dependencies and uris moved into dumpable_status (from other statuses
   and/or imperative code) and made functional
4) all the bugs related to recursive compilation seem to have been fixed by 3)

New version of the library. Several files still do not compile.

Some bugs fixed (and some still open) in recursive compilation of files:
 a) matitac now takes again either a list of files to be compiled or
    nothing (to compile all files in the cwd)
 b) ...

Bug fixed: a file A that includes a file B needs to be recompiled also
when B has been compiled after A.

Dead code removed.

Previous patch improved: we now use an ad-hoc wrapper for Grammar.parsable
in order to localize all Obj.magic --- related to use of Ulexing in Camlp5 ---
in GrafiteParser (as they used to be).

Debugging code removed.

Dead code removed.

BIG BUG FIXED (???): in place of using Grammar.Entry.parse we should have
used from the beginning Grammar.Entry.parse_parsable in order to avoid token
loss (because of backtracking) between consecutive reads. I have fixed the issue
for statements only (since they are the one that show the problem). Should I
do the same everywhere?

Backporting from new Matita:

Patch to avoid double creation of metavariables changed to a simpler one
that keeps disambiguating twice the term. The old patch introduced a few
bugs that were difficult to fix.

Notation for - (clear).

Big change:
 - new command "include alias" to include only the aliases
 - "include" now always includes the aliases and it includes everything else
   only if the file has not been already included

New syntax -H1 .. Hn for clear

Patch to avoid double creation of metavariables changed to a simpler one
that keeps disambiguating twice the term. The old patch introduced a few
bugs that were difficult to fix.

exp and factorial

some progress

Semantics of try changed (fixed) when applied to multiple goals that can now
fail independently.

Back-portin from new Matita: semantics of ntry changed (fixed?) when applied
to multiple goals.

Back-porting from new Matita: improvement to inferred type.

first commit for Helena 0.8.2
autCrg: we removed the computation of the de Bruijn degree
output: we renamed some reductions to reflect the latest terminology
brgSubstitution: icm related bugfix

It is now possible to pass a ${ident x} to another previously defined
notation that expects an ${ident y}.

[ porting from CerCo's Matita ]
1. new implementation of normalize to have a speed up in case of fully applicative terms
2. all reduction tactics used to end with instatiate that re-checked the conversion using
   unification (!!!); added a new flag ?(refine=true) to instantiate to avoid this expensive
   check when we know it is useless

Bad default for ?dorefine for instantiate

1. new implementation of normalize to have a speed up in case of fully applicative terms
2. all reduction tactics used to end with instatiate that re-checked the conversion using
   unification (!!!); added a new flag ?(refine=false) to instantiate to avoid this expensive
   check when we know it is useless

porting to new syntax

Bug fixed: propagation of left expected parameters is now working correctly also
in case of \ldots.

Bug fixed: propagation of left expected parameters is now working correctly also
in case of \ldots.

In the case type_of constructor with expected type T, T is now put in whd to
find an expected inductive type.

In the case type_of constructor with expected type T, T is now put in whd to
find an expected inductive type.

Back-porting from new Matita:

Invariant dropped: NotationPt.NCic t can now contain metas.
We do not know if the invariant was exploited somewhere...

Back-porting from new Matita:

Propagation of left expected parameters in typeof.

Back-porting from new Matita:

- GREAT: when unifying ?1 : Type[i]  with ?2: Type[j] the unifier
  randomly tried to instantiate ?1 with ?2 even when j > i, yielding to
  an unification error later on. In turn, this created that horrible
  behaviour of rewriting that failed if you did not pass enough types
  to the lemma.
- in rewriting the argument is now automatically saturated

These two fixes together allow most of the time to write simply >f as we
did in the old system.

Back-porting from new matita:

New behaviour of fo_unif: in case of  ?f args == t args'
where at least one args is flexible, it now unifies in parallel even if the
two args have different lenghts (as in the old version of Matita).

Back-porting from new Matita:

- GREAT: when unifying ?1 : Type[i]  with ?2: Type[j] the unifier
  randomly tried to instantiate ?1 with ?2 even when j > i, yielding to
  an unification error later on. In turn, this created that horrible
  behaviour of rewriting that failed if you did not pass enough types
  to the lemma.
- in rewriting the argument is now automatically saturated

These two fixes together allow most of the time to write simply >f as we
did in the old system.

Back-porting from new Matita:

Bug fixed: analysing inductive type that contains implicit used to
duplicate the metas in the metasenv since the term was disambiguated
twice, in the analyze and in the tactic that uses the analyze.

Propagation of left expected parameters in typeof.

- GREAT: when unifying ?1 : Type[i]  with ?2: Type[j] the unifier
  randomly tried to instantiate ?1 with ?2 even when j > i, yielding to
  an unification error later on. In turn, this created that horrible
  behaviour of rewriting that failed if you did not pass enough types
  to the lemma.
- in rewriting the argument is now automatically saturated

These two fixes together allow most of the time to write simply >f as we
did in the old system.

New behaviour of fo_unif: in case of  ?f args == t args'
where at least one args is flexible, it now unifies in parallel even if the
two args have different lenghts (as in the old version of Matita).

Debugging code commented out.

Debugging code commented out.

Debugging code commented out.

Small improvement: check now takes the context of the first focused
goal, if any.

Some arithmetics.

- lddl html pages: the transition to xhtml 1.1 + css 2 is complete
- helena: we made a 88 x 32 label for the Web

Implementation of proof irrelevance finished.

Debugging disabled

- auto now uses the equality of the new library

- dead code removed

- number notation ported to new library
- code for number notation made less general by hard-coding the only
  notation

Number notation ported to new library.

Invariant dropped: NotationPt.NCic t can now contain metas.
We do not know if the invariant was exploited somewhere...

Bug fixed: analysing inductive type that contains implicit used to
duplicate the metas in the metasenv since the term was disambiguated
twice, in the analyze and in the tactic that uses the analyze.

we updated the css validation icon

we are migrating the static htnl pagest to html 4 to xhtml 1.1 + css

- stock icons restored
- hbugs got rid of definitely

1) matita.glade ported from glade2 to glade3
2) added a workaround (using xmlling) to convert &#x....; chars generated
   by glade3 into unicode symbols to avoid a corresponding lexing bug in
   lablgladecc2 :-(

let and let rec used wrong tokens

Big bug fixed: grafiteDisambiguate.add_aliases_for_objects used to add
aliases to the status, but not to the .ng.

Fixed, but we probably need a better approach where the addition to the
.ng is performed by the single modules, and not in grafiteEngine as it
is now.

Bug fixed: an assert false was raised before giving the first interpretation.

- bug fixed: fullpath used in place of relative path

- bug fixed: circular dependencies are now detected correctly

now implemented in matitaEngine.ml

Huge change!!!

- matitadep & co removed (RIP)
- both matita and matitac can now recursively compile files as needed
- librarian greatly simplified: now it only handles roots

Probably many bugs left.

- better names, interface simplified

- cleanup

- matitacLib merged into matitaEngine