21 *) |
21 *) |
22 |
22 |
23 signature ISABELLE_PROCESS = |
23 signature ISABELLE_PROCESS = |
24 sig |
24 sig |
25 val isabelle_processN: string |
25 val isabelle_processN: string |
26 val full_markupN: string |
26 val xmlN: string |
27 val yxmlN: string |
|
28 val init: unit -> unit |
27 val init: unit -> unit |
29 end; |
28 end; |
30 |
29 |
31 structure IsabelleProcess: ISABELLE_PROCESS = |
30 structure IsabelleProcess: ISABELLE_PROCESS = |
32 struct |
31 struct |
33 |
32 |
34 (* print modes *) |
33 (* print modes *) |
35 |
34 |
36 val isabelle_processN = "isabelle_process"; |
35 val isabelle_processN = "isabelle_process"; |
37 val full_markupN = "full_markup"; |
36 val xmlN = "XML"; |
38 val yxmlN = "YXML"; |
|
39 |
37 |
40 val _ = Output.add_mode isabelle_processN Output.default_output Output.default_escape; |
38 val _ = Output.add_mode isabelle_processN Output.default_output Output.default_escape; |
41 |
39 val _ = Markup.add_mode isabelle_processN (YXML.output_markup); |
42 val _ = Markup.add_mode isabelle_processN (fn (name, props) => |
|
43 if print_mode_active full_markupN orelse name = Markup.positionN |
|
44 then YXML.output_markup (name, props) else ("", "")); |
|
45 |
40 |
46 |
41 |
47 (* message markup *) |
42 (* message markup *) |
48 |
43 |
49 fun special ch = Symbol.STX ^ ch; |
44 fun special ch = Symbol.STX ^ ch; |
59 |
54 |
60 fun message_props props = |
55 fun message_props props = |
61 let val clean = clean_string [Symbol.STX, "\n", "\r"] |
56 let val clean = clean_string [Symbol.STX, "\n", "\r"] |
62 in implode (map (fn (x, y) => clean x ^ "=" ^ clean y ^ special_sep ^ "\n") props) end; |
57 in implode (map (fn (x, y) => clean x ^ "=" ^ clean y ^ special_sep ^ "\n") props) end; |
63 |
58 |
64 fun message_text ts = |
59 fun message_text class ts = |
65 let |
60 let |
66 val doc = XML.Elem ("message", [], ts); |
61 val doc = XML.Elem ("message", [("class", class)], ts); |
67 val msg = |
62 val msg = |
68 if not (print_mode_active full_markupN) then |
63 if print_mode_active xmlN then XML.header ^ XML.string_of doc |
69 Buffer.content (fold XML.add_content ts Buffer.empty) |
64 else YXML.string_of doc; |
70 else if print_mode_active yxmlN then YXML.string_of doc |
|
71 else XML.header ^ XML.string_of doc; |
|
72 in clean_string [Symbol.STX] msg end; |
65 in clean_string [Symbol.STX] msg end; |
73 |
66 |
74 fun message_pos ts = get_first get_pos ts |
67 fun message_pos ts = get_first get_pos ts |
75 and get_pos (elem as XML.Elem (name, atts, ts)) = |
68 and get_pos (elem as XML.Elem (name, atts, ts)) = |
76 if name = Markup.positionN then SOME (Position.of_properties atts) |
69 if name = Markup.positionN then SOME (Position.of_properties atts) |
77 else message_pos ts |
70 else message_pos ts |
78 | get_pos _ = NONE; |
71 | get_pos _ = NONE; |
79 |
72 |
80 in |
73 in |
81 |
74 |
82 fun message _ "" = () |
75 fun message _ _ "" = () |
83 | message ch body = |
76 | message ch class body = |
84 let |
77 let |
85 val (txt, pos) = |
78 val (txt, pos) = |
86 let val ts = YXML.parse_body body |
79 let val ts = YXML.parse_body body |
87 in (message_text ts, the_default Position.none (message_pos ts)) end |
80 in (message_text class ts, the_default Position.none (message_pos ts)) end; |
88 handle Fail msg => ("*** MALFORMED MESSAGE ***\n" ^ msg, Position.none); |
|
89 val props = |
81 val props = |
90 Position.properties_of (Position.thread_data ()) |
82 Position.properties_of (Position.thread_data ()) |
91 |> Position.default_properties pos; |
83 |> Position.default_properties pos; |
92 in Output.writeln_default (special ch ^ message_props props ^ txt ^ special_end) end; |
84 in Output.writeln_default (special ch ^ message_props props ^ txt ^ special_end) end; |
93 |
85 |
102 |
94 |
103 |
95 |
104 (* channels *) |
96 (* channels *) |
105 |
97 |
106 fun setup_channels () = |
98 fun setup_channels () = |
107 (Output.writeln_fn := message "A"; |
99 (Output.writeln_fn := message "A" "writeln"; |
108 Output.priority_fn := message "B"; |
100 Output.priority_fn := message "B" "priority"; |
109 Output.tracing_fn := message "C"; |
101 Output.tracing_fn := message "C" "tracing"; |
110 Output.warning_fn := message "D"; |
102 Output.warning_fn := message "D" "warning"; |
111 Output.error_fn := message "E"; |
103 Output.error_fn := message "E" "error"; |
112 Output.debug_fn := message "F"; |
104 Output.debug_fn := message "F" "debug"; |
113 Output.prompt_fn := message "G"; |
105 Output.prompt_fn := message "G" "prompt"; |
114 Output.status_fn := message "I"); |
106 Output.status_fn := message "I" "status"); |
115 |
107 |
116 |
108 |
117 (* init *) |
109 (* init *) |
118 |
110 |
119 fun init () = |
111 fun init () = |