equal
deleted
inserted
replaced
5 *) |
5 *) |
6 |
6 |
7 signature PRESENT = |
7 signature PRESENT = |
8 sig |
8 sig |
9 val session_name: theory -> string |
9 val session_name: theory -> string |
|
10 val document_enabled: string -> bool |
10 val document_variants: string -> (string * string) list |
11 val document_variants: string -> (string * string) list |
11 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 -> |
12 (Path.T * Path.T) list -> string * string -> bool -> theory list -> unit (*not thread-safe!*) |
13 (Path.T * Path.T) list -> string * string -> bool -> theory list -> unit (*not thread-safe!*) |
13 val finish: unit -> unit (*not thread-safe!*) |
14 val finish: unit -> unit (*not thread-safe!*) |
14 val theory_output: string -> string -> unit |
15 val theory_output: string -> string -> unit |
190 |
191 |
191 |
192 |
192 |
193 |
193 (** document preparation **) |
194 (** document preparation **) |
194 |
195 |
195 (* document variants *) |
196 (* options *) |
|
197 |
|
198 fun document_enabled s = s <> "" andalso s <> "false"; |
196 |
199 |
197 fun document_variants str = |
200 fun document_variants str = |
198 let |
201 let |
199 fun read_variant s = |
202 fun read_variant s = |
200 (case space_explode "=" s of |
203 (case space_explode "=" s of |