equal
deleted
inserted
replaced
8 sig |
8 sig |
9 val name: unit -> string |
9 val name: unit -> string |
10 val welcome: unit -> string |
10 val welcome: unit -> string |
11 val get_keywords: unit -> Keyword.keywords |
11 val get_keywords: unit -> Keyword.keywords |
12 val init: bool -> bool -> Path.T -> string -> bool -> string -> (string * string) list -> |
12 val init: bool -> bool -> Path.T -> string -> bool -> string -> (string * string) list -> |
13 (Path.T * Path.T) list -> string -> string * string -> bool -> unit |
13 (Path.T * Path.T) list -> Path.T -> string -> string * string -> bool -> unit |
14 val shutdown: unit -> unit |
14 val shutdown: unit -> unit |
15 val finish: unit -> unit |
15 val finish: unit -> unit |
16 val save: string -> unit |
16 val save: string -> unit |
17 val protocol_handler: string -> unit |
17 val protocol_handler: string -> unit |
18 val init_protocol_handlers: unit -> unit |
18 val init_protocol_handlers: unit -> unit |
40 fun get_keywords () = ! keywords; |
40 fun get_keywords () = ! keywords; |
41 |
41 |
42 |
42 |
43 (* init *) |
43 (* init *) |
44 |
44 |
45 fun init build info info_path doc doc_graph doc_output doc_variants doc_files |
45 fun init build info info_path doc doc_graph doc_output doc_variants doc_files graph_file |
46 parent (chapter, name) verbose = |
46 parent (chapter, name) verbose = |
47 if #name (! session) <> parent orelse not (! session_finished) then |
47 if #name (! session) <> parent orelse not (! session_finished) then |
48 error ("Unfinished parent session " ^ quote parent ^ " for " ^ quote name) |
48 error ("Unfinished parent session " ^ quote parent ^ " for " ^ quote name) |
49 else |
49 else |
50 let |
50 let |
51 val _ = session := {chapter = chapter, name = name}; |
51 val _ = session := {chapter = chapter, name = name}; |
52 val _ = session_finished := false; |
52 val _ = session_finished := false; |
53 in |
53 in |
54 Present.init build info info_path (if doc = "false" then "" else doc) |
54 Present.init build info info_path (if doc = "false" then "" else doc) |
55 doc_graph doc_output doc_variants doc_files (chapter, name) |
55 doc_graph doc_output doc_variants doc_files graph_file (chapter, name) |
56 verbose (map Thy_Info.get_theory (Thy_Info.get_names ())) |
56 verbose (map Thy_Info.get_theory (Thy_Info.get_names ())) |
57 end; |
57 end; |
58 |
58 |
59 |
59 |
60 (* finish *) |
60 (* finish *) |