equal
deleted
inserted
replaced
8 struct |
8 struct |
9 |
9 |
10 val _ = |
10 val _ = |
11 Isabelle_Process.protocol_command "Prover.echo" |
11 Isabelle_Process.protocol_command "Prover.echo" |
12 (fn args => List.app writeln args); |
12 (fn args => List.app writeln args); |
13 |
|
14 val _ = |
|
15 Isabelle_Process.protocol_command "Prover.init_symbols" |
|
16 (fn [codes_yxml] => |
|
17 YXML.parse_body codes_yxml |
|
18 |> let open XML.Decode in list (pair string int) end |
|
19 |> HTML.init_symbols); |
|
20 |
13 |
21 val _ = |
14 val _ = |
22 Isabelle_Process.protocol_command "Prover.options" |
15 Isabelle_Process.protocol_command "Prover.options" |
23 (fn [options_yxml] => |
16 (fn [options_yxml] => |
24 let val options = Options.decode (YXML.parse_body options_yxml) in |
17 let val options = Options.decode (YXML.parse_body options_yxml) in |