equal
deleted
inserted
replaced
128 then |
128 then |
129 map (fn (p, name) => |
129 map (fn (p, name) => |
130 Output.output |
130 Output.output |
131 (Thy_Output.string_of_margin ctxt |
131 (Thy_Output.string_of_margin ctxt |
132 (Pretty.indent (Config.get ctxt Thy_Output.indent) p)) ^ |
132 (Pretty.indent (Config.get ctxt Thy_Output.indent) p)) ^ |
133 "\\rulename{" ^ Output.output (Pretty.str_of (Thy_Output.pretty_text ctxt name)) ^ "}") |
133 "\\rulename{" ^ |
|
134 Output.output (Pretty.unformatted_string_of (Thy_Output.pretty_text ctxt name)) ^ "}") |
134 #> space_implode "\\par\\smallskip%\n" |
135 #> space_implode "\\par\\smallskip%\n" |
135 #> Latex.environment "isabelle" |
136 #> Latex.environment "isabelle" |
136 else |
137 else |
137 map (fn (p, name) => |
138 map (fn (p, name) => |
138 Output.output (Pretty.str_of p) ^ |
139 Output.output (Pretty.unformatted_string_of p) ^ |
139 "\\rulename{" ^ Output.output (Pretty.str_of (Thy_Output.pretty_text ctxt name)) ^ "}") |
140 "\\rulename{" ^ |
|
141 Output.output (Pretty.unformatted_string_of (Thy_Output.pretty_text ctxt name)) ^ "}") |
140 #> space_implode "\\par\\smallskip%\n" |
142 #> space_implode "\\par\\smallskip%\n" |
141 #> enclose "\\isa{" "}"))); |
143 #> enclose "\\isa{" "}"))); |
142 |
144 |
143 |
145 |
144 (* Isabelle/Isar entities (with index) *) |
146 (* Isabelle/Isar entities (with index) *) |