Is there an include-like command for 'struct', similar to 'include' for 'sig'?

Question

This question is related to how sectioning and Sidekick can be used with Isabelle/ML in Isabelle/jEdit.

Consider two Isar commands, section and ML. These commands act as sectioning commands in the tree of the jEdit Sidekick plugin.

One consequence is that I can use multiple ML{*...*} statements in a THY file to document, organize, and discuss ML code, rather than import ML using a ML_file command. There are reasons not to do this, but it can be useful.

There is a problem, though. I don't know how to break up the defining of multiple functions in a structure.

Below, I show three THY files, to show different things I've tried. I ask my question here: "Is there a way to break up a structure, to end up with one structure, so I have one name space for a set of functions?"

I begin by wanting one name space, Foo

Here is what I want my end result to look like:

ML{* 
  Foo.val1;
  Foo.val2
*} 

Breaking up my signature is not a problem. I can easily do that with include, but I don't know of any include-like statement for structure. So, if I had 50 functions in my signature Foo, I would have one big, long ML{*...*} command.

theory i150312ba__sig_with_2_sig_includes___one_struct
imports Complex_Main
begin
section{* FOO_1, FOO_2, FOO *} 

    ML{*signature FOO_1 = 
    sig
      val val1 : string
    end*}

    ML{*signature FOO_2 = 
    sig
      val val2 : string
    end*}

    ML{*signature FOO = 
    sig
      include FOO_1
      include FOO_2
    end*}

section{* Foo *}

    ML{*structure Foo : FOO = 
    struct
      val val1 = "val1"
      val val2 = "val2"
    end*}

section{* One namespace, but had to define 'Foo' all at once *}

    ML{* 
      Foo.val1;
      Foo.val2
    *}    

end

A sig with 2 structs, but then I have 2 name spaces

I get this:

ML{*
  Sig.S1.val1;
  Sig.S2.val2
*}

So the following example is no good either:

theory i150312bb__sig_with_two_structures
imports Complex_Main
begin
section{* FOO_1, Foo_1 *} 

    ML{*signature FOO_1  
    =sig
      val val1 : string
    end*}

    ML{*structure Foo_1 : FOO_1 
    =struct
      val val1 = "val1"
    end*}

section{* FOO_2, Foo_2 *} 

    ML{*signature FOO_2  
    =sig
      val val2 : string
    end*}

    ML{*structure Foo_2 : FOO_2  
    =struct
      val val2 = "val2"
    end*}

section{* FOO_, Foo_ *}       

    ML{*signature FOO_  
    =sig
       structure S1 : FOO_1
       structure S2 : FOO_2
    end*}

    ML{*structure Foo : FOO_  
    =struct
      structure S1 = Foo_1
      structure S2 = Foo_2
    end*}

section{* Nested namespaces; no good *} 

    ML{*
      Foo.S1.val1;
      Foo.S2.val2
    *}

Two outside structs named different, with inside structs named the same

I have structures Foo_1_2 and Foo_2_2. Both contain a different structure, but with the same name Foo. I try to open them both, but the last use of open takes priority, so this doesn't work:

ML{*
  Foo.val2;
  Foo.val1 (*Not visible.*)
*}

The theory:

theory i150312bc__outside_name_different__inside_name_the_name
imports Complex_Main
begin
section{* FOO_1, Foo_1, FOO_1_2, Foo_1_2 *} 

    ML{*signature FOO_1 =
      sig
        val val1 : string
      end

      structure Foo_1 : FOO_1 =
      struct
        val val1 = "val1"
      end

      signature FOO_1_2 = sig 
        structure Foo : FOO_1
      end

      structure Foo_1_2 : FOO_1_2 = struct
        structure Foo = Foo_1
      end

      open Foo_1_2;
    *}

section{* FOO_2, Foo_2, FOO_2_2, Foo_2_2 *} 

    ML{*signature FOO_2 =
      sig
        val val2 : string
      end

      structure Foo_2 : FOO_2 =
      struct
        val val2 = "val2"
      end

      signature FOO_2_2 = sig 
        structure Foo : FOO_2
      end

      structure Foo_2_2 : FOO_2_2 = 
      struct
        structure Foo = Foo_2
      end

      open Foo_2_2;
    *}

section{* The last 'open' takes priority *}     
    ML{*
      Foo.val2;
      Foo.val1 (*Not visible.*)
    *}

Answer 1

The structure-level equivalent to include is open:

structure Foo1 = 
struct
  val val1 = "val1"
end

structure Foo2 = 
struct
  val val2 = "foo2"
end

structure Foo = 
struct
  open Foo1
  open Foo2
end