src/Pure/Tools/build.ML

   parent_name: string,
   chapter: string,
   name: string,
   master_dir: Path.T,
   theories: (Options.T * (string * Position.T) list) list,
+  sessions: string list,
   global_theories: (string * string) list,
   loaded_theories: string list,
   known_theories: (string * string) list};
 
 fun decode_args yxml =
   let
     open XML.Decode;
     val position = Position.of_properties o properties;
     val (symbol_codes, (command_timings, (do_output, (verbose, (browser_info,
       (document_files, (graph_file, (parent_name, (chapter, (name, (master_dir,
-      (theories, (global_theories, (loaded_theories, known_theories)))))))))))))) =
+      (theories, (sessions, (global_theories, (loaded_theories, known_theories))))))))))))))) =
       pair (list (pair string int)) (pair (list properties) (pair bool (pair bool (pair string
         (pair (list (pair string string)) (pair string (pair string (pair string (pair string
           (pair string
             (pair (((list (pair Options.decode (list (pair string position))))))
-              (pair (list (pair string string))
-                (pair (list string) (list (pair string string)))))))))))))))
+              (pair (list string) (pair (list (pair string string))
+                (pair (list string) (list (pair string string))))))))))))))))
       (YXML.parse_body yxml);
   in
     Args {symbol_codes = symbol_codes, command_timings = command_timings, do_output = do_output,
       verbose = verbose, browser_info = Path.explode browser_info,
       document_files = map (apply2 Path.explode) document_files,
       graph_file = Path.explode graph_file, parent_name = parent_name, chapter = chapter,
-      name = name, master_dir = Path.explode master_dir, theories = theories,
+      name = name, master_dir = Path.explode master_dir, theories = theories, sessions = sessions,
       global_theories = global_theories, loaded_theories = loaded_theories,
       known_theories = known_theories}
   end;
 
 fun build_session (Args {symbol_codes, command_timings, do_output, verbose, browser_info,
-    document_files, graph_file, parent_name, chapter, name, master_dir, theories,
+    document_files, graph_file, parent_name, chapter, name, master_dir, theories, sessions,
     global_theories, loaded_theories, known_theories}) =
   let
     val symbols = HTML.make_symbols symbol_codes;
 
     val _ =
       Resources.init_session_base
-        {global_theories = global_theories,
+        {sessions = sessions,
+         global_theories = global_theories,
          loaded_theories = loaded_theories,
          known_theories = known_theories};
 
     val _ =
       Session.init