equal
deleted
inserted
replaced
19 |
19 |
20 signature ISABELLE_PROCESS = |
20 signature ISABELLE_PROCESS = |
21 sig |
21 sig |
22 val test_markupN: string |
22 val test_markupN: string |
23 val test_markup: Markup.T -> output * output |
23 val test_markup: Markup.T -> output * output |
|
24 val isabelle_processN: string |
24 val init: unit -> unit |
25 val init: unit -> unit |
25 end; |
26 end; |
26 |
27 |
27 structure IsabelleProcess: ISABELLE_PROCESS = |
28 structure IsabelleProcess: ISABELLE_PROCESS = |
28 struct |
29 struct |
29 |
30 |
30 (* test markup *) |
31 (* test_markup *) |
31 |
32 |
32 val test_markupN = "test_markup"; |
33 val test_markupN = "test_markup"; |
33 |
34 |
34 fun test_markup (name, props) = |
35 fun test_markup (name, props) = |
35 (enclose "<" ">" (space_implode " " (name :: map XML.attribute props)), |
36 (enclose "<" ">" (space_implode " " (name :: map XML.attribute props)), |
37 |
38 |
38 val _ = Markup.add_mode test_markupN test_markup; |
39 val _ = Markup.add_mode test_markupN test_markup; |
39 |
40 |
40 |
41 |
41 (* channels *) |
42 (* channels *) |
|
43 |
|
44 val isabelle_processN = "isabelle_process"; |
42 |
45 |
43 local |
46 local |
44 |
47 |
45 fun special c = chr 2 ^ c; |
48 fun special c = chr 2 ^ c; |
46 val special_end = special "."; |
49 val special_end = special "."; |
56 Output.tracing_fn := output "C" Markup.tracing; |
59 Output.tracing_fn := output "C" Markup.tracing; |
57 Output.warning_fn := output "D" Markup.warning; |
60 Output.warning_fn := output "D" Markup.warning; |
58 Output.error_fn := output "E" Markup.error; |
61 Output.error_fn := output "E" Markup.error; |
59 Output.debug_fn := output "F" Markup.debug); |
62 Output.debug_fn := output "F" Markup.debug); |
60 |
63 |
|
64 val _ = Markup.add_mode isabelle_processN (fn (name, _) => |
|
65 if name = Markup.promptN then (special "G", special_end ^ "\n") |
|
66 else ("", "")); |
|
67 |
61 end; |
68 end; |
62 |
69 |
63 |
70 |
64 (* init *) |
71 (* init *) |
65 |
72 |
66 fun init () = |
73 fun init () = |
67 (Output.writeln_default ("\nPID=" ^ string_of_pid (Posix.ProcEnv.getpid ())); |
74 (Output.writeln_default ("\nPID=" ^ string_of_pid (Posix.ProcEnv.getpid ())); |
68 setup_channels (); |
75 setup_channels (); |
|
76 change print_mode (update (op =) isabelle_processN); |
69 Isar.secure_main ()); |
77 Isar.secure_main ()); |
70 |
78 |
71 end; |
79 end; |
72 |
80 |