Carsten:
paper

to do
omitted codomain defaults to current signature (nice to use toplevel views as realizations)
permit shadowing of constant names on toplevel
forbid *+- as module identifiers
bug: it's possible to change the fixity of a constant in an included signature
functions that may not use their argument (as Jason did); this can be checked after normal type-checking if an attribution is added in I.Pi; find out where to skip the corresponding equality check
intertwine view and logical relation: semantics: every type goes to a subtype, every function preserves the subtype relation; using the relation during the definition of the view corresponds to proofs-in-terms
hide/filter/remove definitions from a signature (%sig ADD = Add %filter definitions except +)
parametrized views and structures
conservative structure declarations: definiens of structure is checked but dropped
  for declared structures this would also check totality
partial views default to identity; _ as module name; then %view %implicit _ : A -> B = {} to check definitional extensions.
make symbols with fixity parsable separately: look for corresponding error message in parse-term.fun; see if it can be done easily
read assignments in structures separately
%main c : A. in sig S; s : S used as constant defaults to s.c; same for included signatures
print out with nicer names
are implicit arguments printed?
exception when using non-existing field name of a struct
it should be possible to include morphisms for signatures that are not directly included; defaulting to identity should work even if such an import is already present; use case: import FOL with a single instantiation for the universe

filtering
anonymous morphisms
structure variables
patterns
pair types with proof irrelevance
morphism equality check, isomorphism check

ideas
designated arguments in modules to allow unqualified instantiation
skolem constants

--------
done
flattening of openend names
added roles of constants: type, constructor, judgment, rule; infered using switches %syntax. and %semantics
warnings and recoverable errors
- problems with preserved comments cause warning
- partial views/relations cause recoverable errors (unrecoverable error, if they are applied at the undefined argument)
- recover from error in definition by trying to omit the definiens
morphisms out of signatures with ancestors are legal if the ancestors are included into the codomain already
structure-includes
 - structures of signatures with includes do not have to include morphisms
   * instead another structure is generated
   * the name of the signature is the identifier of a generated structure
   * exception: no structure is generated for the meta-theory, instead a morphism must be provided by the structure (default to identity)
 - includes are always flattened transitively, i.e., all includes are direct
 - redundant includes are an error
 - opening included constants after a structure possible
the signature name is used as concrete syntax for the identity morphism
meta-theories: the first include of a signature may be given as %meta S
using URIs to identify namespaces and to abstract from file systems
dynamic loading of modules (%read deprecated)
eliminated .. qualifier, lookup now decides dynamically whether a name is a namespace prefix, a module name, or a list of symbol names
all toplevel declarations are pairs of a namespace and a name, prefixes can be declared to access names in other namespaces, namespace defaults to current file, in configurations name lookup searches all namespaces to achieve backwards compatibility
comments via %* *% before a named declaration are preserved with their line/column position, printed to OMDoc
anonymous constants _ : t
logical relations
includes and subsignatures reimplemented, includes can occur anywhere in a signature and include subsignatures
unqualified names are looked up in all parents first, first match is used; then in all included signatures, fail if non-unique
links can have multiple includes
added twelf-save-reset-check-file to emacs mode (works together with empty sources.cfg)
forbid instantiating defined constants
shadowing on toplevel
implement include in link, only one %include allowed in a link for now
empty %open in include chains name lookups (obsoleted later)
signatures may refer to symbols of ancestor signatures (qualified or - if not shadowed - directly)
views are only legal if no ancestor relation between domain and codomain and if all ancestors of domain are ancestors of codomain
%read reads a file; cfg files are deprecated, only elf file needed from now on
OMDoc export prints
 - only modules of a certain file
 - main file name is relative to pwd
 - all references to other modules and files with proper MMT-URIs
 - to do: nested signatures, toplevel signature
%struct %implicit and %view %implicit for implicit coercions