Flattening

Flattening is the normalization of documents with respect to ref elements, variants and theory imports. It also includes the reverse process of contracting referenced content, i.e., introduction of references in the form of refs or variants. This is handled by the code in the flattening package.

Ref Introduction

Ref introduction is the process of replacing specific elements with ref elements. A RefIntroducer can be used to just replace a given element with a ref.

Variant Contraction

See Abstract Documents Module

Ref Introduction

Ref introduction is the process of replacing specific elements with ref elements. RefIntroducer? can be used to replace a given element with a ref.

Variant Introduction

VariantIntroducer is same as the RefIntroducer, but instead of a ref element it introduces a variant.

Document Introduction

DocumentIntroducer is a flexible element introducer in a whole document, in which elements that should be replaced are selected with XPath expressions. The original elements can be placed in the same document or in a new content document. For replacing the selected it can use a RefIntroducer, or a VariantIntroducer.

Theory Flattening

Theory flattening is the process of replacing imports elements in theories, with the theories they import. This flattening is done recursively, until no imports are left in the original theory. The theory flattening functionality is available as a method of an !OMDocDocument, and can be used like this:

OMDocDocument omdoc = Parser.parse(xomDocument);
omdoc.flatten();
// print result to standard output
Serializer.serialize(omdoc, System.out);