76 fun pgip_serial () = inc pgip_seq |
47 fun pgip_serial () = inc pgip_seq |
77 |
48 |
78 fun assemble_pgips pgips = |
49 fun assemble_pgips pgips = |
79 Pgip { tag = SOME pgip_tag, |
50 Pgip { tag = SOME pgip_tag, |
80 class = pgip_class, |
51 class = pgip_class, |
81 seq = pgip_serial(), |
52 seq = pgip_serial (), |
82 id = !pgip_id, |
53 id = ! pgip_id, |
83 destid = !pgip_refid, |
54 destid = ! pgip_refid, |
84 (* destid=refid since Isabelle only communicates back to sender *) |
55 (* destid=refid since Isabelle only communicates back to sender *) |
85 refid = !pgip_refid, |
56 refid = ! pgip_refid, |
86 refseq = !pgip_refseq, |
57 refseq = ! pgip_refseq, |
87 content = pgips } |
58 content = pgips } |
88 in |
59 in |
89 |
60 |
90 fun init_pgip_session_id () = |
61 fun init_pgip_session_id () = |
91 pgip_id := getenv "HOSTNAME" ^ "/" ^ getenv "USER" ^ "/" ^ |
62 pgip_id := getenv "HOSTNAME" ^ "/" ^ getenv "USER" ^ "/" ^ |
92 getenv "ISABELLE_PID" ^ "/" ^ Time.toString (Time.now ()) |
63 getenv "ISABELLE_PID" ^ "/" ^ Time.toString (Time.now ()) |
93 |
64 |
94 fun matching_pgip_id id = (id = !pgip_id) |
65 fun matching_pgip_id id = (id = ! pgip_id) |
95 |
66 |
96 val output_xml_fn = ref Output.writeln_default |
67 val output_xml_fn = ref Output.writeln_default |
97 fun output_xml s = (!output_xml_fn) (XML.string_of s); (* TODO: string buffer *) |
68 fun output_xml s = ! output_xml_fn (XML.string_of s); |
98 |
69 |
99 val output_pgips = |
70 val output_pgips = XML.string_of o PgipOutput.output o assemble_pgips o map PgipOutput.output; |
100 XML.string_of o PgipOutput.output o assemble_pgips o map PgipOutput.output; |
71 |
101 |
72 val output_pgmlterm = XML.string_of o Pgml.pgmlterm_to_xml; |
102 val output_pgmlterm = |
73 val output_pgmltext = XML.string_of o Pgml.pgml_to_xml; |
103 XML.string_of o Pgml.pgmlterm_to_xml; |
|
104 |
|
105 val output_pgmltext = |
|
106 XML.string_of o Pgml.pgml_to_xml; |
|
107 |
74 |
108 |
75 |
109 fun issue_pgip_rawtext str = |
76 fun issue_pgip_rawtext str = |
110 output_xml (PgipOutput.output (assemble_pgips [XML.Output str])) |
77 output_xml (PgipOutput.output (assemble_pgips (YXML.parse_body str))); |
111 |
|
112 fun issue_pgips pgipops = |
|
113 output_xml (PgipOutput.output (assemble_pgips (map PgipOutput.output pgipops))); |
|
114 |
78 |
115 fun issue_pgip pgipop = |
79 fun issue_pgip pgipop = |
116 output_xml (PgipOutput.output (assemble_pgips [PgipOutput.output pgipop])); |
80 output_xml (PgipOutput.output (assemble_pgips [PgipOutput.output pgipop])); |
117 |
81 |
118 end; |
82 end; |
119 |
83 |
120 |
84 |
121 fun pgml area terms = Pgml.Pgml { version=NONE,systemid=NONE, |
|
122 area=SOME area, content=terms } |
|
123 |
85 |
124 (** messages and notification **) |
86 (** messages and notification **) |
125 |
87 |
|
88 (* PGML terms *) |
|
89 |
126 local |
90 local |
127 val delay_msgs = ref false (*true: accumulate messages*) |
91 |
128 val delayed_msgs = ref [] |
92 fun pgml_sym s = |
129 |
93 if ! pgmlsymbols_flag then |
130 fun queue_or_issue pgip = |
94 (case Symbol.decode s of |
131 if ! delay_msgs then |
95 Symbol.Sym name => Pgml.Sym {name = name, content = s} |
132 delayed_msgs := pgip :: ! delayed_msgs |
96 | _ => Pgml.Str s) |
133 else issue_pgip pgip |
97 else Pgml.Str s; |
134 |
98 |
135 fun wrap_pgml area s = |
99 val pgml_syms = map pgml_sym o Symbol.explode; |
136 if String.isPrefix "<pgml" s then |
100 |
137 XML.Output s (* already pgml outermost *) |
101 val token_markups = |
138 else |
102 [Markup.tclassN, Markup.tfreeN, Markup.tvarN, Markup.freeN, |
139 Pgml.pgml_to_xml (pgml area [Pgml.Raw (XML.Output s)]) (* mixed *) |
103 Markup.boundN, Markup.varN, Markup.skolemN]; |
140 |
104 |
141 in |
105 in |
142 fun normalmsg area s = |
106 |
143 let |
107 fun pgml_terms (XML.Elem (name, atts, body)) = |
144 val content = wrap_pgml area s |
108 if member (op =) token_markups name then |
145 val pgip = Normalresponse { content=[content] } |
109 let val content = pgml_syms (Buffer.content (fold XML.add_content body Buffer.empty)) |
146 in |
110 in [Pgml.Atoms {kind = SOME name, content = content}] end |
147 queue_or_issue pgip |
111 else |
|
112 let val content = maps pgml_terms body in |
|
113 if name = Markup.blockN then |
|
114 [Pgml.Box {orient = NONE, indent = Properties.get_int atts Markup.indentN, content = content}] |
|
115 else if name = Markup.breakN then |
|
116 [Pgml.Break {mandatory = NONE, indent = Properties.get_int atts Markup.widthN}] |
|
117 else if name = Markup.fbreakN then |
|
118 [Pgml.Break {mandatory = SOME true, indent = NONE}] |
|
119 else content |
148 end |
120 end |
149 |
121 | pgml_terms (XML.Text text) = map (Pgml.Raw o Pgml.atom_to_xml) (pgml_syms text); |
150 fun errormsg area fatality s = |
122 |
151 let |
|
152 val content = wrap_pgml area s |
|
153 val pgip = Errorresponse { fatality=fatality, |
|
154 location=NONE, |
|
155 content=[content] } |
|
156 in |
|
157 queue_or_issue pgip |
|
158 end |
|
159 |
|
160 (* Error responses with useful locations *) |
|
161 fun error_with_pos area fatality pos s = |
|
162 let |
|
163 val content = wrap_pgml area s |
|
164 val pgip = Errorresponse { fatality=fatality, |
|
165 location=SOME (PgipIsabelle.location_of_position pos), |
|
166 content=[content] } |
|
167 in |
|
168 queue_or_issue pgip |
|
169 end |
|
170 |
|
171 fun start_delay_msgs () = (set delay_msgs; delayed_msgs := []) |
|
172 fun end_delayed_msgs () = (reset delay_msgs; ! delayed_msgs) |
|
173 end; |
123 end; |
174 |
124 |
175 (* NB: all of the standard error/message functions now expect already-escaped text. |
125 |
176 FIXME: this may cause us problems now we're generating trees; on the other |
126 (* messages *) |
177 hand the output functions were tuned some time ago, so it ought to be |
127 |
178 enough to use XML.Output always above. *) |
128 fun pgml area content = |
179 (* NB 2: all of standard functions print strings terminated with new lines, but we don't |
129 Pgml.Pgml {version = NONE, systemid = NONE, area = SOME area, content = content}; |
|
130 |
|
131 fun message_content default_area s = |
|
132 let |
|
133 val body = YXML.parse_body s; |
|
134 val area = |
|
135 (case body of |
|
136 [XML.Elem (name, _, _)] => |
|
137 if name = Markup.stateN then PgipTypes.Display else default_area |
|
138 | _ => default_area); |
|
139 in Pgml.pgml_to_xml (pgml area (maps pgml_terms body)) end; |
|
140 |
|
141 |
|
142 fun normalmsg area s = issue_pgip |
|
143 (Normalresponse {content = [message_content area s]}); |
|
144 |
|
145 fun errormsg area fatality s = issue_pgip |
|
146 (Errorresponse {fatality = fatality, location = NONE, content = [message_content area s]}); |
|
147 |
|
148 (*error responses with useful locations*) |
|
149 fun error_with_pos area fatality pos s = issue_pgip |
|
150 (Errorresponse { |
|
151 fatality = fatality, |
|
152 location = SOME (PgipIsabelle.location_of_position pos), |
|
153 content = [message_content area s]}); |
|
154 |
|
155 fun panic s = (errormsg Message Panic ("## SYSTEM EXIT ##\n" ^ s); exit 1); |
|
156 fun nonfatal_error s = errormsg Message Nonfatal s; |
|
157 fun log_msg s = errormsg Message Log s; |
|
158 |
|
159 (* NB: all of standard functions print strings terminated with new lines, but we don't |
180 add new lines explicitly in PGIP: they are left implicit. It means that PGIP messages |
160 add new lines explicitly in PGIP: they are left implicit. It means that PGIP messages |
181 can't be written without newlines. *) |
161 can't be written without newlines. *) |
182 |
|
183 fun setup_messages () = |
162 fun setup_messages () = |
184 (Output.writeln_fn := (fn s => normalmsg Message s); |
163 (Output.writeln_fn := (fn s => normalmsg Message s); |
185 Output.status_fn := (fn _ => ()); |
164 Output.status_fn := (fn _ => ()); |
186 Output.priority_fn := (fn s => normalmsg Status s); |
165 Output.priority_fn := (fn s => normalmsg Status s); |
187 Output.tracing_fn := (fn s => normalmsg Tracing s); |
166 Output.tracing_fn := (fn s => normalmsg Tracing s); |
188 Output.warning_fn := (fn s => errormsg Message Warning s); |
167 Output.warning_fn := (fn s => errormsg Message Warning s); |
189 Output.error_fn := (fn s => errormsg Message Fatal s); |
168 Output.error_fn := (fn s => errormsg Message Fatal s); |
190 Output.debug_fn := (fn s => errormsg Message Debug s)); |
169 Output.debug_fn := (fn s => errormsg Message Debug s)); |
191 |
|
192 fun panic s = (errormsg Message Panic ("## SYSTEM EXIT ##\n" ^ s); exit 1); |
|
193 fun nonfatal_error s = errormsg Message Nonfatal s; |
|
194 fun log_msg s = errormsg Message Log s; |
|
195 |
170 |
196 |
171 |
197 (* immediate messages *) |
172 (* immediate messages *) |
198 |
173 |
199 fun tell_clear_goals () = |
174 fun tell_clear_goals () = |
208 issue_pgip (Informfileoutdated {url=PgipTypes.pgipurl_of_path path, |
183 issue_pgip (Informfileoutdated {url=PgipTypes.pgipurl_of_path path, |
209 completed=completed}) |
184 completed=completed}) |
210 fun tell_file_retracted completed path = |
185 fun tell_file_retracted completed path = |
211 issue_pgip (Informfileretracted {url=PgipTypes.pgipurl_of_path path, |
186 issue_pgip (Informfileretracted {url=PgipTypes.pgipurl_of_path path, |
212 completed=completed}) |
187 completed=completed}) |
213 |
|
214 |
|
215 (* common markup *) |
|
216 |
|
217 local |
|
218 |
|
219 val no_text = chr 0; |
|
220 |
|
221 val pgmlterms_no_text= [Pgml.Raw (XML.Output no_text)] |
|
222 |
|
223 fun split_markup text = |
|
224 (case space_explode no_text text of |
|
225 [bg, en] => (bg, en) |
|
226 | _ => (error ("Internal error: failed to split XML markup:\n" ^ text); ("", ""))); |
|
227 |
|
228 |
|
229 fun block_markup markup = |
|
230 let |
|
231 val pgml = Pgml.Box { orient = NONE, |
|
232 indent = Markup.get_int markup Markup.indentN, |
|
233 content = pgmlterms_no_text } |
|
234 in split_markup (output_pgmlterm pgml) end; |
|
235 |
|
236 fun break_markup markup = |
|
237 let |
|
238 val pgml = Pgml.Break { mandatory = NONE, |
|
239 indent = Markup.get_int markup Markup.widthN } |
|
240 in (output_pgmlterm pgml, "") end; |
|
241 |
|
242 fun fbreak_markup markup = |
|
243 let |
|
244 val pgml = Pgml.Break { mandatory = SOME true, indent = NONE } |
|
245 in (output_pgmlterm pgml, "") end; |
|
246 |
|
247 val state_markup = |
|
248 split_markup (output_pgmltext (pgml PgipTypes.Display pgmlterms_no_text)) |
|
249 |
|
250 val token_markups = |
|
251 [Markup.tclassN, Markup.tfreeN, Markup.tvarN, Markup.freeN, |
|
252 Markup.boundN, Markup.varN, Markup.skolemN]; |
|
253 |
|
254 in |
|
255 |
|
256 val _ = Markup.add_mode proof_generalN (fn (markup as (name, _)) => |
|
257 if name = Markup.blockN then block_markup markup |
|
258 else if name = Markup.breakN then break_markup markup |
|
259 else if name = Markup.fbreakN then fbreak_markup markup |
|
260 else if name = Markup.stateN then state_markup |
|
261 else if member (op =) token_markups name then XML.output_markup ("atom", [("kind", name)]) |
|
262 else ("", "")); |
|
263 |
|
264 end; |
|
265 |
188 |
266 |
189 |
267 (* theory loader actions *) |
190 (* theory loader actions *) |
268 |
191 |
269 local |
192 local |
696 |
619 |
697 |
620 |
698 fun idvalue strings = |
621 fun idvalue strings = |
699 issue_pgip (Idvalue { thyname=thyname, objtype=objtype, name=name, |
622 issue_pgip (Idvalue { thyname=thyname, objtype=objtype, name=name, |
700 text=[XML.Elem("pgml",[], |
623 text=[XML.Elem("pgml",[], |
701 map XML.Output strings)] }) |
624 maps YXML.parse_body strings)] }) |
702 |
625 |
703 fun string_of_thm th = Output.output |
626 fun string_of_thm th = Pretty.string_of |
704 (Pretty.string_of |
|
705 (Display.pretty_thm_aux |
627 (Display.pretty_thm_aux |
706 (Syntax.pp_global (Thm.theory_of_thm th)) |
628 (Syntax.pp_global (Thm.theory_of_thm th)) |
707 false (* quote *) |
629 false (* quote *) |
708 false (* show hyps *) |
630 false (* show hyps *) |
709 [] (* asms *) |
631 [] (* asms *) |
710 th)) |
632 th) |
711 |
633 |
712 fun strings_of_thm (thy, name) = map string_of_thm (PureThy.get_thms thy name) |
634 fun strings_of_thm (thy, name) = map string_of_thm (PureThy.get_thms thy name) |
713 |
635 |
714 val string_of_thy = Output.output o |
636 val string_of_thy = Pretty.string_of o ProofDisplay.pretty_full_theory false |
715 Pretty.string_of o (ProofDisplay.pretty_full_theory false) |
|
716 in |
637 in |
717 case (thyname, objtype) of |
638 case (thyname, objtype) of |
718 (_,ObjTheory) => idvalue [string_of_thy (ThyInfo.get_theory name)] |
639 (_, ObjTheory) => idvalue [string_of_thy (ThyInfo.get_theory name)] |
719 | (SOME thy, ObjTheorem) => idvalue (strings_of_thm (ThyInfo.get_theory thy, name)) |
640 | (SOME thy, ObjTheorem) => idvalue (strings_of_thm (ThyInfo.get_theory thy, name)) |
720 | (NONE, ObjTheorem) => idvalue (strings_of_thm (splitthy name)) |
641 | (NONE, ObjTheorem) => idvalue (strings_of_thm (splitthy name)) |
721 | (_, ot) => error ("Cannot show objects of type "^(PgipTypes.name_of_objtype ot)) |
642 | (_, ot) => error ("Cannot show objects of type "^(PgipTypes.name_of_objtype ot)) |
722 end |
643 end |
723 |
644 |