src/Pure/Tools/build.ML
changeset 67219 81e9804b2014
parent 66873 9953ae603a23
child 67297 86a099f896fc
     1.1 --- a/src/Pure/Tools/build.ML	Sat Dec 16 20:02:40 2017 +0100
     1.2 +++ b/src/Pure/Tools/build.ML	Sat Dec 16 21:53:07 2017 +0100
     1.3 @@ -148,6 +148,7 @@
     1.4    name: string,
     1.5    master_dir: Path.T,
     1.6    theories: (Options.T * (string * Position.T) list) list,
     1.7 +  sessions: string list,
     1.8    global_theories: (string * string) list,
     1.9    loaded_theories: string list,
    1.10    known_theories: (string * string) list};
    1.11 @@ -158,33 +159,34 @@
    1.12      val position = Position.of_properties o properties;
    1.13      val (symbol_codes, (command_timings, (do_output, (verbose, (browser_info,
    1.14        (document_files, (graph_file, (parent_name, (chapter, (name, (master_dir,
    1.15 -      (theories, (global_theories, (loaded_theories, known_theories)))))))))))))) =
    1.16 +      (theories, (sessions, (global_theories, (loaded_theories, known_theories))))))))))))))) =
    1.17        pair (list (pair string int)) (pair (list properties) (pair bool (pair bool (pair string
    1.18          (pair (list (pair string string)) (pair string (pair string (pair string (pair string
    1.19            (pair string
    1.20              (pair (((list (pair Options.decode (list (pair string position))))))
    1.21 -              (pair (list (pair string string))
    1.22 -                (pair (list string) (list (pair string string)))))))))))))))
    1.23 +              (pair (list string) (pair (list (pair string string))
    1.24 +                (pair (list string) (list (pair string string))))))))))))))))
    1.25        (YXML.parse_body yxml);
    1.26    in
    1.27      Args {symbol_codes = symbol_codes, command_timings = command_timings, do_output = do_output,
    1.28        verbose = verbose, browser_info = Path.explode browser_info,
    1.29        document_files = map (apply2 Path.explode) document_files,
    1.30        graph_file = Path.explode graph_file, parent_name = parent_name, chapter = chapter,
    1.31 -      name = name, master_dir = Path.explode master_dir, theories = theories,
    1.32 +      name = name, master_dir = Path.explode master_dir, theories = theories, sessions = sessions,
    1.33        global_theories = global_theories, loaded_theories = loaded_theories,
    1.34        known_theories = known_theories}
    1.35    end;
    1.36  
    1.37  fun build_session (Args {symbol_codes, command_timings, do_output, verbose, browser_info,
    1.38 -    document_files, graph_file, parent_name, chapter, name, master_dir, theories,
    1.39 +    document_files, graph_file, parent_name, chapter, name, master_dir, theories, sessions,
    1.40      global_theories, loaded_theories, known_theories}) =
    1.41    let
    1.42      val symbols = HTML.make_symbols symbol_codes;
    1.43  
    1.44      val _ =
    1.45        Resources.init_session_base
    1.46 -        {global_theories = global_theories,
    1.47 +        {sessions = sessions,
    1.48 +         global_theories = global_theories,
    1.49           loaded_theories = loaded_theories,
    1.50           known_theories = known_theories};
    1.51