doc-src/IsarRef/logics.tex

 
 typeconstructor : nameref;
 
 class : nameref;
 
-seri : target | 'SML' ( string | '-' | ()) | 'Haskell' (string | ());
+seri : target | 'SML' ( string | '-' ) | 'Haskell' ( 'root:' string ) ? 'string\_classes' ? string;
 
 target : 'SML' | 'Haskell';
 
 'code\_const' (const + 'and') \\
   ( ( '(' target ( syntax + 'and' ) ')' ) + );

   In the first case, code is written to the specified file, in the latter
   it is compiled internally in the context of the current ML session.
 
   For \emph{Haskell}, a directory name is specified; different modules
   are serialized to different files in this directory or
-  subdirectories, reflecting the module hierarchy.
+  subdirectories, reflecting the module hierarchy. Additionally
+  a module name prefix may be given using the ``root:'' argument;
+  ``string\_classes'' adds a ``deriving (Read, Show)'' clause
+  to each appropriate datatype declaration.
 
 \item [$\isarcmd{code_const}$] associates a list of constants
   with target-specific serializations.
 
 \item [$\isarcmd{code_type}$] associates a list of type constructors