99 else Pgml.Str s; |
99 else Pgml.Str s; |
100 |
100 |
101 val pgml_syms = map pgml_sym o Symbol.explode; |
101 val pgml_syms = map pgml_sym o Symbol.explode; |
102 |
102 |
103 val token_markups = |
103 val token_markups = |
104 [Markup.tfreeN, Markup.tvarN, Markup.freeN, |
104 [Isabelle_Markup.tfreeN, Isabelle_Markup.tvarN, Isabelle_Markup.freeN, |
105 Markup.boundN, Markup.varN, Markup.skolemN]; |
105 Isabelle_Markup.boundN, Isabelle_Markup.varN, Isabelle_Markup.skolemN]; |
106 |
106 |
107 in |
107 in |
108 |
108 |
109 fun pgml_terms (XML.Elem ((name, atts), body)) = |
109 fun pgml_terms (XML.Elem ((name, atts), body)) = |
110 if member (op =) token_markups name then |
110 if member (op =) token_markups name then |
111 let val content = pgml_syms (XML.content_of body) |
111 let val content = pgml_syms (XML.content_of body) |
112 in [Pgml.Atoms {kind = SOME name, content = content}] end |
112 in [Pgml.Atoms {kind = SOME name, content = content}] end |
113 else |
113 else |
114 let val content = maps pgml_terms body in |
114 let val content = maps pgml_terms body in |
115 if name = Markup.blockN then |
115 if name = Isabelle_Markup.blockN then |
116 [Pgml.Box {orient = NONE, indent = Properties.get_int atts Markup.indentN, content = content}] |
116 [Pgml.Box {orient = NONE, |
117 else if name = Markup.breakN then |
117 indent = Properties.get_int atts Isabelle_Markup.indentN, content = content}] |
118 [Pgml.Break {mandatory = NONE, indent = Properties.get_int atts Markup.widthN}] |
118 else if name = Isabelle_Markup.breakN then |
|
119 [Pgml.Break {mandatory = NONE, indent = Properties.get_int atts Isabelle_Markup.widthN}] |
119 else content |
120 else content |
120 end |
121 end |
121 | pgml_terms (XML.Text text) = map (Pgml.Raw o Pgml.atom_to_xml) (pgml_syms text); |
122 | pgml_terms (XML.Text text) = map (Pgml.Raw o Pgml.atom_to_xml) (pgml_syms text); |
122 |
123 |
123 end; |
124 end; |
132 let |
133 let |
133 val body = YXML.parse_body s; |
134 val body = YXML.parse_body s; |
134 val area = |
135 val area = |
135 (case body of |
136 (case body of |
136 [XML.Elem ((name, _), _)] => |
137 [XML.Elem ((name, _), _)] => |
137 if name = Markup.stateN then PgipTypes.Display else default_area |
138 if name = Isabelle_Markup.stateN then PgipTypes.Display else default_area |
138 | _ => default_area); |
139 | _ => default_area); |
139 in Pgml.pgml_to_xml (pgml area (maps pgml_terms body)) end; |
140 in Pgml.pgml_to_xml (pgml area (maps pgml_terms body)) end; |
140 |
141 |
141 |
142 |
142 fun normalmsg area s = issue_pgip |
143 fun normalmsg area s = issue_pgip |