Can Common Logic text structure be mapped to DOL theories in a better way?

[tillmo]

Currently, the abstract syntax of Common Logic starts as follows:

-- Common Logic Syntax
data TEXT_META = Text_meta { getText :: TEXT
                           , textIri :: Maybe IRI
                           , nondiscourseNames :: Maybe (Set NAME)
                           , prefix_map :: [PrefixMapping]
                           } deriving (Show, Eq, Ord, Typeable, Data)

data TEXT = Text [PHRASE] Id.Range
          | Named_text NAME TEXT Id.Range
            deriving (Show, Ord, Eq, Typeable, Data)

data PHRASE = Module MODULE
            | Sentence SENTENCE
            | Importation IMPORTATION
            | Comment_text COMMENT TEXT Id.Range
              deriving (Show, Ord, Eq, Typeable, Data)

data SENTENCE = Quant_sent QUANT [NAME_OR_SEQMARK] SENTENCE Id.Range
              | Bool_sent BOOL_SENT Id.Range
              | Atom_sent ATOM Id.Range
              | Comment_sent COMMENT SENTENCE Id.Range
              | Irregular_sent SENTENCE Id.Range
                deriving (Show, Ord, Eq, Typeable, Data)

data QUANT = Universal | Existential
             deriving (Show, Ord, Eq, Typeable, Data)

data BOOL_SENT = Junction AndOr [SENTENCE]
               | Negation SENTENCE
               | BinOp ImplEq SENTENCE SENTENCE
                 deriving (Show, Ord, Eq, Typeable, Data)

data AndOr = Conjunction | Disjunction
             deriving (Show, Ord, Eq, Typeable, Data)

data ImplEq = Implication | Biconditional
              deriving (Show, Ord, Eq, Typeable, Data)

data ATOM = Equation TERM TERM
          | Atom TERM [TERM_SEQ]
            deriving (Show, Ord, Eq, Typeable, Data)
[...]

Now Common logic sentences, which are used to form DOL theories, are TEXT_METAs. This leads to the weird situation that a whole Common Logic theory typically consists of a single sentence (aka TEXT_META), and also for theorem proving, only one sentence is shown. Also, prefix maps are usually stored together with DOL libraries, not with single sentences.
How can we map Common Logic TEXT_METAs in a better way to DOL/Hets theories? Ideally, SENTENCE should be used as sentences, and the remaining Common Logic structure elements should be mapped to DOL structure elements. However, for MODULEs, this probably will not work. Perhaps, we just need to keep the present structure in case that MODULEs are present, but map to DOL in a better way, if they are not present.